| Claim | Paper | Lean | Chapter |
|---|---|---|---|
| η exists as IVT root of x³−x²−x−1; η>1; weight sequence w_k=η⁻ᵏ strictly antitone, →0
The amplitude-envelope foundation, §3.2 |
nbonacci_dnls_paper / paper_v4.tex 10.5281/zenodo.20075822 |
sorry-free TribonacciDNLS.lean — η_gt_one, η_pos, η_characteristic, w_pos, w_strictAnti, w_tendsto_zero |
chEta-tribonacci.html, ch-eta-dnls.html |
| IPR functional: scale-invariant, bounded in [1/N,1]; PoreSpace compact/finite-measure; tridiagonal Hamiltonian symmetric
Functional-analytic scaffolding, not the paper's headline result |
— (infrastructure, not a paper claim itself) | 1 disclosed sorry DNLSFoundations.lean — ipr_scale_invariant, hamMatrix_isSymm, poreSpace_isCompact proved; ipr_le_one depends on sum_sq_le_sq_sum_of_nonneg (sorry) |
ch-eta-dnls.html (implicit — the live IPR demo) |
| Differential nonlinear robustness: Fibonacci IPR drops ~57%, Tribonacci <5% at λ=1.5, T=50; long-time saturation ratio 1.04±0.04 at T~3×10⁵
This is the paper's actual headline claim |
paper_v4.tex §4 | not formalized DNLS_MeasureTheory_Roadmap.lean Tiers 2/4/5/8 sketch what a proof would need (discrete Harnack via ellipticity ratio 2 vs 4); Tiers 8.2/8.3/8.5 explicitly marked "STILL OPEN" / "remains numerical" in the roadmap's own text — honest, not silently claimed |
ch-eta-dnls.html |
| Fold-event lock-in: G⁶(hex)=33, saturating counter model | NPB §4 (lock-in prediction) | sorry-free FoldEvents.lean — stability_at_threshold, g6_hex_lockin, g6_hex_lockin_in_orbit |
none No chapter narrates this result yet |
| Claim | Paper | Lean | Chapter |
|---|---|---|---|
| Theorem 5.3 — the operators C,K,F,U do not commute; order-dependent
The abstract root all D2/D3/D4 domain claims specialize |
vol1-mathematics.html §5 | 1 disclosed sorry CatGT_PROOFS_COMPLETE.lean — NonCommutativity, boundary-discontinuity step left open |
vol1-mathematics.html §5 |
| ZSM-5 (C→K→F→U) suppresses aromatics — Selectivity = 0 | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md | sorry-free CatGT_PROOFS_COMPLETE.lean — ZSM5_SupportsAromatics |
ch-catgt-zeolite.html, ch18 |
| MCM-22 (C→F→K→U) permits aromatics, Selectivity > 0.2 (~0.35 simulated) | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md | 2 disclosed sorries CatGT_PROOFS_COMPLETE.lean — MCM22_PermitsAromatics, both numerical-integral gaps; roadmap Tiers 6-7 sketch a from-first-principles close (not yet mechanized) |
ch18 |
| Operator order determines selectivity [MAIN theorem, combines the two above] | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md §4.4 | genuine gap, not just sorry CatGT_PROOFS_COMPLETE.lean — shares one K between two branches needing K = two different concrete operators at once; flagged in the file's own header, not silently patched |
ch18 |
| D3 — enzyme biocatalysis extends Thm 5.3 to a third domain (branch multiplicity, concentration-tilted selection) | — (chapter-original derivation from Vol I Assumptions 2.2/2.5/2.6, not yet a standalone paper) | not formalized | ch19-enzyme-noncommutativity.html |
| D4 — SAF/biomass bridge domain (D2 zeolite + D3 enzyme in series) | — (chapter-original) | not formalized | ch20-saf-noncommutativity.html |
| Autophagy: mTOR as fold operator F, C→K→F→U in molecular biology | criticality_paper/ (dnls repo) | "0 sorry" per living-book.html's own card AutophagyDm3.lean (dnls/criticality_paper/) — not re-read this session; status taken from the chapter card's own claim, flagging for a real re-check rather than silently trusting it |
chA-autophagy.html |