Table of Contents

Abstract Preface 1 · Introduction 1.1 The Problem: From Folds to Dissipation 1.2 Role of the dm³ Toy Model 1.3 Main Results A · B · C 1.4 Standing Assumptions 2 · Contact Realization of the Fold 2.1 From Symplectic to Contact 2.2 The Fold as Contact Discontinuity 2.3 Contact Normal Form 2.4 Correspondence Table (Theorem A) 3 · Equivalence of κ* and τ 3.1 Geometric → Stochastic 3.2 Stochastic → Geometric 3.3 Theorem B 4 · Explicit Verification 4.3 The Exact Equations 4.4 Threshold Values 4.5 Contact Normal Form 4.6 Stability Radius ε₀ = 1/3 5 · Singularity–Bifurcation Correspondence 6 · Discussion Appendix A · Lean 4 Status References
← Volume I: Mathematics → Toy Model: SIAM Paper → Interactive Dashboard
Principia Orthogona · Volume II · Version V5 · August 2026
C K F U

Contact Realization of
Generative Transitions

Fold–contact correspondence · Threshold equivalence κ* ↔ τ · Singularity–bifurcation correspondence
Pablo Nogueira Grossi · G6 LLC · Newark, New Jersey, USA
ORCID: 0009-0000-6496-2186 · pgrossi888@outlook.com
DOI 10.5281/zenodo.22117968 Lean 4 · 8 proved 4 open sorry CC BY-NC-ND 4.0 MSC 37C10 · 53D10 · 58K05 · 37H10
Theorem A
Contact Realization of the Fold
The fold operator F is the pre-contact limit of the dm³ operator \(A_{\mathrm{dm^3}}\). The distributional impulse \(p^+\!-\!p^-=\mu\mathbf{n}\) corresponds to \(H_{\mathrm{diss}}\) in the \(\beta\to\infty\) limit. sorry ★★★★
Theorem B
Threshold Equivalence
\(|\kappa|\uparrow\kappa^*\;\Leftrightarrow\;\mu_{\max}<0\;\Leftrightarrow\;\tau\in(0,\infty)\). The curvature threshold and embodiment threshold are two names for the same event. sorry ★★★★★
Theorem C
Singularity–Bifurcation
The four dm³ bifurcations (Hopf, saddle-node, Neimark–Sacker, slow-fast) correspond surjectively to Whitney \(A_1\)–\(A_3\) types; Hopf and saddle-node share the \(A_1\) preimage, so the map is two-to-one there and injective on \(A_2\), \(A_3\). proved ✓ — NS row: [OPEN] OP-NS. The bare dm³ ODE cannot produce it: \(J(z)\) is triangular with real eigenvalues at every \(z\), and NS needs a complex pair. The \(D_6\)-equivariant DNLS ring has exactly that structure — degenerate eigenspaces carrying the 2-D irreps of \(D_6\) — so the row is a claim about the DNLS extension, not about the toy model (§5.3, V5)
Abstract

This volume is the second in the Principia Orthogona series. Volume I developed the singularity-theoretic and variational foundations of generative transitions: the operator sequence \(C \to K \to F \to U\), the curvature threshold \(\kappa^*\), the Whitney \(A_1\)–\(A_3\) singularity classification, and a symplectic preservation theorem for the fold map. The present volume constructs the explicit contact-geometric realization of those foundations.

Three main results: (A) a precise correspondence between the geometric fold operator \(F\) and the dm³ contact Hamiltonian dissipation \(H_{\mathrm{diss}}\); (B) equivalence of the curvature threshold \(\kappa^*\) and the embodiment threshold \(\tau\), with explicit values \(\tau=2\), \(\varepsilon_0=1/3\) verified in the dm³ toy model; (C) a bifurcation analysis showing that the four dm³ bifurcations correspond surjectively to the Whitney \(A_1\)–\(A_3\) singularity types, two-to-one on \(A_1\). Version V5 regenerates Appendix A from the Lean file (six of V4’s twelve entries named declarations that have never existed), restates result (C) as a surjection, corrects the Lean file path, and adds §5.3 on the \(D_6\)-equivariant DNLS results. Version V4 corrected the Contact Hopf bifurcation point in §5 (\(\gamma^* = e^{z_0} \to 2e^{z_0}\), propagated from the dm³ toy model V3 erratum). Version V3 added the certified inner-basin boundary \(r^* = 0.77594058\) (§4.7). Version 2a added: Lean 4 formal proof skeleton (VolumeTwo.lean), fully-reproducible figures (figures.py, exact §4.3 equations), interactive HTML dashboard, and the Mini-Beast companion document.

