10.5281/zenodo.19117399, which is the concept DOI of
Principia Orthogona Volume I, a separate record).
The paper itself is the PDF on Zenodo; this page is a guide to it, not a copy.
How to read the tags
Every result in the paper carries one of three tags. Version 4 made the first one strict.
| Tag | Meaning in Version 4 |
|---|---|
| T | Kernel-checked. The Lean declaration named with the result is in a deposited
file, at a stated commit and Lean/Mathlib pin, and #print axioms reports only
propext, Classical.choice, Quot.sound. A (T) certifies the
Lean statement, not the prose around it. |
| S | A proof or proof sketch in the text, not kernel-checked — including results whose nearest Lean declaration does not state the result itself. |
| C | Conjecture. |
Before Version 4, (T) meant “proved without sorry in the AXLE engine”, and Part III widened it further to “or algebraically complete and ready for formalisation”. Under that reading a tag could point at a file that was never compiled, or at no declaration at all.
The four parts
Part I · Mathematical foundations
The operator sequence \(C \to K \to F \to U\) (compression, curvature, fold, unfolding) on a Riemannian manifold, under six stated assumptions; the Whitney \(A_1\)–\(A_3\) singularity classification; symplectic preservation for the fold map; a variational characterization of the unfolding; and the g-series lock-in threshold \(g = 33\). This is the material of Volume I, currently Version 7 (Zenodo 10.5281/zenodo.22084842).
| Result | Tag | Lean |
|---|---|---|
| Sequential consistency; singularity classification; symplectic preservation; variational characterization | S | — |
| g-series growth | T | nextLevel_layer_count_gt (PrincipiaVol1) |
| \(V(q)+2=(q-1)^2(q+2)\); \(V''(1)=6\) | T | V_factored, V_second_deriv_at_one (PrincipiaVol1) |
Part II · Contact realization
The passage to the contact 3-manifold \(M=\mathbb{R}^2_{>0}\times\mathbb{R}\) with
\(\alpha = dz - r^2\,d\theta\); Theorem A (contact realization of the fold), Theorem B
(the curvature threshold \(\kappa^*\) and the embodiment threshold \(\tau\) are equivalent),
the dm³ toy model, and Theorem C (singularity–bifurcation correspondence). This is the
material of Volume II, currently Version 5
(Zenodo 10.5281/zenodo.22117968), whose Lean file VolumeTwo.lean is kernel-checked at AXLE commit e44e8d1.
| Result | Tag | Note |
|---|---|---|
| Theorems A and B and their lemmas | S | Proof sketches. VolumeTwo.lean has declarations named after both, but
thm_A_contact_realization_fold concludes True and thm_B_threshold_equivalence holds by hypothesis; neither is cited. |
| Theorem C: four bifurcations onto three Whitney types | S, combinatorics T | Corrected in V4. V1–V3 said the bifurcations “correspond exactly” to \(A_1\)–\(A_3\). Two of them
(Contact Hopf, saddle-node) map to \(A_1\), so it is a surjection, not a bijection: thm_C_A1_surjective,
thm_C_not_bijective (VolumeTwo.lean). |
| Canonical invariants \((T^*,\mu_{\max},\tau)=(2\pi,-2,2)\), \(\varepsilon_0=1/3\), \(\kappa^*=\sqrt{7/9}\) | S | Retagged from (T) in V4. The cited declarations are kernel-checked but do not state the items:
dm3_basin_compact proves \([1/3,2]\) is compact, not \(\tau=2\). For \(\varepsilon_0\) the
checked content is arithmetic only — epsilon0_of_eq_third_iff:
\(2/(2(1+H)) = 1/3 \iff H = 2\); the bound \(H=2\) is not formalised. Properties of
\(\lambda(z)=\mu_{\max}(1-e^{-\beta z})\) are kernel-checked (eigenvalue_at_zero, eigenvalue_neg_pos_z,
eigenvalue_limit), as is \(\sqrt{4/1}=2\) (toyModel_tau); tau_eq_abs_mu_iff shows \(\tau=|\mu_{\max}|\)
holds only at \(|\mu_{\max}|=2\). |
| Contact normal form | S | Retagged from (T) in V4: no declaration states it. |
Part III · Seven proofs that \(\eta \approx 1.8393\) is the characteristic root
The dm³ fold recurrence \(w(k+3)=w(k+2)+w(k+1)+w(k)\) grows at the Tribonacci constant \(\eta\), the real root of \(x^3-x^2-x-1=0\). The paper gives seven arguments; each has a companion page.
- Operator algebra · S
Retagged from (T) in V4: algebraically complete, not formalised.
- Distribution theory · S
Retagged from (T) in V4: algebraically complete, not formalised.
- Whitney \(A_1\) catastrophe cascade · S
Recurrence coefficients rest on an admitted step,
whitneyFold_conditional. - Contact geometry · T in part
Existence, \(1<\eta<2\) and uniqueness in \((1,2)\) are kernel-checked for the constructed root:
η_characteristic,η_gt_one,η_lt_two,η_unique_in_Ioo(TribonacciMeasure.lean). Uniqueness is algebraic: \((x-\eta)\,[x(x-1)+\eta(\eta-1)+(x\eta-1)] = 0\). The cohomology count it also cites is (S): V1–V3 citedreeb_orbit_is_integral, which does not exist as a declaration. - Perron–Frobenius spectral theory · S
Retagged from (T) in V4: algebraically complete, not formalised.
- Certified numerical computation · S
Retagged from (T) in V4. V1–V3 cited
def eta := 1.839286755214161inAXLE_v8.1.lean, a decimal literal; V4 cites the root it locates toTribonacciMeasure.lean(\(T\)) and leaves the sixteen digits (S). - Fisher information geometry · S
Retagged from “(T) in part” in V4: no declaration states it.
“Seven independent proofs” is the paper’s phrase. Whether the seven are independent — rather than seven derivations sharing a hypothesis, such as the three-step traversal that selects \(n=3\) — is not examined in Version 4.
Part IV · Applications to nuclear matter
Confinement, hadronization and the onset of coherent structure in the quark–gluon plasma are modelled as iterated fold events under a conjectural effective contact form \(\alpha_{\mathrm{QCD}}\) C. Five falsifiable conditions are stated. The triple-alpha process is examined in the same conjectural register: the paper proves that no map reproducing its temperature sensitivity can be both parameter-free and derived from the contact form, and derives an Arrhenius factor only in a scoped local regime near the neutral point. Where the correspondence is analogy rather than derivation, the paper says so (for example, the link between \(g = 33\) and a nuclear multiplicity is labelled analogical). The invariants Part IV quotes (\(\mu_{\max}=-2\), \(\tau=2\), \(\varepsilon_0=1/3\)) are now tagged (S), following “Canonical invariants”.
The paper places itself in a programme of three lines, PoA + CatGT + TOGT. PoA is the four-deposit translational series prepared for the Princess of Asturias submission: the series overview and domain monographs on RNA switching and NGS, aminoglycoside riboswitches and microtubule curvature. CatGT is the self-trapping selectivity paper. Volume III, the Living Book — the “Mini-Beast” — carries the domain instantiations. It is published online and never closed: each teaching meeting, in which a doctoral researcher presents their work in English, adds a chapter.
Kernel-checked files (paper §23)
| File | Cited declarations | Check |
|---|---|---|
PrincipiaVol1.leanTOTOGT/vol1-proofs@be9a20b |
V_critical_at_one, V_second_deriv_at_one, V_factored, gronwall_radius,
epsilon0_of_two, epsilon0_of_eq_third_iff, contactCoeff_neg, basin_asymmetry,
noiseTolerance, closurePoints_stationary, nextLevel_layer_count_gt |
CI run #17: 82/82 (58 + 24) standard axioms, no sorryAxLean v4.14.0 |
AutophagyDm3_v2.leansame commit |
contactCoeff_neg, V_factored, gronwall_radius, basin_asymmetry,
dm3_basin_compact, contactForm_nondeg_scalar | |
TribonacciMeasure.leanin the V4 deposit |
η_characteristic, η_gt_one, η_lt_two, η_unique_of_char, η_unique_in_Ioo |
author’s run 2026-09-24: 5/5 standard axioms Lean v4.14.0 |
CatGT_Main.leanTOTOGT/io; CATGT V6 |
ipr_between_zero_and_one, helical_selectivity, criticalRadius_pos,
criticalRadius_antitone, selectivityFactor_eq |
23/23, v4.14.0 and v4.32.0 (CATGT V6) |
VolumeTwo.leanTOTOGT/AXLE@e44e8d1; Vol II V5 |
toyModel_tau, eigenvalue_at_zero, eigenvalue_neg_pos_z, eigenvalue_limit,
tau_eq_abs_mu_iff, thm_C_A1_surjective, thm_C_not_bijective |
19/19 pass the gate, Lean v4.14.0 (Vol II V5, App. A) |
Links: vol1-proofs@be9a20b ·
CI run #17 ·
TOTOGT/io. The V4 deposit’s verify.sh re-runs the first three in one environment.
Known gaps, stated rather than hidden
reeb_orbit_is_integral, a name that does not exist. Version 4 retags them (S). main_v7.lean,
DustyPlasma.lean and AXLE_v8.1.lean are no longer cited as verification.
UnfoldOp.stable_branch in PrincipiaVol1.lean holds at \(n = 0\) for every map. The file proves
this itself (unfold_stable_branch_is_vacuous), and no result in the paper depends on it. A repaired
form requiring \(n > 0\) is in TOTOGT/io Theorem53NonCommutativity.lean (commit 8cdd05f); it
states that image points are periodic, not that anything is stable or attracting.
#print axioms rules out sorry. It does not show that the Lean statement is the
claim the prose makes. helical_selectivity, for instance, is the implication
\(r^2 \le a^2J/\lambda \Rightarrow r \le r^*\) — square-root monotonicity — whatever the
surrounding text says about helical branches.
What changed from Version 3
- Theorem C corrected: a surjection, two-to-one at \(A_1\), not an exact correspondence.
- Every body (T) tag re-checked; those without a kernel-checked declaration are now (S).
- Bibliography brought to Volume I V7, Volume II V5 and the dm³ toy model V3; PoA defined and cited.
- Concept DOI corrected to
10.5281/zenodo.20682933. - Status-tag legend made strict (above).
- “Canonical invariants” retagged (T) → (S).
- “Proved in AXLE” now names
PrincipiaVol1.lean. - \(\eta\) cited to the constructed root in
TribonacciMeasure.lean, not to a decimal literal. - The verification table (“48+ proved” across undeposited files) now lists only deposited files, with commit, pin and axiom report.