The formalization: what is proved, and how to trust it

The paper's two main theorems are machine-checked in Lean 4 over Mathlib: Theorem 1.1 for every complete discrete valuation ring with finite residue field, and Theorem 1.2 as identities of rational functions. This page says exactly what the Lean statements are, what a reader has to audit to trust them, which certificates exist, and how far the rest of the paper is formalized.

1. The four main theorems

All four depend only on the axioms propext, Classical.choice, Quot.sound (#print axioms, re-run by tools/release_check.sh; log below). The codebase contains no sorry, admit, axiom or native_decide.

theorem main_dvr (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]
    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]
    (htop : IsAdic (IsLocalRing.maximalIdeal O))
    (n : ℕ) (σ : FactorType) :
    SurfaceBlowup.monicDensity O n σ =
        densityValue (monicExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) ∧
    SurfaceBlowup.projectiveDensity O n σ =
        densityValue (projectiveExpr n σ) (Nat.card (IsLocalRing.ResidueField O))

main_dvr is Theorem 1.1: for every complete DVR O with finite residue field (any characteristic, any ramification), with its adic topology, Borel σ-algebra and normalized Haar measure, the monic and projective type probabilities are the values at q = |k| of the universal expressions monicExpr n σ, projectiveExpr n σ (defined by the finite recursion of Sections 6–7). The hypotheses hn, hσ, hdegree are not used by the proof; they are kept so that the statement is, constant for constant, the certified one. Tests/NonVacuity.lean instantiates it at 𝔽_q⟦X⟧.

theorem recip_main (n : ℕ) (hn : 0 < n) (σ : FactorType) :
    (monicExpr n σ).rational =
      ((lawCoeff (rootLaw n) σ).subst (.inv .var)).rational ∧
    (projectiveExpr n σ).rational =
      ((projectiveExpr n σ).subst (.inv .var)).rational

recip_main is Theorem 1.2, coefficientwise: A_{n,σ}(q) = B_{n,σ}(1/q) and R_{n,σ}(1/q) = R_{n,σ}(q) in ℚ(q), where B_{n,σ} is the coefficient of the root law rootLaw n (the law of S(1;n), which root_cell_law identifies with the Xⁿ-cluster model).

theorem main_field_form (n : ℕ) (σ : FactorType) :
    ∃ A R : RatFunc ℚ, A = (monicExpr n σ).rational ∧ R = (projectiveExpr n σ).rational ∧
      (∀ q : ℕ, PrimePower q → RegularAt A q ∧ RegularAt R q) ∧
      (∀ q : ℕ, PrimePower q → RatFunc.eval (RingHom.id ℚ) q A = (monicExpr n σ).eval q ∧
        RatFunc.eval (RingHom.id ℚ) q R = (projectiveExpr n σ).eval q) ∧
      ∀ (p : ℕ) [Fact p.Prime] (K : Type) [Field K] [Algebra ℚ_[p] K] [Algebra ℤ_[p] K]
        [IsScalarTower ℤ_[p] ℚ_[p] K] [FiniteDimensional ℚ_[p] K]
        [TopologicalSpace (padicIntegers p K)] [IsTopologicalRing (padicIntegers p K)]
        [CompactSpace (padicIntegers p K)] [T2Space (padicIntegers p K)]
        [SecondCountableTopology (padicIntegers p K)] [MeasurableSpace (padicIntegers p K)]
        [BorelSpace (padicIntegers p K)],
        PadicUnramified p K → IsAdic (Ideal.span {(p : padicIntegers p K)}) →
          monicDensity (padicIntegers p K) n σ = densityValue (monicExpr n σ)
            (Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)})) ∧
          projectiveDensity (padicIntegers p K) n σ = densityValue (projectiveExpr n σ)
            (Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)})) ∧
          monicDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)
            ((Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)}) : ℕ) : ℚ) A :
              ℚ) : ℝ) ∧
          projectiveDensity (padicIntegers p K) n σ = ENNReal.ofReal ((RatFunc.eval (RingHom.id ℚ)
            ((Nat.card (padicIntegers p K ⧸ Ideal.span {(p : padicIntegers p K)}) : ℕ) : ℚ) R :
              ℚ) : ℝ)

theorem main_field_form_ramified (n : ℕ) (σ : FactorType) (p : ℕ) [Fact p.Prime] (K : Type)
    [Field K] [Algebra ℚ_[p] K] [Algebra ℤ_[p] K] [IsScalarTower ℤ_[p] ℚ_[p] K]
    [FiniteDimensional ℚ_[p] K]
    [TopologicalSpace (padicIntegers p K)] [IsTopologicalRing (padicIntegers p K)]
    [CompactSpace (padicIntegers p K)] [T2Space (padicIntegers p K)]
    [SecondCountableTopology (padicIntegers p K)] [MeasurableSpace (padicIntegers p K)]
    [BorelSpace (padicIntegers p K)]
    (had : letI := padicIntegers_isDVR p K; IsAdic (IsLocalRing.maximalIdeal (padicIntegers p K))) :
    letI