Dedicated to my children Vic (R.I.P.), Giulia, Alice (R.I.P.), Sarah (R.I.P.), and David. Once tiny, always strong.
PPreface
Volume II · Contact Realization of Generative Transitions

Volume I established that generative transitions are localised geometric events classified by the Whitney \(A_1\)–\(A_3\) hierarchy. The fold operator \(F\) was shown to act as a symplectic canonical transformation on \(T^*X\), and the full transition \(G = U \circ F \circ K \circ C\) was shown to be a piecewise-smooth symplectic map. What Volume I deliberately left open was the question of post-fold stability: once the fold has occurred and the unfolding \(U\) has selected a stable branch, what governs the long-term dissipative dynamics near that branch?

The Hamiltonian framework of Volume I cannot answer this question: Liouville's theorem forbids attractors in symplectic systems on compact manifolds. The answer is contact geometry. The contact manifold \(M = X \times \mathbb{R}\) with contact form \(\alpha = dz - \lambda\) provides the correct geometric setting for dissipative dynamics with limit cycle attractors, stochastic stability, and variational structure.

The central results are: a precise correspondence between the geometric fold operator \(F\) and the dm³ contact Hamiltonian dissipation (§2); a theorem establishing the equivalence of the curvature threshold \(\kappa^*\) and the embodiment threshold \(\tau\) (§3); explicit verification in the dm³ toy model (§4); and a bifurcation analysis (§5). Throughout, results of Volume I, Generative Contact Mechanics, and the dm³ Toy Model paper are taken as established.

1Introduction
1.1 The Problem: From Geometric Folds to Dissipative Dynamics

Volume I established that generative transitions are classified by the Whitney \(A_1\)–\(A_3\) hierarchy. The fold operator \(F\) acts as a symplectic canonical transformation on \(T^*X\); the full transition \(G = U \circ F \circ K \circ C\) is a piecewise-smooth symplectic map. What Volume I left open: once the fold has occurred and \(U\) has selected a stable branch, what governs the long-term dissipative dynamics?

The Hamiltonian framework of Volume I cannot answer this: Liouville's theorem forbids attractors in symplectic systems on compact manifolds. The answer is contact geometry. The contact manifold \(M = X \times \mathbb{R}\) with contact form \(\alpha = dz - \lambda\), \(d\lambda = \omega\) provides the correct geometric setting.

1.2 Role of the dm³ Toy Model

The dm³ Toy Model [3] serves as a complete, explicit realization of the abstract contact-geometric framework and as the bridge certifying the realizability of the geometric fold theory of Volume I. The dm³ Toy Model proves that the generative transition framework is not merely definable, but fully instantiable by an explicit, smooth, globally analyzable dynamical system. Its role is logical, not empirical. See also the companion SIAM paper → and interactive dashboard →.

1.3 Main Results
SORRY ★★★★ Theorem A · Contact Realization of the Fold

The fold operator \(F\) of Volume I is the piecewise-smooth, pre-contact limit of the dm³ operator \(A_{\mathrm{dm^3}} = \varphi^{T^*/4}\) of [2]. Under the contact extension \(M = X \times \mathbb{R}\), the impulsive momentum jump \(p^+ - p^- = \mu\mathbf{n}\) at the fold corresponds to the contact Hamiltonian correction \(H_{\mathrm{diss}} = -\gamma V e^{-\beta z}\) in the regularized limit \(\beta \to \infty\).

SORRY ★★★★★ Theorem B · Threshold Equivalence

\[|\kappa|\uparrow\kappa^* \;\Longleftrightarrow\; \mu_{\max} < 0 \;\Longleftrightarrow\; \tau = \sqrt{c/\kappa_{\mathrm{noise}}} \in (0, \infty).\]

The curvature threshold \(\kappa^*\) and the embodiment threshold \(\tau\) are two parameterizations of the same event: the onset of transverse stability in the post-fold dissipative system.

PROVED ✓ Theorem C · Singularity–Bifurcation Correspondence

