Vérification formelle

Formalisation Lean 4

Trente théorèmes fondationnels de PT, vérifiés sans aucun sorry.

Le cœur arithmétique de la Théorie de la Persistance est entièrement reproduit dans Lean 4 + Mathlib. Le chemin critique $T_1 \to T_3 \to s = 1/2 \to T_2 \to L_0 \to T_7 \to W_7\text{-}1$ est kernel-vérifié bidirectionnellement : chaque étape est une preuve formelle dont l'exactitude est garantie par le noyau de Lean, et l'identité de spirale W7-1 admet désormais ses deux directions. Cent soixante modules secondaires couvrent l'écosystème environnant. Aucune affirmation [THM] du chapitre 1 n'est laissée à la charge du papier.

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

théorèmes nommés du chemin critique
kernel-vérifiés, 0 sorry
incluant W7-1 réciproque, T6b 4 axiomes, T2 spectral bridge

196

modules Lean au total
(8 sur le chemin critique
+ 188 dans l'écosystème)

~2 885

déclarations formelles
(théorèmes + lemmes + définitions
+ instances)

Le chemin critique

Tous les énoncés ci-dessous sont prouvés sans hypothèse externe à Mathlib : chaque étape ne dépend que des précédentes. La lecture de gauche à droite est exactement la dépendance logique vérifiée par le noyau Lean.

Transitions mod 3 interdites

→

Matrice antidiagonale

→

s = ½

Distribution stationnaire unique

→

α_cons = s² = ¼

→

Géométrique = max-entropie

→

μ* = 15

Point fixe unique

→

Mertens

Compactness borne

→

W7-1

Identité de spirale

Théorèmes du site et leur module Lean

Chaque théorème listé ci-dessous a une fiche dédiée sur le site, et un module Lean correspondant que l'on peut ouvrir directement sur le dépôt GitHub.

Théorème	Énoncé court	Module Lean	Statut
GFT	$\log_2 m = D_\mathrm{KL} + H$ — principe fondamental de la persistance.	PT.Information.GFTIdentity	kernel-vérifié, 0 sorry
L0	L’unique distribution sans-mémoire d’entropie maximale sur les écarts pairs.	PT.Information.L0MaxEntropy	kernel-vérifié, 0 sorry
T1	Le crible interdit deux résidus consécutifs identiques mod 3.	PT.Sieve.T1ForbiddenTransitions	kernel-vérifié, 0 sorry
T2	Identité spectrale exacte $\|\lambda_2(T_{30})\| = s^2 = 1/4$.	PT.Conservation.T2Alpha	kernel-vérifié, 0 sorry
T3	$T_3 = \mathrm{antidiag}(1,1)$ — la matrice mod 3 est purement off-diagonale.	PT.Sieve.T3Antidiagonal	kernel-vérifié, 0 sorry
T4	$\alpha_k \to 1/2$ quand la profondeur du crible $k \to \infty$.	PT.NumberTheory.T4MertensActivePrimes	kernel-vérifié, 0 sorry
T5	Après cristallisation de p = 2, le secteur réduit du crible admet un unique attracteur physique : $\mu^* = 3+5+7 = 15$.	PT.FixedPoint.T7MuStar	kernel-vérifié, 0 sorry
T6	$\sin^2 \theta_p = \delta_p (2 - \delta_p)$ — la trigonométrie émerge du crible.	PT.Holonomy.CyclicPhaseIdentity	kernel-vérifié, 0 sorry
N1	Les nombres premiers sont les uniques atomes du monoïde multiplicatif $(\mathbb{N}_{\geq 1}, \times)$.	PT.Sieve.N1AtomicUniqueness	kernel-vérifié, 0 sorry
N2	Le crible d’Ératosthène est l’unique crible multiplicatif auto-cohérent sur $\mathbb{N}_{\geq 2}$.	PT.Sieve.N2SelfCoherence	kernel-vérifié, 0 sorry
N3	$(\mathbb{N}_{\geq 1}, \times)$ est l’unique monoïde libre commutatif à factorisation unique avec atomes dénombrables.	PT.Sieve.N3aMinimalMonoid	kernel-vérifié, 0 sorry
N4	Dans l’ordre canonique du crible, $p = 3$ est le premier niveau dynamique. $p = 2$ joue un rôle structurellement distinct (info / anti-info).	PT.Sieve.N4DimensionCascade	kernel-vérifié, 0 sorry
BA5	À l’attracteur réduit $\mu^* = 15$, le couplage du crible est le produit $\prod_{p \in \{3,5,7\}} \sin^2\theta_p(q_+)$.	PT.Anomaly.BargmannBA5	kernel-vérifié, 0 sorry
G1	Sur le simplexe de crible avec structure CRT, $D_{KL}$ est l’unique divergence cohérente.	PT.Information.T6cG1Autonomous	kernel-vérifié, 0 sorry
G3	La métrique de Fisher est l’unique métrique riemannienne Markov-monotone sur le simplexe.	PT.Information.G3FisherUniqueness	kernel-vérifié, 0 sorry
Mertens	La fonction $M(x) - \log\log x$ est bornée — classique, importée dans la PT.	PT.NumberTheory.T5Mertens	scaffold
ActivePrime	Un premier $p$ est actif si et seulement si $\gamma_p > s = 1/2$ — l’ensemble actif est exactement $\{3,5,7\}$.	PT.Holonomy.ActivePrimeCriterion	kernel-vérifié, 0 sorry
Nc	$N_c = N_{\text{spatial}} = 3$ : unique solution entière de $(N_c+1)!/(N_c+3) = 2^{N_{\text{spatial}}-1}$.	PT.FixedPoint.T7MuStar	kernel-vérifié, 0 sorry
CRT	Le crible se factorise additivement : $\mathbb{Z}/P \cong \bigoplus_p \mathbb{Z}/p$. Les opérations à différents premiers commutent.	PT.Stochastic.CRTFactorizationT2	kernel-vérifié, 0 sorry

Les théorèmes T0, E, F, G, FisherKoide, FourierKoide et OS3 ne sont pas encore formalisés.

Catalogue complet par sujet

Au-delà du chemin critique et des théorèmes du site déjà présentés en haut de page, 188 modules supplémentaires (sur les 196 modules totaux du dépôt) couvrent l'écosystème environnant : variantes, raffinements, identités auxiliaires, structures algébriques. Chaque sujet est regroupé ci-dessous ; ouvre une section pour voir la liste détaillée. Chaque module pointe vers son fichier .lean sur GitHub.

Crible (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

Stochastique 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

Holonomie 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)

Point fixe 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)

