Formal verification

Lean 4 formalisation

Thirty foundational PT theorems, machine-checked with no sorry.

The arithmetic core of Persistence Theory is reproduced in full in Lean 4 + Mathlib. The critical path $T_1 \to T_3 \to s = 1/2 \to T_2 \to L_0 \to T_7 \to W_7\text{-}1$ is kernel-verified in both directions: every step is a formal proof whose correctness is guaranteed by the Lean kernel, and the W7-1 spiral identity now carries both directions. About one hundred and sixty secondary modules cover the surrounding ecosystem. No [THM] statement from Chapter 1 is left on paper alone.

Build status (2026-05-24) : Lean v4.30.0-rc2 · Mathlib master @ e12bcd0 · `lake build` clean on 3587 jobs.

named theorems on the critical path
kernel-verified, 0 sorry
including W7-1 reverse, T6b full 4-axiom, T2 spectral bridge

196

Lean modules in total
(8 on the critical path
+ 188 in the ecosystem)

~2,885

formal declarations
(theorems + lemmas + definitions
+ instances)

The critical path

All statements below are proved without external hypotheses beyond Mathlib: each step depends only on the previous ones. Read left to right, the diagram matches the exact logical dependency verified by the Lean kernel.

Forbidden mod-3 transitions

→

Antidiagonal transfer matrix

→

s = ½

Unique stationary distribution

→

α_cons = s² = ¼

→

Geometric is max-entropy

→

μ* = 15

Unique fixed point

→

Mertens

Compactness bound

→

W7-1

Spiral identity

Site theorems and their Lean modules

Each theorem listed below has a dedicated page on this site and a matching Lean module that can be opened directly on GitHub.

Theorem	Short statement	Lean module	Status
GFT	$\log_2 m = D_\mathrm{KL} + H$ — fundamental principle of persistence.	PT.Information.GFTIdentity	kernel-verified, 0 sorry
L0	The unique memoryless maximum-entropy distribution on even gaps.	PT.Information.L0MaxEntropy	kernel-verified, 0 sorry
T1	The sieve forbids two consecutive identical residues mod 3.	PT.Sieve.T1ForbiddenTransitions	kernel-verified, 0 sorry
T2	Exact spectral identity $\|\lambda_2(T_{30})\| = s^2 = 1/4$.	PT.Conservation.T2Alpha	kernel-verified, 0 sorry
T3	$T_3 = \mathrm{antidiag}(1,1)$ — the mod-3 matrix is purely off-diagonal.	PT.Sieve.T3Antidiagonal	kernel-verified, 0 sorry
T4	$\alpha_k \to 1/2$ as the sieve depth $k \to \infty$.	PT.NumberTheory.T4MertensActivePrimes	kernel-verified, 0 sorry
T5	After p = 2 crystallises, the reduced sieve sector admits a unique physical attractor: $\mu^* = 3+5+7 = 15$.	PT.FixedPoint.T7MuStar	kernel-verified, 0 sorry
T6	$\sin^2 \theta_p = \delta_p (2 - \delta_p)$ — trigonometry emerges from the sieve.	PT.Holonomy.CyclicPhaseIdentity	kernel-verified, 0 sorry
N1	The primes are the unique atoms of the multiplicative monoid $(\mathbb{N}_{\geq 1}, \times)$.	PT.Sieve.N1AtomicUniqueness	kernel-verified, 0 sorry
N2	The Eratosthenes sieve is the unique self-consistent multiplicative sieve on $\mathbb{N}_{\geq 2}$.	PT.Sieve.N2SelfCoherence	kernel-verified, 0 sorry
N3	$(\mathbb{N}_{\geq 1}, \times)$ is the unique free commutative cancellative UFD monoid with countable atoms.	PT.Sieve.N3aMinimalMonoid	kernel-verified, 0 sorry
N4	In the canonical sieve ordering, $p = 3$ is the first dynamical level. $p = 2$ has a structurally distinct role (info / anti-info).	PT.Sieve.N4DimensionCascade	kernel-verified, 0 sorry
BA5	At the reduced attractor $\mu^* = 15$, the sieve coupling is the product $\prod_{p \in \{3,5,7\}} \sin^2\theta_p(q_+)$.	PT.Anomaly.BargmannBA5	kernel-verified, 0 sorry
G1	On the CRT-structured sieve simplex, $D_{KL}$ is the unique consistent divergence.	PT.Information.T6cG1Autonomous	kernel-verified, 0 sorry
G3	Fisher is the unique Markov-monotone Riemannian metric on the simplex.	PT.Information.G3FisherUniqueness	kernel-verified, 0 sorry
Mertens	The function $M(x) - \log\log x$ is bounded — classical, imported into PT.	PT.NumberTheory.T5Mertens	scaffold
ActivePrime	A prime $p$ is active iff $\gamma_p > s = 1/2$ — the active set is exactly $\{3,5,7\}$.	PT.Holonomy.ActivePrimeCriterion	kernel-verified, 0 sorry
Nc	$N_c = N_{\text{spatial}} = 3$: unique integer solution of $(N_c+1)!/(N_c+3) = 2^{N_{\text{spatial}}-1}$.	PT.FixedPoint.T7MuStar	kernel-verified, 0 sorry
CRT	The sieve factors additively: $\mathbb{Z}/P \cong \bigoplus_p \mathbb{Z}/p$. Operations at different primes commute.	PT.Stochastic.CRTFactorizationT2	kernel-verified, 0 sorry