The four bifurcations of the dm³ toy model [3] correspond to the Whitney singularity types of Volume I under the projection \(M = S \times \mathbb{R} \to S\). The correspondence is surjective, and injective away from \(A_1\): contact Hopf and saddle-node both arise from rank-1 loss in the radial direction and share the \(A_1\) type, so four bifurcations map onto three Whitney types, two-to-one at \(A_1\). It is not a bijection, and cannot be.

1.4 Standing Assumptions
Assumption 1.1 · Volume I Framework

The operator sequence \(C \to K \to F \to U\), the threshold \(\kappa^*\), and all results of [1] hold.

Assumption 1.2 · dm³ Framework

The dm³ system, contact manifold \(M = S \times \mathbb{R}\), and all results of [2, 3] hold.

2Contact Realization of the Fold Operator
2.1 From Hamiltonian Phase Space to Contact Extension

In Volume I, the fold is realized in \(T^*X\) as a symplectic discontinuity. At fold point \(s_0\):

\[ p(s_0^+) - p(s_0^-) = \mu\,\mathbf{n}(s_0), \]

generated by \(S(\gamma) = \mu\,\Theta(|\kappa(\gamma)| - \kappa^*)\) ([1], §12). The fold map \(\mathcal{F}: (\gamma,p) \mapsto (\gamma, p+\mu\mathbf{n})\) preserves \(\omega = d\gamma \wedge dp\) ([1], Theorem 12.1). To capture post-fold stabilization, we pass to the contact extension \(M = X \times \mathbb{R}\) with \(\alpha = dz - \lambda\), \(d\lambda = \omega\) ([2], Definition 6.1).

2.2 The Fold as a Contact Discontinuity
Proposition 2.1 · Regularization of the Fold Generator

The contact dissipation \(H_{\mathrm{diss}}(x,z) = -\gamma V(x)e^{-\beta z}\) is a smooth regularization of \(S(\gamma) = \mu\,\Theta(|\kappa(\gamma)| - \kappa^*)\): as \(\beta \to \infty\) and \(z \to 0^+\), the correction \(-\gamma \nabla V e^{-\beta z}\) concentrates near \(\Gamma = \{V=0\}\) and mimics the threshold activation of \(\Theta\) at \(\kappa = \kappa^*\).

Structural properties: (i) \(H_{\mathrm{diss}}|_\Gamma = 0\); (ii) off \(\Gamma\): \(H_{\mathrm{diss}} < 0\); (iii) \(e^{-\beta z}\) weakens dissipation as action accumulates — the orbit earns its stability.

2.3 Relation to the dm³ Contact Normal Form

By [2] (Theorem C), every dm³ system near \(\Gamma\) is locally contact-diffeomorphic to the normal form:

\[ \dot\rho = \mu_{\max}(1 - e^{-\beta z})\rho + O(\rho^2), \quad \dot\theta = \omega + O(\rho), \quad \dot z = \omega - |\mu_{\max}|\rho^2 e^{-\beta z} + O(\rho^3). \]
2.4 Correspondence Table (proves Theorem A)
Volume I (geometric)GCM / dm³ (contact)
Curvature threshold \(\kappa^*\)Onset of transverse contraction
Fold impulse \(p^+ - p^- = \mu\mathbf{n}\)Contact correction \(H_{\mathrm{diss}} = -\gamma V e^{-\beta z}\)
Rank-1 Jacobian lossDissipative contact normal form
Unfolding \(U\)Gradient flow to \(\Gamma\)
Distributional generator \(S\)Regularized \(H_{\mathrm{diss}}\) (Prop. 2.1)

Theorem A is structural: the fold and the contact correction are two descriptions of the same event at different levels of regularization. The formal proof is open. thm_A_contact_realization_fold in VolumeTwo.lean states the hypotheses and carries the conclusion True as an explicit placeholder; the distributional convergence of \(e^{-\beta z}\) to \(\Theta\) as \(\beta \to \infty\) is not formalised.

3Equivalence of κ* and τ (Theorem B)
3.1 Geometric Threshold Implies Stochastic Threshold
PROVED Lemma 3.1 · Fold activation produces hyperbolicity

