Coverage summary
5Lean files
0Coq files
~48Lemmas, hand-checked
10sorry (open)
proved stated and proved in-file; independently re-verified this session by symbolic/numeric cross-check; NOT yet lake-built
sorry explicitly marked open, with a stated proof route
open / no content placeholder (e.g.
True) with no mathematical content claimed — honestly blocked (usually on missing Mathlib infrastructure)arithmetic resolved a flagged discrepancy that was independently re-derived and closed this session
Volume I files
ExistenceWellPosedness.lean
Vol. I §4 · Book I: Existence and Well-Posedness
Rewritten 2026-07-03 to remove vacuous tautologies (the original proved
only that Lean functions are functions). Now states real metric content:
compression genuinely contracts by
r*, and the composite
Φ=R∘K∘F∘C contracts when F, K, R are non-expansive.
The Banach fixed-point conclusion is correctly routed to Mathlib's
ContractingWith API rather than asserted.
| Lemma | Status | Notes |
|---|---|---|
| compression_contracts | proved | Independently re-verified numerically this session. |
| compression_strict | proved | Direct consequence of the above. |
| Phi_contracts | proved | Sound calc-chain, checked by hand. |
| Phi_wellPosed | sorry | Banach fixed point via ContractingWith.fixedPoint. |
| Phi_iterates_converge | sorry | Same witness as above, plus tendsto_iterate_fixedPoint. |
FiniteBranching.lean
Vol. I §5 · Book I: Finite Branching
Kept unchanged from the original draft — the audit found this file
already followed the correct discipline (honestly incomplete, not falsely
complete). Reference pattern the other four files were rewritten to match.
| Lemma | Status | Notes |
|---|---|---|
| analytic_zeros_isolated | sorry | Route via AnalyticOn.eq_zero_of_frequently_zero, contrapositive. |
| discrete_closed_in_compact_finite | sorry | Route via compactness + discrete topology → finite. |
| finiteBranching | sorry | Combines the two lemmas above. |
| branchingIndex | sorry | Depends on finiteBranching. |
Invariant75.lean
Vol. I §7.5 · Book I: Invariant 7.5 companion note
Rewritten 2026-07-03 after the audit found the original formalized a
different theorem (a generic Lyapunov-contraction inequality,
not the injectivity/chord-arc statement of §7.5). Now states and
proves the real theorem: condition (D) ⇒ injectivity, with the
Gerono lemniscate proved as the necessity witness. Zero
sorry
in this file — the one open geometric obligation (concrete
curvature ⇒ chord-arc constant) is correctly left as an abstract
hypothesis, not a claimed-and-failed proof.
| Lemma | Status | Notes |
|---|---|---|
| invariant_7_5_injective | proved | From ConditionD, an abstract hypothesis (concrete unfolding lives in the geometry file, not claimed here). |
| gerono_self_intersects | proved | γ(π/2)=γ(3π/2)=(0,0); independently confirmed numerically to float precision. |
| gerono_not_injOn | proved | Direct consequence. |
| gerono_fails_conditionD | proved | Contrapositive of invariant_7_5_injective. |
| cos_three_pi_div_two | proved | Addition-formula route independently confirmed symbolically. |
Volume II files
ContactHopf.lean
Vol. II §3 · Book II: Contact Hopf coefficient correction
Rewritten 2026-07-03 to remove a fabricated geometric justification (a
claimed "Reeb-direction projection" mechanism for the factor of 2, which
the session never derived). Replaced with the real algebra. The file then
flagged an apparent direction conflict between the coefficient correction
and the γ* correction — correctly refusing to guess —
which was independently re-derived and resolved this session (see
Book II for the full derivation): both directions are correct
simultaneously, since the coefficient sits in the denominator when
solving for the root.
| Lemma | Status | Notes |
|---|---|---|
| gammaStar_eq_two_mul_old | proved | Arithmetic identity. |
| linearization_erroneous_expansion | proved | ring identity; the honest locus of the factor of 2. |
| erroneous_root_is_exp | arithmetic resolved | Independently re-verified: 2·(e^z0·e^-z0)−2=0. |
| gammaStar_is_root | arithmetic resolved | Independently re-verified: confirms 2e^z0 solves the corrected equation. |
| contactHopf_bifurcation | sorry | The actual Hopf existence/uniqueness theorem — genuine open geometric content; no general Hopf theorem in Mathlib yet. |
dm³ toy model files
Dm3Arithmetic.lean
dm³ toy model V3 · three arithmetic corrections
Rewritten 2026-07-03. The original defined a plain exponential-decay flow
and a textbook
N(0,σ²) density — neither
matched the paper's actual corrected objects. Now states the real
Bernoulli-solution flow and the correctly-centered, correctly-coefficiented
stationary density, both independently re-verified this session.
| Lemma | Status | Notes |
|---|---|---|
| flowAux_ode | proved | Derivative independently re-verified symbolically — exact match. |
| flow_equilibrium_at_one | proved | Trivial arithmetic, confirmed. |
| μ_hopf_approx | proved | Numeric bound (1.55, 1.56) independently recomputed: 2r*=1.55188118. |
| ρ_peak_at_one | proved | Trivial, confirmed. |
| ρ_nonneg | proved | Standard positivity argument. |
| flow_zero | sorry | rpow coercion mechanics only — elementary, pending exact Mathlib lemma names. |
| flow_ode | sorry | ṙ=r−r³ derivative of the Bernoulli solution; route verified by hand this session, not yet machine-checked. |
| ρ_normalised | sorry | Normalization constant 2/(σ√π) independently re-integrated and confirmed correct; Gaussian integral lemma name pending. |
| ρ_is_stationary_of_dm3_flow | open / no content | Honestly blocked — no Fokker–Planck/SDE machinery in Mathlib4 yet. |
Coq
No Coq files exist in this project. All formal verification work to date is in Lean 4 / Mathlib4. This section is a placeholder in case that changes.
How this registry is maintained
A row is added only after the corresponding Lean file has been read in
full and every claim marked “proved” has been independently
re-derived — by symbolic computation, numeric cross-check, or both
— not merely re-read. sorry rows are never silently
closed; they move to proved
only after a real derivation is added to the file and re-verified here.
This page tracks code. For the theorem-level prose audit trail these files are ports of — including gaps found, counterexamples constructed, and citations corrected — see Book I and Book II.
Pablo Nogueira Grossi · G6 LLC, Newark NJ · ORCID 0009-0000-6496-2186