Theorems T0, E, F, G, FisherKoide, FourierKoide and OS3 are not formalised yet.

Full catalog by topic

Beyond the critical path and the site theorems featured at the top of this page, 188 additional modules (out of 196 total in the repository) cover the surrounding ecosystem: variants, refinements, auxiliary identities, algebraic structures. Each topic is collapsed below; open a section to see the full list. Every module links to its .lean file on GitHub.

Sieve PT.Sieve.* 32 modules

AdmissibleRMasterCharacterisation — Admissible residues `R` — master characterisation (App N synthesis)
AdmissibleResiduesArithmetic — Admissible residues — Arithmetic invariants (App N extension)
AdmissibleResiduesCubeSumMod — Admissible residues — Sum of cubes modulo various `q` (App N extension)
AdmissibleResiduesFifthPowerSumMod — Admissible residues — Sum of fifth powers modulo various `q` (App N extension)
AdmissibleResiduesFourthPowerSumMod — Admissible residues — Sum of fourth powers modulo various `q` (App N extension)
AdmissibleResiduesProductMod — Admissible residues — Product modulo several moduli (App N extension)
AdmissibleResiduesSixthPowerSumMod — Admissible residues — Sum of sixth powers modulo various `q` (App N extension)
AdmissibleResiduesSquareSumMod — Admissible residues — Sum of squares modulo various `q` (App N extension)
AdmissibleSemigroupQuotient — Admissible residues — Quotient `R / selfInverses ≅ ℤ/2ℤ` (App N)
AdmissibleSquareGroupStructure — Admissible residues — Subgroup structure of squares modulo 30 (App N)
Bimodality — Bimodality theorem (Appendix N)
BimodalityCardinality — Bimodality — cardinality balance from `(ℤ/5ℤ)*` character orthogonality
BimodalityCharacterFormula — Bimodality — Closed-form character formula `δ̄(r) = 9 - 2·(r/5)` (App N)
BimodalityT1Projection — Bimodality as T1 projection (Appendix N, #42)
CoprimeAdmissibilityProduct — Admissible residues — Multiplicative invariants (App N extension)
KleinFourEmbedding — Klein-four embedding `selfInverses ↪ (ℤ/2ℤ)²` (App N)
LegendreLogParity — Legendre symbol mod 5 = log-parity (Appendix N, #41)
N2UniqueFixedPoint — N2 — Uniqueness: `ℙ` is the unique self-coherent subset of `ℕ_{≥2}`
N3aFactorisation — N3a — Explicit factorisations and PT-relevant instances (Ch02 extension)
N3bSieveTaxonomy — N3b — Sieve Taxonomy: Minimality of the Operation (Eratosthenes vs Lucky)
N3cCanonicalOrdering — N3c — Canonical Ordering of Primes: `2 < 3 < 5 < 7 < ⋯`
N4PrimeCascade — N4 — Bifurcation at `p = 2, 3`: info/anti-info versus first cascade
PrimitiveRootCascade — Primitive root cascade across the PT-active primes `p ∈ {3, 5, 7}`
PrimorialCoprime — Admissible residues — Coprimality with the third primorial `30 = 2·3·5`
SixRough — 6-Rough Integers — Definition and Residue Characterisation
T1AntidiagOrbits — T1 — Orbits of the antidiagonal transfer `T_3`
T1OrbitsZMod5 — T1 — Orbits of the doubling map on `(ℤ/5ℤ)*`
T1OrbitsZMod7 — T1 — Orbits of the multiplication-by-3 map on `(ℤ/7ℤ)*`
T6aFieldStructure — T6a — Field-structure uniqueness: `R_p = {0}` in `ℤ/pℤ`
T6bAxiomsC1C4 — T6b — Axioms C1–C4 force `E_p = {0}` (Eratosthenes from ring congruence)
T6bAxiomsFull — T6b (full) — Axioms C1–C4 force `d` prime and `E = {0}`
TotientCascadeIdentities — Euler-totient identities for the PT cascade

Stochastic PT.Stochastic.* 27 modules

SpectralDominance — Spectral Dominance — Perron eigenvalue and spectral closure of `T_3`
T2T30Normalisation — T2 — Three-factor CRT normalisation `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T2T3CesaroLimit — `T_2 ⊗ T_3` Cesàro limit — Finite-time exact equality on the 2D Kronecker block
T2T3KroneckerEigenvalues — Full spectrum of `T_2 ⊗ T_3` (Ch07 extension)
T2T3PerronEigenvectorUniqueness — Uniqueness (up to scaling) of the Perron eigenvector of `T_2 ⊗ T_3`
T2T3SpectralMixing — Spectral mixing analysis for `T_2 ⊗ T_3`
T2T3StationaryUniqueness — Unicité de la distribution stationnaire pour `T_2 ⊗ T_3`
T2T3T5KroneckerSpectrum — `T_30` Kronecker spectrum: explicit 4 eigenpairs and absolute-value
T30AntiSector — `T_30` anti-sector eigenvalues (Ch07 extension)
T30CharPolyComplete — T2 — Complete characteristic polynomial of `T_30` (even-polynomial closure)
T30FullDeterminantIdentity — T2 — Full determinant identity for `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T30FullEigenpairCount — Full eigenpair count for `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T30FullSpectralAnalysis — T2 — Full spectral analysis of `T_30 = T_2 ⊗ T_3 ⊗ T_5` (master synthesis)
T30PerronAntiCommutator — Perron / anti commutator — `[Π_+, Π_-] = 0` and `[T_3, Π_±] = 0`
T30PerronUniqueness — Uniqueness (up to scaling) of the Perron eigenvector of `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T30SpectralMixingExtended — Extended spectral mixing analysis for `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T30TraceCubeIdentity — T2 — Cubic identities `tr(T_30^3) = 0` and Newton–Girard consequences
T30TraceDeterminant — T2 — Trace and determinant invariants of `T_30 = T_2 ⊗ T_3 ⊗ T_5`
T30TraceFifthPowerIdentity — T2 — Quintic identities `tr(T_30^5) = 0` and Newton–Girard consequences
T30TraceFormulaExtended — T2 — Trace formula for `T_30^n` via Kronecker-power factorisation
T30TraceFourthPowerIdentity — T2 — Quartic identities `tr(T_30^4) = 2 · tr(T_5^4)` and Newton–Girard consequences
T30TracePowerSequence — T2 — Explicit trace sequence `(tr T_30^n)_{n = 1..6}`
T30TraceSquaredIdentity — T2 — Algebraic identities `tr(T_30^a) · tr(T_30^b) = 0` and consequences
T3CesaroLimit — `T_3` Cesàro limit — Exact equality at even `N` (Ch07 extension)
T3SpectralDecomposition — Spectral decomposition extension — Eigenbasis closure for `T_3`
T5Canonical — T_5 canonical — concrete instance of `T5Like` making T2 unconditional
T5CanonicalTight — T_5 canonical (tight) — concrete instance of `T5Like` saturating `|λ₂| = 1/4`

Conservation PT.Conservation.* 26 modules

BifurcationVertexEdge — Bifurcation vertex-edge — two canonical PT parameters
ConservationActivePrimes — Conservation Identity at Active Primes — `{3, 5, 7}` and `μ* = 15`
ConservationID — Conservation Identity — `∑ g_n = p_{N+1} - 2`
ConservationIDExtensions — Conservation Identity — algebraic extensions
ConservationIDPrimorial — Conservation ID at primorial indices (Ch03 extension)
CumulativeBoundsExtended — Cumulative gap bounds — extension to `N ∈ {5, …, 10}`
GapBoundedBelow — Gap sequence — Strict positivity / bounded below (Ch03 extension)
GapDistributionAllMomentsMaster — Master aggregator — all six distributional central moments of the PT
GapDistributionFifthMoment — Distributional fifth central moment of the PT gap distribution —
GapDistributionKurtosisExtended — Distributional kurtosis (fourth central moment) of the PT gap
GapDistributionMeanExtended — Distributional mean of the PT gap distribution — extension `N ∈ {5, …, 10}`
GapDistributionMomentsSummary — Summary table — first four distributional moments of the PT gap distribution
GapDistributionSixthMoment — Distributional sixth central moment of the PT gap distribution —
GapDistributionSkewExtended — Distributional skewness (third central moment) of the PT gap
GapDistributionVariance — Variance of the **normalised PT gap distribution** — small `N`
GapDistributionVarianceExtended — Distributional variance of the PT gap distribution — extension `N ∈ {5, …, 10}`
GapEntropyBound — Shannon entropy of the PT prime-gap distribution
GapMaxBound — Gap sequence — Upper bounds on `g_n` (Ch03 extension)
GapMomentsNExtended — Prime gap moments — extension to `N ∈ {5, …, 10}`
GapParityDecomposition — Gap parity decomposition for the PT prime sequence (Ch03 extension)
GapStatisticalMoments — Higher central moments of PT prime gaps — `N ∈ {3, 4}`
GapSumMasterIdentity — Gap-sum master identity — synthesis aggregator
GapVarianceSmallN — Gap mean and variance on small `N` — `N ∈ {2, 3, 4}`
PrimeGapMoments — Prime gap moments — weighted sums on the PT prime sequence
PtPrimeStructuralTheorem — PT prime structural theorem — master synthesis aggregator
T2SpectralBridge — T2 — Spectral bridge: `|λ_2(T_30)| = s² = 1/4 = α_cons`

Information PT.Information.* 27 modules

BekensteinBound — Bekenstein Bound — `D_KL(P ‖ U_m) ≤ log m`
BekensteinEquality — Bekenstein Equality — `D_KL(P ‖ U_m) = log m ↔ P` is a Dirac mass
BekensteinExtensions — Bekenstein Bound — Saturation and corner equalities (Ch04 #18 extension)
BinaryEntropyMonotonicity — Monotonicity envelope of binary entropy
ConditionalEntropy — Conditional entropy `H(X | Y) := H(X, Y) − H(Y)`
CrossEntropyBound — Cross-entropy `H(p, q) := -∑ p log q` — algebraic identities and bounds
EntropyAdditivityCorners — Entropy / GFT additivity at the two corners (Ch04 extension)
EntropyBoundsTight — Tight entropy bounds — strict Bekenstein away from delta (Ch04 extension)
EntropyDifferenceSymmetric — Entropy differences at PT-canonical points
EntropyJointProduct — Joint entropy and the `log m` increment from independent uniforms
EntropyMasterFramework — Entropy Master Framework — Unified PT view of GFT, Bekenstein, additivity,
EntropyMonotonicity — Monotonicity properties of Shannon entropy
EntropyOfBinaryDistribution — Entropy of binary distributions at PT-canonical points
EntropyTernaryDistribution — Entropy of ternary distributions at PT-canonical points
G2FisherEmergence — G2 — Émergence of the Fisher information metric as the Hessian of `D_KL`
GFTOnZMod30 — GFT identity on the 8 admissible residues of `(ℤ/30ℤ)*` (Ch04 #18 application)
GFTSpecialMValues — GFT — Specialised instances at `m ∈ {2, 8, 30}` (Ch04 extension)
GFTSpecialisations — GFT — Specialisations and corollaries (Ch04 #16/#18 extensions)
InfoTheoreticMaster — Information-Theoretic Master — TIER 2 extension of `EntropyMasterFramework`.
KLAdditivityFromMI — KL Additivity via the GFT identity (alternative route through `H(joint)`)
KLAdditivityProduct — KL divergence — Additivity at the delta corner (Ch04 extension)
L0Uniqueness — L0 — Uniqueness of the maximum-entropy distribution
MutualInfoDistributional — Distributional mutual information `I(X; Y)` for arbitrary joints
MutualInformationBasic — Basic Mutual Information `I(X; Y) := H(X) + H(Y) - H(X, Y)`
RelativeEntropyAdditivity — Additivity of relative entropy on tensor products (Ch04 §"Additivité KL")
ShannonEntropyConcavity — Concavity of Shannon entropy
T6cChencov — T6c — Shannon entropy infrastructure and Cauchy's logarithmic equation

Holonomy PT.Holonomy.* 29 modules

ActivePrimeAnalyticMonotonicity — Active Prime Analytic Monotonicity — uniform inactivity for every `p ≥ 11`
ActivePrimeMargins — Active Prime — Quantitative margins (Ch06 extension)
ActivePrimeMonotonicity — Active Prime Monotonicity — extension of inactivity beyond `p ∈ {11, 13}`
AlphaGammaRelation — Algebraic relations between `α_bare`, `Π γ_p` and `Σ γ_p` on the active cascade
AlphaInverseCascadeIdentity — `α_bare⁻¹` Cascade Identity (structural exhaustion)
AlphaInversePowerSequence — Inverse-power sequence of the bare coupling — `(α_bare⁻¹)^n` for `n = 1..5`
AlphaInverseTimesGammaSum — Mixed invariant `α_bare⁻¹ · Σ γ_p` and its inverse power-tower
AlphaPowerSequence — Power sequence of the bare coupling — `α_bare^n` for `n = 1..5`
AlphaTimesGammaSum — Mixed invariant `α_bare · Σ γ_p` and its power-tower `α_bare^n · Σ γ_p`
CouplingReconstruction — Coupling Reconstruction — `α_bare = ∏_{p ∈ {3,5,7}} sin²θ_p`
CouplingReconstructionBounds — Coupling reconstruction — Bounds and reciprocal (Ch09 #39 extension)
CyclicPhaseAlgebraic — Cyclic Phase — Algebraic content of Route 3 (Fisher), audit row #25
CyclicPhaseInversion — Cyclic Phase — Inversion and monotonicity (Route 2 proxy, Ch06 #24)
CyclicPhaseSpectral — Cyclic Phase Identity — **Route 2 (Spectral / Fourier contraction)**
CyclicPhaseTable — Cyclic phase — Complete table at `q = qPT = 13/15` (Ch06 extension)
GammaMonotonicity — Gamma Monotonicity — `γ_p > γ_{p'}` for `3 ≤ p < p'`
GammaPrimorialProduct — Joint invariant `Γ_active · ∏ p` over the active cascade `{3, 5, 7}`
GammaProduct — Product of anomalous dimensions `∏ γ_p` over the active cascade `{3, 5, 7}`
GammaRatio — γ_p / γ_{p'} — Ratios of anomalous dimensions across the PT cascade
GammaSumActive — Sum of anomalous dimensions `Σ γ_p` over the active cascade `{3, 5, 7}`
GammaSumProduct — Combined sum–product invariant `Σ_active · Π_active` over `{3, 5, 7}`
GammaTablesExtended — γ_p — Extended exact table for `p ∈ {3, 5, 7, 11, 13, 17, 19, 23}`
HolonomyMasterFramework — Holonomy — Master Framework (aggregator)
InvAlphaSquaredBracket — `(1/α_bare)²` and higher inverse powers (Ch09 extension)
InverseSinSq — Inverse cyclic-phase squared sines `1 / sin²θ_p`
InverseSinSqProduct — Product of inverses `∏ 1 / sin²θ_p` (active cascade + echo extension)
SinSqProductBounds — `∏ sin²θ_p` — Partial product bounds on the active cascade (Ch09 extension)
SinSqProductChain — `∏ sin²θ_p` — Extended chain over `{3, 5, 7, 11, 13}` (Ch09 echo-prime extension)
SinSqRatios — `∏ sin²θ_p` — Ratios of partial products (Ch09 cascade)

Fixed point PT.FixedPoint.* 4 modules

CrystallisationBinary — Crystallisation binaire — `μ = 17 ⟶ μ* = 15`
DimensionProtection — Dimension protection (audit row #35)
FixedPointMasterTheorem — FixedPoint Master Theorem — `μ⋆ = 15` and its full arithmetic ecosystem
T7GlobalUniqueness — T7 — Global uniqueness of `μ* = 15` (Appendix, item #34)

EML (Sheffer) PT.EML.* 7 modules

EMLAlgebra — EML — Algebraic properties (App O extension)
EMLDepth3 — EML — Depth-3 constructions (App O extension)
EMLIdentities — EML algebraic identities (App O follow-up)
EMLSheffer3Args — EML — 3-argument extension and Sheffer composition (App O extension)
QParameterMonotonicity — `q_+(μ)` and `q_-(μ)` — Strict monotonicity in `μ` (App O extension)
QPlusQMinusComparison — Comparison of `q_+(μ)` and `q_-(μ)` on `(0, ∞)` (App O addendum)
QSheffer — EML primitivity of `q_+` and `q_-` (App O)

Analysis PT.Analysis.* 1 module

W7SpiralIdentityReverse — W7-1 — Reverse direction of the spiral identity

Math/physics bridge PT.Bridge.* 20 modules

BridgeAxioms — The Six Bridge Axioms BA0–BA5 — Canonical Wrappers
Buchstab — The Buchstab Inductive Limit (Theorem `thm:inductive_limit`)
CauchyMultiplicativeExp — Multiplicative Cauchy functional equation : `f(x+y) = f(x)·f(y)` ⇒ `f = exp(c·x)`
CutoffMeanCharacterisation — Characteristic scale of the PT spectral cutoff
FiniteSpectralTriple — Finite spectral triple `ST_F` of the PT bifurcation
GibbsDistribution — Gibbs distribution on a finite spectrum
HeatKernelPostulate — Heat-kernel postulate: PT cutoff = Gibbs partition function
HiggsCutoffUniqueness — Uniqueness of the PT spectral cutoff `f_PT(u) = exp(-u/N_b)`
HilbertReconstruction — Lemma G — Hilbert Reconstruction (Theorem `thm:hilbert_reconstruction`)
JaynesPrinciple — Jaynes Maximum Entropy Principle and the PT heat-kernel cutoff
K4LambdaH — K4 closure : `λ_H = 1/8` from the canonical identification (E6c) + cutoff uniqueness (E8)
MathPhysicsDissolution — Math / Physics Dissolution — A meta-statement on the PT bridge
MetricReconstruction — Lemma F — Metric Reconstruction (Theorem `thm:metric_reconstruction`)
OS3Uniform — Uniform OS3 reflection positivity (Theorem `thm:OS3_uniform`)
PTCascadeDerivationChain — The PT Derivation Chain — Cross-Axes Synthesis Theorem
PartitionFunctionFactorisation — Multiplicativity of the partition function on tensor products
ScaleFromFiniteSpectralTriple — Scale of the PT spectral cutoff from `ST_F`
ShoreJohnsonG1Spectral — Shore--Johnson G1 applied to PT spectral cutoffs
SpectralAction — Spectral action `Tr f(D²/Λ²)` for the PT bifurcation (scalar case)
StatusGraphFormalisation — Status Graph Formalisation — A formal dependency graph for PT modules

CRT decoupling PT.CrtDecoupling.* 7 modules

Empirical — Theorem 6.1 (empirical form) — Phase 2
Main — Geometric Decoupling Theorem, Ruelle form (Theorem 6.2)
Phase3 — Phase 3 — Infinite-state Theorem 6.1 via Birkhoff–Hopf
Phase4 — Phase 4 — The sieve path space and its shift dynamical system
Phase4Instance — Phase 4 — Existence of a populated `SieveErgodicSetup`
SpectralReduction — Phase 2.5 — Closing the ergodicity loop without external hypothesis
Tensor — CRT Tensor Factorization and Ruelle Factorization

Algebra PT.Algebra.* 1 module

PMAlgebra — PM algebra — the primorial-modular ring

Chemistry PT.CH.* 1 module

PhaseTransitionAlgebraic — PT_CH Phase Transition: Algebraic Identities (Tier A)

NashDeGiorgi PT.NashDeGiorgi.* 4 modules

GammaAtMu — `γ_p(μ)` for variable `μ` — extended threshold values
LemmaAFormal — Lemma A — analytical proof of $\gamma_p$ monotonicity in $\mu$
MainTheorems — Main theorems of `PT_NASH_DEGIORGI` (Z1, Z2, Z3, Z4)
Z1ActiveSet — Z1 — Eventually-exact convergence of the truncated sieve

root PT.root.* 2 modules

NashDeGiorgi — PT.NashDeGiorgi — umbrella module
PTGrandUnifiedTheorem — Persistence Theory — Grand Unified Theorem (Tier 1 capstone)

Why formalise?

A theorem proved on paper lives in the reader's trust. A kernel-verified theorem demands none: the Lean kernel is a roughly six-thousand-line program, reviewed by the community for over fifteen years, which accepts a declaration theorem X : P := proof only if proof constructs, type by type, a witness for P. Any short-cut, any hidden hypothesis, any "this is obvious" fails typechecking.

For Persistence Theory this discipline already had an immediate effect: while bringing up the T3Antidiagonal module, six concrete mistakes were caught (wrong Mathlib import path, a ring tactic that failed to close a goal, a noncomputable attribute missing on a real literal, ...) that no human reviewer had spotted. The source remains inspectable: every [THM] assertion in the paper has a formal witness pointable to the exact line.

Across the 196 modules under PT/, 195 are entirely sorry-free. The only remaining one is G3FisherUniqueness (Fisher metric uniqueness up to scale), a classical result already marked \leanExternal in the monograph. It is off PT's critical path.

Reproduce the verification

Install the Lean toolchain through elan, then:

git clone https://github.com/Igrekess/PersistenceTheory.git
cd PersistenceTheory/pt_lean
lake exe cache get      # ~1 GB of Mathlib oleans, ~5 min
lake build              # ~5 min cold, ~10 s cached

The Lean version is pinned by lean-toolchain, Mathlib by lake-manifest.json. No version juggling required.

Source code

Lean 4 formalisation

The critical path

Site theorems and their Lean modules

Full catalog by topic

Why formalise?

Reproduce the verification

`pt_lean/` repository

Detailed README

Annotated theorems

Lean 4 formalisation

The critical path

Site theorems and their Lean modules

Full catalog by topic

Why formalise?

Reproduce the verification

pt_lean/ repository

Detailed README

Annotated theorems

`pt_lean/` repository