If \(K\) drives curvature to \(\kappa^*\), \(F\) is rank-1, and \(U\) selects a nondegenerate branch, then \(\Gamma\) is hyperbolic with \(\mu_{\max} < 0\) and \(\dot V \leq -cV\) for some \(c > 0\).

Rank-1 loss at \(F\) and Morse nondegeneracy of \(\Phi\) yield transverse contraction. Floquet theory gives \(\mu_{\max} < 0\).

SORRY ★★★★★ Theorem 3.2 · Geometric implies stochastic threshold

Under Lemma 3.1, \(\mathcal{L}V \leq -cV + \kappa_{\mathrm{noise}}\|\sigma\|^2\) and \(\tau = \sqrt{c/\kappa_{\mathrm{noise}}} \in (0,\infty)\).

\(\dot V \leq -cV\) plus the Itô correction \(\frac{1}{2}\|\sigma\|^2 \|\mathrm{Hess}\,V\|\) gives \(\mathcal{L}V \leq -cV + \kappa_{\mathrm{noise}}\|\sigma\|^2\) with \(\kappa_{\mathrm{noise}} = \frac{1}{2}\sup\|\mathrm{Hess}\,V\|\). Then \(\tau = \sqrt{c/\kappa_{\mathrm{noise}}} > 0\). (Proof requires Floquet theory + SDE stability — the 5-star sorry.)

3.2 Stochastic Threshold Implies Geometric Threshold
PROVED Lemma 3.3 · Finite τ implies transverse contraction

If \(\mathcal{L}V \leq -cV + \kappa_{\mathrm{noise}}\|\sigma\|^2\) with \(c > 0\), then \(\mu_{\max} < 0\) and \(\dot V \leq -cV\) near \(\Gamma\).

SORRY ★★★★★ Theorem 3.4 · Stochastic implies geometric threshold

If \(\tau \in (0,\infty)\), then the trajectory must have crossed \(\kappa^*\) and undergone a rank-1 fold.

By Lemma 3.3, \(\mu_{\max} < 0\), so a hyperbolic attracting cycle exists. Suppose \(|\kappa| < \kappa^*\) everywhere. Then [1] (Invariant 7.5, unconditional folding corollary) gives: below threshold no rank-1 fold occurs, hence no fold-generated attracting cycle. Contradiction.

V6 dependency note: this backward direction uses only the unconditional folding part of Invariant 7.5, so it needs no displacement condition (D). The unqualified global-injectivity form (previously cited here as "Invariant I5") is false without (D) — witnessed by the Gerono lemniscate — but Theorem 3.4, and therefore Theorem B (3.5), do not depend on it. Statements unchanged; citation narrowed.

3.3 The Equivalence Theorem
SORRY ★★★★★ Theorem 3.5 · Threshold Equivalence (Theorem B)

\[ |\kappa|\uparrow\kappa^* \;\Longleftrightarrow\; \mu_{\max} < 0 \;\Longleftrightarrow\; \tau \in (0,\infty). \]

The curvature threshold \(\kappa^*\) is the geometric precursor of \(\tau\): curvature accumulation creates the conditions under which stochastic stability becomes meaningful.

Forward: Theorem 3.2. Backward: Theorem 3.4. Middle chain: \(\tau > 0 \Leftrightarrow c > 0 \Leftrightarrow \mu_{\max} < 0\) (Lemma 3.3). Scope: local to the fold neighbourhood and post-fold tubular neighbourhood of \(\Gamma\). Full proof requires Floquet theory + SDE regularity, and is not formalised: thm_B_threshold_equivalence in VolumeTwo.lean establishes only the middle⇔right link, and does so from assumptions on both sides.

Figure 2 · Theorem B — Threshold Equivalence Chain
κ* ↔ μ_max < 0 ↔ τ ∈ (0,∞)
Panel A: curvature ratio κ/κ* (normalised). Panel B: effective contraction rate μ_eff(z) = −2(1−e^{−z}) approaching μ_max = −2. Panel C: embodiment threshold τ = √(c/κ_noise); dm³ toy model: c=4, κ_noise=1, τ=2.
4Explicit Verification in the dm³ Toy Model
Theorem 4.1 · Verification of the Framework by the dm³ Toy Model

