Lean sources
The unified Lean 4 / Mathlib codebase (namespace SurfaceBlowup), 66 files, 52300 lines, syntax-highlighted with line anchors; every identifier defined in the codebase links to its definition. Lines carrying a coloured chip are cited by the paper ↔ Lean map. Raw files sit next to the pages (same path, .lean). Root files: SurfaceBlowup.lean · Tests.lean · README.md · lakefile.lean · lean-toolchain · lake-manifest.json.
Toolchain: Lean v4.33.1, Mathlib 0df444a (pinned in lakefile.lean). Main theorems: main_dvr, main_field_form, main_field_form_ramified, recip_main; trust boundary: Basic.lean. Declaration index (reverse map Lean → paper).
SurfaceBlowup/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| Basic.lean | Statement-level definitions (the trust boundary) | 503 | 79 | 43 |
| Main.lean | Main theorems | 120 | 3 | 3 |
SurfaceBlowup/Algebra/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| AlgebraType.lean | Algebra types and integral closures over a discrete valuation ring | 644 | 32 | 3 |
| FactorInvariant.lean | Invariance of factor invariants and uniqueness of algebra types | 324 | 6 | 0 |
SurfaceBlowup/Assembly/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| Formulas.lean | The density formulas for the route-F densities | 139 | 2 | 2 |
| MonicCells.lean | Monic, projective and divisor cells | 1342 | 9 | 3 |
| NullBridges.lean | Strict-transform measures, type events and the projective null bridge | 490 | 18 | 4 |
| TypeEvents.lean | Type events and divisor counts | 1330 | 17 | 0 |
SurfaceBlowup/Blowup/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| CechStability.lean | Stability of the finite Čech coefficients | 312 | 4 | 3 |
| Charts.lean | Blow-up charts, the exceptional line, and curve data | 1158 | 144 | 2 |
| CurveOrders.lean | Curve orders, the exceptional line, and finitely supported local data | 1050 | 26 | 1 |
| CurveSections.lean | Curve sections on the two-chart blow-up | 1110 | 18 | 2 |
| Directions.lean | Closed points and divisors on the exceptional line | 154 | 16 | 0 |
| DivisorPoints.lean | Exceptional divisor points of two-chart curve data | 1459 | 10 | 2 |
| ExceptionalLayers.lean | Exceptional layers of the point blow-up | 842 | 11 | 1 |
| FixedTangentCellBijection.lean | Strict transforms give a bijection on a fixed tangent cell | 480 | 4 | 4 |
| H0Comparison.lean | Comparing surface functions with Čech data on the blow-up | 1245 | 20 | 3 |
| NilpotentGluing.lean | Nilpotent gluing of exceptional levels | 1490 | 16 | 3 |
| PointTransport.lean | Transport of points between blow-up charts | 1284 | 24 | 0 |
| StrictNormalizer.lean | Strict transforms and the strict normalizer | 1497 | 22 | 5 |
| TwoChartCurveData.lean | Two-chart curve data | 1389 | 12 | 0 |
SurfaceBlowup/Formula/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| FiniteFieldCounts.lean | Counting over finite fields | 78 | 3 | 1 |
| LawAlgebra.lean | Expression and law algebra, children of tangent patterns | 914 | 46 | 2 |
| PatternCounts.lean | Counting divisors with a given tangent pattern | 661 | 7 | 3 |
| RationalEval.lean | Evaluating the universal rational functions | 66 | 1 | 0 |
| StateCombinatorics.lean | Combinatorics of states, ranks and safety of the laws | 611 | 14 | 7 |
| TypeTransport.lean | Transport of factorization types and cell measures | 281 | 8 | 1 |
SurfaceBlowup/Measure/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| AdicCylinders.lean | Adic congruences, adic cylinders and division charts | 989 | 47 | 5 |
| AdicTransport.lean | Adic congruences, adic perturbations and transport of cylinder measures | 323 | 10 | 0 |
| Atlas.lean | Ideal-chart atlases and atlas independence of the state measure | 315 | 7 | 4 |
| Haar.lean | Haar measures on unramified extensions and strict-transform normalizations | 376 | 6 | 2 |
| HenselProducts.lean | Hensel factorization, finite products and coefficient measures | 1267 | 25 | 0 |
| MemberBoxes.lean | Measure of member boxes | 601 | 2 | 2 |
| MemberCharts.lean | Charts of concrete members and the inseparable locus | 602 | 14 | 3 |
| Normalizer.lean | Generator normalization and residue-ideal counts | 381 | 9 | 5 |
| PrimitiveLocus.lean | The primitive locus, state measures, and integral closures | 381 | 14 | 2 |
| StateVolumes.lean | Single-state residue ideal counts and Haar-measure transport | 209 | 4 | 2 |
SurfaceBlowup/Reciprocity/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| Defs.lean | Reciprocity: definitions and basic lemmas | 1044 | 95 | 23 |
| Main.lean | The reciprocity law (Theorem R) | 301 | 5 | 8 |
| Patterns.lean | Pattern sums, crossing factorization and unitarity | 1045 | 23 | 11 |
| Plethysm.lean | Plethystic calculus for the reciprocity law | 1034 | 48 | 7 |
| Quantum.lean | Reciprocity: the quantum torus, dilations and reciprocal substitution | 920 | 72 | 11 |
SurfaceBlowup/Recursion/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| ChildMembers.lean | Child members and terminal states of the blowup recursion | 1215 | 14 | 4 |
| Events.lean | Return and exit events of the blowup recursion | 922 | 14 | 7 |
| Members.lean | Members of the recursion universe | 1427 | 71 | 2 |
| OrderDefect.lean | Order defects and child data for the blowup recursion | 1151 | 14 | 2 |
| RootCellLaw.lean | The root cell law | 1365 | 7 | 4 |
| Termination.lean | Termination of the recursion | 1316 | 22 | 3 |
SurfaceBlowup/Surfaces/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| ChartCompletions.lean | Completions of the blow-up charts of the concrete surface | 894 | 7 | 0 |
| Completeness.lean | Completeness of the concrete surface | 414 | 14 | 0 |
| ConcreteAtlas.lean | Ideal atlases and curve data on the concrete surface | 725 | 5 | 0 |
| ConcretePoints.lean | Closed points on the blow-up of the concrete surface | 439 | 7 | 0 |
| ConcreteStrictTransforms.lean | Volumes and strict transforms on the concrete surface | 486 | 6 | 2 |
| Lengths.lean | Concrete surfaces, chart substitutions and lengths | 1284 | 80 | 7 |
| PowerSeries.lean | Power series, residue bases and the local structure of concrete surfaces | 1011 | 25 | 1 |
| Regularity.lean | Regularity of the concrete surface | 691 | 15 | 1 |
| TruncatedSeries.lean | Truncations of `k⟦T, X⟧` and contacts on the special fibre | 556 | 16 | 0 |
SurfaceBlowup/Unramified/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| DescentTypes.lean | Types under unramified base change | 366 | 7 | 3 |
| Extension.lean | Binary forms, factor cells and unramified extensions | 1160 | 60 | 0 |
| FactorCells.lean | Factor cells: residue cells of factor products and root-field isomorphisms | 547 | 11 | 0 |
| FrobeniusDescent.lean | Frobenius descent for unramified extensions | 1189 | 15 | 4 |
| HomogeneousCells.lean | Measure-preserving maps between homogeneous cells | 781 | 5 | 2 |
| LocalDescent.lean | Local lengths and finite quotients of completions | 190 | 5 | 2 |
| PolynomialTypes.lean | Polynomial types, form products and residue cells | 1251 | 19 | 1 |
Tests/
| file | title | lines | public decls | cited by the paper map |
|---|---|---|---|---|
| NonVacuity.lean | Non-vacuity of the hypotheses of `main_dvr` | 128 | 12 | 1 |
| Regression.lean | Regression guards for the universal density expressions | 2031 | 22 | 16 |