2. The trust boundary

Lean checks proofs, not statements. To trust the theorems above a reader must audit only:

1. SurfaceBlowup/Basic.lean (~500 lines): factorization types, the rational expressions Expr, laws, recursion states and tangent patterns, the weights, the recursion stateLaw, the universal expressions monicExpr/projectiveExpr, and the densities monicDensity/projectiveDensity. These are, constant for constant, the owner-signed definitions published as Prove2Me nodes N001–N010 (namespace SurfaceBlowupV2), checked at kernel level by Checks/run_checks.sh.
2. The statements of the four theorems above (in Main.lean and Reciprocity/Main.lean).

Every other file contains only proofs and auxiliary definitions that do not occur in these statements.

Human sign-off. The definitions (N001–N010) and the statement of main_field_form (Theorem 1.1 for unramified K/ℚ_p, Prove2Me node N660) were signed off by the owner before the formalization campaign; the statement of recip_main (N1319) was signed off on 2026-10-09. The statement of main_dvr uses only the signed definitions and is kernel-identical to the certified general-DVR statement (MONOLITH_REPORT_general_dvr). [OWNER: confirm whether the main_dvr statement text itself has been signed off.]

How the proof differs from the paper. The formal proof follows the paper's architecture (recursion on blow-up states, Gaussian measure identity, Hensel assembly, contact algebra for reciprocity) but works on the concrete surfaces O⟦T,X⟧/(π − u·T^a·X^b) rather than on all regular surfaces, replaces analytic arguments (analytic normalization, inverse-function theorem, change of variables) by finite-digit congruence and cylinder-set arguments, replaces the formal-scheme cohomology of Section 4 by explicit two-chart Čech complexes, and handles inseparability through type predicates with finite integral closures plus a Haar-null bridge (orig_monicDensity_eq). Nothing is cited from the literature: everything bottoms out in Mathlib.

3. Certificates

• Release check of this codebase (tools/release_check.sh): build (8771 jobs), axioms of the four main theorems, statement preservation (3/3 KERNEL_OK: main_dvr, recip_main, main_field_form against the certified one-theorem-per-file trees), forbidden-token scan, warning count (exactly the 5 unused frozen hypotheses).
• Monolith certificates of the trees the codebase was obtained from: the published 1001-theorem tree for main_field_form, its reciprocity extension (133 theorems) for recip_main, and the general-DVR tree for main_dvr (with non-vacuity over 𝔽_p⟦X⟧ and 𝔽_p^m⟦X⟧).

Copies: release check (final) · axioms of the main theorems · monolith certificate: main_field_form · monolith certificate: main_dvr (general DVR) · monolith certificate: recip_main.

'SurfaceBlowup.main_dvr' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.main_field_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.main_field_form_ramified' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.recip_main' depends on axioms: [propext, Classical.choice, Quot.sound]

4. Prove2Me

The SurfaceBlowupV2 tree (1201 nodes, incl. main_field_form N660 and recip_main N1319) is published PRIVATE on Prove2Me; links resolve only for the owner's account until it is made public. main_dvr (the general-DVR theorem) and the unified SurfaceBlowup codebase are not on Prove2Me. Visibility: PRIVATE. Link pattern used on this site: https://prove2.me/theorems/{theorem_id} — [UNVERIFIED: the API documents only https://prove2.me/api/v1/theorems/{theorem_id}; the public page pattern is a guess (OWNER: confirm)]. The unified codebase was obtained from those trees by merging along the usage DAG and three golfing cycles; declarations are matched to Prove2Me nodes by name and a curated alias table.

5. How much of the paper is formalized

The map below lists every numbered statement of the paper (32 theorems, lemmas, propositions, corollaries, examples and remarks), the key displays ((1.1)–(1.4), (G), (H), (S), (T), the recursion and assembly displays, the Section 10–11 formulas), and the key unnumbered definitions — 82 entries in all. Relations: exact / definition — the Lean statement or definition is the paper's; specialization — proved in a special setting (concrete surfaces; a = b = 1); covered by lemmas — no single Lean statement, the listed declarations jointly establish the content, often restructured; instances checked — particular values only; not formalized.

Not formalized: the totally ramified recursion of Section 10 (only the values A_(3,1)(3) = 10/121, A_(4,1)(2) = 107/1533, R_(4,1)(2) = 856/15841 are checked, and the projective half of Corollary 10.3 is an instance of recip_main); the literature comparisons of Section 11 (root moments, the BGMR splitting recursion, Shmueli's unramified formulas); the crossing reciprocity formula of Theorem 9.3; the scaling identities in (H); and the worked Example 5.2. The map, as JSON: data/paper_lean_map.json (with the reverse index Lean → paper); browsable reverse index: declaration index.

6. The full map

Click a column header to sort.