There exists an explicit smooth dynamical system on a contact manifold — the dm³ toy model — in which all of the following hold by direct computation: (1) all eight dm³ axioms satisfied simultaneously; (2) explicit contact structure \(\alpha = dz - r^2 d\theta\); (3) contact normal form with \((\mu_{\max}, \omega, \beta) = (-2, 1, 1)\); (4) operator algebra closure; (5) stochastic stability with \(\tau = 2\); (6) global dynamics: attractor \(\Gamma_{12}\), four predicted bifurcations.

4.3 The Exact Equations

On \(M = \mathbb{R}^2_{>0} \times \mathbb{R}\) with polar coordinates \((r, \theta, z)\) and contact form \(\alpha = dz - r^2 d\theta\):

\[ \dot r = r(1 - r^2) + 2(r-1)e^{-z}, \qquad \dot\theta = 1, \qquad \dot z = r^2 - 2(r-1)^2 e^{-z}. \tag{4.1–4.3} \]

Limit cycle: \(\Gamma = \{r = 1\}\), period \(T^* = 2\pi\). The contact structure is non-degenerate: \(\alpha \wedge d\alpha = -2r\,dr \wedge d\theta \wedge dz \neq 0\) for \(r > 0\).

Figure 1 · Phase Portrait — Exact dm³ Equations §4.3
RK4 integrator · exact equations 4.1–4.3
Left: phase portrait — coloured curves converge to Γ = {r=1} (gold). Blue = converging; red = escaping (r < ε₀ = 1/3). Right: transverse eigenvalue λ(z) = −2(1−e^{−z}): λ(0)=0 (neutral, pre-embodiment), λ(z)<0 for z>0 (attracting).
4.4 Threshold Values
PROVED Proposition 4.2 · Explicit threshold values

\(\mu_{\max} = -2\), \(\kappa_{\mathrm{noise}} = 1\), \(\tau = 2\). Verified by norm_num in Lean 4.

The transverse eigenvalue \(\lambda(z) = -2(1 - e^{-z})\) satisfies: \(\lambda(0) = 0\) (neutral, pre-embodiment); \(\lambda(z) < 0\) for \(z > 0\) (attracting, post-embodiment); \(\lambda(z) \to -2\) as \(z \to \infty\) (full dm³ rate).

Linearize at \(r = 1\): \(\dot\rho = -2(1-e^{-z})\rho + O(\rho^2)\). Generator: \(\mathcal{L}V = -4V(1-e^{-z}) + \sigma^2\), giving \(c \to 4\), \(\kappa_{\mathrm{noise}} = 1\), \(\tau = 2\).

The neutral stability at \(z = 0\) is the mathematical content of the embodiment threshold: the orbit earns its stability by accumulating action. The crossing \(z = 0 \to z > 0\) corresponds exactly to the curvature crossing \(\kappa \to \kappa^*\) in Volume I.

4.5 Contact Normal Form
PROVED Proposition 4.3 · Contact Normal Form

In coordinates \((\rho, \theta, z)\) with \(\rho = r - 1\), the system takes the contact normal form of [2] (Theorem C) with \((\mu_{\max}, \omega, \beta) = (-2, 1, 1)\):

\[ \dot\rho = -2(1-e^{-z})\rho + O(\rho^2), \quad \dot\theta = 1 + O(\rho), \quad \dot z = 1 - 2\rho^2 e^{-z} + O(\rho^3). \]
4.6 Stability Radius
PROVED Proposition 4.4 · Stability Radius ε₀ = 1/3

\[ \varepsilon_0 = \frac{|\mu_{\max}|}{2(1 + \sup_\Gamma\|\mathrm{Hess}\,V\|)} = \frac{2}{2(1+2)} = \frac{1}{3}. \]

The basin asymmetry — \(\varepsilon_0 = 1/3\) is established for the outer basin \(\{r > r_{\mathrm{att}}\}\) only. The inner basin is asymmetric: trajectories from \(r_0 \in (2/3,\, r^*)\) lie inside the Gronwall ball and still escape to \(r \to 0\). The boundary \(r^* = 0.77594058\) is certified numerically by certify_rstar.py (DOP853, rtol 1e-12, atol 1e-14, bisection 1e-7), giving \(\varepsilon_0 = 1/3 < 2/3 < r^* \approx 0.776 < \kappa^* = \sqrt{7/9} \approx 0.882 < 1\). A numerical certificate is not a proof: no Lean declaration for this obligation exists.