Analyse PT.Analysis.* 1 module

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

Pont math/physique 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

Découplage CRT 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

Algèbre PT.Algebra.* 1 module

PMAlgebra — PM algebra — the primorial-modular ring

Chimie 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)

Pourquoi formaliser ?

Un théorème démontré sur papier vit dans la confiance du lecteur. Un théorème kernel-vérifié ne demande aucune confiance : le noyau de Lean est un programme d'environ 6 000 lignes, relu par la communauté depuis plus de quinze ans, qui n'accepte une déclaration theorem X : P := proof que si proof construit, type à type, une preuve de P. Tout court-circuit, toute hypothèse cachée, tout « c'est évident » fait échouer le typage.

Pour la Théorie de la Persistance, cette discipline a déjà eu un effet immédiat : lors de la mise en place du module T3Antidiagonal, six erreurs concrètes ont été détectées (mauvais chemin d'import Mathlib, tactique ring incapable de fermer un but, fonction noncomputable requise...) qu'aucun relecteur humain n'avait remarquées. Le code source reste consultable : chaque assertion [THM] du papier admet un témoin formel pointable à la ligne près.

Sur les 196 modules sous PT/, 195 sont entièrement sans sorry. Le seul module qui en contient encore un est G3FisherUniqueness (unicité à un facteur près de la métrique de Fisher), un résultat classique déjà signalé \leanExternal dans la monographie. Il n'est pas sur le chemin critique de PT.

Reproduire la vérification

Installer la chaîne d'outils Lean via elan, puis :

git clone https://github.com/Igrekess/PersistenceTheory.git
cd PersistenceTheory/pt_lean
lake exe cache get      # ~1 Go d'oleans Mathlib, ~5 min
lake build              # ~5 min à froid, ~10 s en chaud

La version de Lean est figée par lean-toolchain, Mathlib par lake-manifest.json. Aucun ajustement de version n'est nécessaire.

Code source

Formalisation Lean 4

Le chemin critique

Théorèmes du site et leur module Lean

Catalogue complet par sujet

Pourquoi formaliser ?

Reproduire la vérification

Dépôt `pt_lean/`

README détaillé

Théorèmes annotés

Formalisation Lean 4

Le chemin critique

Théorèmes du site et leur module Lean

Catalogue complet par sujet

Pourquoi formaliser ?

Reproduire la vérification

Dépôt pt_lean/

README détaillé

Théorèmes annotés

Dépôt `pt_lean/`