5Singularity–Bifurcation Correspondence (Theorem C)

From [3] (Theorem C), the dm³ toy model exhibits four bifurcations: (i) contact Hopf at \(\gamma = 2e^{z_0}\): limit cycle loses stability, new cycle bifurcates (corrected in V4; the earlier \(\gamma^* = e^{z_0}\) carried a spurious factor of 2 in the linearized transverse eigenvalue, and the canonical case \(\gamma = 2\) used throughout matches the corrected value at \(z_0 = 0\)); (ii) saddle-node at \(\eta \approx 0.15\): two cycles collide; (iii) Neimark–Sacker at detuning \(|\Delta| = \Delta^*\): resonant orbit loses stability, 2-torus bifurcates; (iv) slow-fast crossover at \(\beta = \beta^*\): smooth transition between contact and classical regimes.

PROVED ✓ (A₁, A₃ rows) · [MODEL] (A₂/NS row — 2026-08-07) Proposition 5.1 · Singularity–Bifurcation Correspondence

Under projection \(M = S \times \mathbb{R} \to S\): \(A_1\) (codim 0) \(\leftrightarrow\) Contact Hopf + Saddle-node; \(A_2\) (codim 1) \(\leftrightarrow\) Neimark–Sacker [MODEL — see correction below]; \(A_3\) (codim 2) \(\leftrightarrow\) Slow-fast crossover.

Higher singularities excluded: in Volume I by the Morse condition; in [2] by contact normal form rigidity (Theorem C). Proves Theorem C for the A₁ and A₃ rows.

Correction notice (2026-08-07): The A₂ ↔ NS correspondence is [MODEL], not proved. The bare dm³ ODE linearises to a triangular 2×2 Jacobian J(z) = [[−2(1−e−z), 0], [2, 0]] with only real eigenvalues at every z — verified by direct computation. A Neimark–Sacker bifurcation requires a complex-conjugate eigenvalue pair, which is absent from the 3-equation system. The NS mechanism is the modulational instability of the DNLS amplitude equation (J hopping term, threshold λ_c = −2J/|A|²), correctly identified by the "2nd angular direction / detuning Δ" language in the table but not derivable from (r,θ,z) alone. [OPEN]

Whitney TypeCodimdm³ BifurcationMechanism
\(A_1\) fold0Contact Hopf (H)Rank-1 loss, radial direction
\(A_1\) fold0Saddle-node (SN)Rank-1 loss, radial collision
\(A_2\) cusp1Neimark–Sacker (NS)Rank-1, 2nd angular direction
\(A_3\) swallowtail2Slow-fast crossover (SF)Rank-1, 3rd-order \(z\)-change

\(A_1\) has two dm³ preimages (both from rank-1 loss in one transverse direction). Table 2 proves Theorem C.

Figure 3 · Bifurcation Diagram — Four Bifurcation Types
γ-axis: fold depth parameter · teal = stable branch r* = 1
H = Contact Hopf (A₁), SN = Saddle-node (A₁), NS = Neimark–Sacker (A₂), SF = Slow-fast (A₃). Whitney correspondence shown at right.
6Discussion
6.1 Summary

(1) The fold operator \(F\) is the geometric precursor of the dm³ contact Hamiltonian \(H_{\mathrm{diss}}\); the distributional generator \(S\) is regularized by \(H_{\mathrm{diss}}\) in the limiting sense of Proposition 2.1 (Theorem A).

(2) \(\kappa^*\) and \(\tau\) are equivalent: each is finite and positive if and only if the other is, both detecting the onset of transverse stability (Theorem B).

(3) The four dm³ bifurcations correspond to Whitney \(A_1\)–\(A_3\) types, completing the singularity-theoretic classification of the toy model dynamics (Theorem C).

6.2 Role in the G-Series

The Principia Orthogona series is a spiral, not a ladder. Each volume is a complete orbit — a full turn around the fixed point. \(G\) applied five times is \(G^5\) = Complete Completeness. \(G^6\) is still open (2026).

G-Level / VolumeCore ConceptFixed Point
G¹ / Vol. IAbstract Operator AlgebraOrthogonal operator
G² / Vol. II (this)Contact Geometry, g₃₃ = 33Contact fixed point
G³ / Vol. IIIBiological InstantiationsLiving form
G⁴ / Vol. IVGTCT T1, IMPATemporal contact
G⁵ / Vol. V + AXLEBanach FPT, formal proofComplete Completeness
G⁶ / Issue 6χ(H*(X⁶)) = 33 ∀nOpen — 2026
6.3 Open Problems

Global Equivalence. Theorem B is local. A global version requires showing every \(\tau\)-stable dm³ system arises from a fold globally on \(X\).

Higher Resonances. Systematic treatment of \(k:m\) correspondence between higher \(A_k\) singularities and higher resonances.

Basin Asymmetry (AXLE Issue #13). \(\varepsilon_0 = 1/3\) is established for the outer basin only. The inner boundary r* = 0.77594058 is certified numerically (V3); the formal proof is open, and no Lean declaration for it exists in VolumeTwo.lean.

Figure 5 · Coherence Bridge — Six Application Domains
All domains share the same contact normal form structure (Theorem 5.4 Mini-Beast)
Rows: six domains. Columns: contact normal form parameters (μ_max, ω, β, κ*). Values from Mini-Beast p. 26 (exact). Colour encodes parameter value normalised to [0,1].
ALean 4 Formal Verification Status

The Lean lives at AXLE/PrincipiaOrthogona_v2/VolumeTwo.lean. This table is generated from that file, not written alongside it. Reproduce with:

git clone https://github.com/TOTOGT/AXLE && cd AXLE bash tools/verify-vol2/run.sh

That builds the PrincipiaVol2 target at Lean v4.14.0, asks the kernel for the axiom dependencies of all nineteen declarations, and refuses on sorryAx or on any axiom outside {propext, Classical.choice, Quot.sound}. All nineteen pass, and two depend on no axioms at all.

The state described here is AXLE commit e44e8d1 — pinned to a commit rather than a branch, so it resolves to what was checked when this was written.

Passing that gate is necessary and not sufficient. A theorem whose conclusion is True, or whose hypotheses already contain its conclusion, is a true theorem and reports clean axioms. Three rows below are marked for exactly that reason, and the marks are the point of the table.

Theorem / LemmaLean NameStatusNotes
τ > 0 (Thm 3.2)embodimentThreshold_pos✓ provedsqrt_pos_of_pos
τ = 2 (Prop. 4.2)toyModel_tau✓ provedReal.sqrt_sq
λ(0) = 0 (Prop. 4.2)eigenvalue_at_zero✓ provedsimp
λ(z) < 0 for z > 0eigenvalue_neg_pos_z✓ provedReal.exp_lt_exp
λ(z) → μmaxeigenvalue_limit✓ provedconst_mul_atTop_of_neg, tendsto_exp_atBot
Thm 3.3 stability certificatevol2_contact_Theorem_3_3✓ provedconjunction of the two preceding rows
ε0 = 1/3 (§4.6)toyModel_epsilon0✓ provednorm_num
NJ|Γ = 0 (Thm 15.2, Level 1)Theorem_15_2_integrability✓ proveddimension count on a 1-dimensional tangent space
alternating m-form vanishes when m > dimalternating_vanishes_beyond_dim✓ provedmap_linearDependent
Thm C — unique preimages of A₂, A₃thm_C_singularity_bijection✓ provedthe name overstates it: no surjectivity conjunct, and the map is not a bijection
A₁ surjectivitythm_C_A1_surjective✓ proved (V5)closes a row V4 listed as proved against a name that existed nowhere. No axioms.
the map is not a bijectionthm_C_not_bijective✓ proved (V5)contact Hopf and saddle-node share the A₁ preimage, so injectivity fails. No axioms.
Thm A — correction vanishes off the foldthm_A_regularization_pointwise✓ proved (V5)the pointwise skeleton of the distributional claim
Thm A — correction constant on the foldthm_A_regularization_at_fold✓ proved (V5)the other half: it does not move with β at z = 0
τ = |μ| iff |μ| = 2tau_eq_abs_mu_iff✓ proved (V5)the toyModel_tau docstring caveat, now a theorem: τ = |μmax| is a property of the canonical value, not an identity
ε0 = 1/3, Waddington readingepsilon_zero_waddingtonduplicatestatement identical to toyModel_epsilon0; proof is := toyModel_epsilon0
μmax + τ = 0entropy_lyapunov_duality⚠ arithmeticreduces to −2 + 2 = 0; c = 4 is supplied by hand, not derived from μmax
Thm B — μmax < 0 ⇔ τ > 0thm_B_threshold_equivalence⚠ trivialboth branches discard the hypothesis; μmax < 0 is a field of DM3System, so each side is independently true
Thm A (full)thm_A_contact_realization_fold⚠ placeholder ★★★★conclusion is True. Not a sorry — so no axiom check can flag it. Distribution theory unformalised.
Thm B (full chain |κ| ↑ κ*)⚠ open ★★★★★no declaration; proved at the prose level in §3.3 only. Floquet + SDE.
Gronwall asymmetry, r* = 0.77594058⚠ open ★★★ Issue #13no declaration; numerical certificate only
NJ|ξ = 0 (Level 2d)— (OP4)⚠ open ★★★★not yet statable: NJ needs Lie brackets of vector fields
NJ|M = 0 (Level 2d+t)— (OP5)⚠ open ★★★★depends on OP4
-- lambda(z) < 0 for z > 0 (proved, no sorry, kernel-checked) theorem eigenvalue_neg_pos_z (sys : DM3System) (z : ) (hz : 0 < z) : transverseEigenvalue sys z < 0 := by unfold transverseEigenvalue apply mul_neg_of_neg_of_pos sys.mu_neg have hbz : -sys.beta * z < 0 := by nlinarith [sys.beta_pos] have hexp : Real.exp (-sys.beta * z) < Real.exp 0 := Real.exp_lt_exp.mpr hbz rw [Real.exp_zero] at hexp linarith

Full source: github.com/TOTOGT/AXLE · PrincipiaOrthogona_v2/VolumeTwo.lean · verifier tools/verify-vol2/run.sh

References
  1. [1]P. Nogueira Grossi, Principia Orthogona, Volume I: The Mathematics of Generative Transitions, Version 4, G6 LLC, 2026. vol1-mathematics.html · Zenodo 10.5281/zenodo.21146416 (v6, current version). The April 2026 Second Edition is retained at book1/vol1-mathematics.html; it is the only copy carrying the note on “orthogenesis.”
  2. [2]P. Nogueira Grossi, Generative Contact Mechanics, submitted to J. Geom. Mech., 2026. Zenodo 19122168
  3. [3]P. Nogueira Grossi, The dm³ Operator: Explicit Toy Model and Global Dynamical Analysis, submitted to SIAM J. Appl. Dyn. Syst., 2026. vol2-toymodel.html · Zenodo 21147306 (V3, latest)
  4. [4]V.I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed. Springer, 1989.
  5. [5]A. Bravetti, Contact Hamiltonian mechanics, Ann. Phys. 376 (2017), 17–39.
  6. [6]M. de León and M. Lainz Valcázar, Contact Hamiltonian systems, J. Math. Phys. 60 (2019), 102902.
  7. [7]J. Guckenheimer and P. Holmes, Nonlinear Oscillations, Dynamical Systems, and Bifurcations of Vector Fields, Springer, 1983.
  8. [8]M.W. Hirsch, C.C. Pugh, and M. Shub, Invariant Manifolds, Lecture Notes in Mathematics 583, Springer, 1977.
  9. [9]R.Z. Has'minskiǐ, Stochastic Stability of Differential Equations, Sijthoff and Noordhoff, 1980.
  10. [10]P. Nogueira Grossi, AXLE: Lean 4 Formal Verification Engine. github.com/TOTOGT/AXLE (2026).

Acknowledgments. The author acknowledges with gratitude the foundational influence of the teachings of Paramahamsa Nithyananda and the yogic scriptural tradition from which this work derives.

Continue the Series

The toy model SIAM paper proves four theorems (A–D) with full global dynamical analysis. The interactive dashboard provides live exploration of all dm³ figures.

Toy Model Paper → Interactive Dashboard → ← Volume I
Proved · kernel-checked
eigenvalue_neg_pos_z Orthogenesis/Architecture/ToyModel.lean:100
toyModel_tau Orthogenesis/Architecture/ToyModel.lean:151 Each name above is declared in this repository at the line shown and appears in an axiom report with no sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.
G6 LLC  ·  g6llc@proton.me  ·  +1 (646) 342-3751