The Open Gap in Vols I–V
Volumes I through V of the Principia Orthogona series establish the dm³ framework — the contact manifold, the operator chain, the recurrence ladder of constants \(\varphi, \mu, \eta, \Delta, \Sigma, \Omega \to \tau = 2\), and the Alternating Vanishing Theorem closing \(N_J|_\Gamma = 0\). The global attractor is proved (Theorems B.1–B.5); the Whitney A₁ fold at \(r_\star \approx 0.776\) is identified.
What remains open is explicit: the operators C, K, F, U appear in the symbolic chain as formal endomorphisms of the contact module, but their Aᵢ matrix entries — finite-rank approximants that compose to G — have not been written down and verified sorry-free in Lean 4. Vol VI supplies these matrices.
Theorem Manifest — Vol VI
The following table is the complete theorem manifest for Vol VI. Status reflects the current AXLE sorry queue.
| Code | Statement | Depends on | Status |
|---|---|---|---|
| VI.C.1 | Existence of \(A_C \in M_3(\mathbb{Z}[\tau])\) linearizing the C-operator at the fixed point | B.1, Vol I §4 | ⚠ sorry |
| VI.C.2 | Spectrum of \(A_C\): eigenvalues \(\{-2, 0, 1\}\) over \(\mathbb{Z}[\tau]\) | VI.C.1 | ⚠ sorry |
| VI.C.3 | \(A_C\) preserves the contact form: \(\alpha(A_C v) = \alpha(v)\) for all tangent \(v\) | VI.C.1, Vol II §2 | ✗ open |
| VI.K.1 | Existence of \(A_K\) encoding the Whitney A₁ fold at \(r_\star \approx 0.776\) | B.5, Vol I §6 | ⚠ sorry |
| VI.K.2 | Off-diagonal entry of \(A_K\) equals \(-2e^{-z_\star}\) evaluated at the saddle \(z_\star\) | VI.K.1, B.3 | ✗ open |
| VI.K.3 | \(A_K\) is the Jacobian of the LAW3M ODE at \((r_\star, \theta_0, z_\star)\) | VI.K.1, B.4 | ⚠ sorry |
| VI.F.1 | Companion matrix of \(x^2 - x - 1\) realizes F as a \(\mathbb{Z}[\varphi]\)-module map | Vol I §3, ch9-phi | ⬡ Lean sketch |
| VI.F.2 | Characteristic polynomial of \(A_F\) equals the Fibonacci minimal polynomial | VI.F.1 | ⬡ Lean sketch |
| VI.F.3 | The Reeb flow \(\partial_\theta\) is the exponential of \(A_F\): \(\exp(t A_F) = \text{Reeb}_t\) | VI.F.1, Vol II §5 | ✗ open |
| VI.U.1 | Existence of \(A_U\) such that \(A_U A_F A_K A_C = \text{Jac}(G)|_{\text{fixed pt}}\) | VI.C.1, VI.K.1, VI.F.1 | ✗ open |
| VI.U.2 | \(\det(A_U A_F A_K A_C) = (-1)^n\) (orientation-preserving contact map) | VI.U.1 | ✗ open |
| VI.U.3 | Entries of \(A_U\) lie in \(\mathbb{Z}[\tau]\) with \(\tau = 2\) | VI.U.1 | ✗ open |
| VI.G.1 | Main Theorem: \(G = U \circ F \circ K \circ C\) is realized sorry-free as \(A_U A_F A_K A_C\) over \(\mathbb{Z}[\tau]\) | VI.U.1–3, all prior | ✗ open · Vol VI headline |
| VI.G.2 | The characteristic polynomial of G factors as a product of n-bonacci polynomials \(\prod_{k=2}^{6} p_k(\lambda)\) | VI.G.1, chPI–chOmega | ✗ open · ladder closure |
| VI.G.3 | Spectral radius of G equals \(\tau = 2\): \(\rho(A_G) = 2\) | VI.G.2 | ✗ open · embodiment threshold |
| VI.X.1 | Contact diffeomorphism between LAW3M saddle, jackknife fold, and MTPA boundary (Earth Transport conjecture) | B.5, VI.K.3 | ✗ open · conjecture |
| VI.X.2 | Closed-form expression for \(r_\star\): algebraic number over \(\mathbb{Q}(\tau)\) | B.3, B.5 | ✗ open · hardest problem in series |
| VI.X.3 | N-bonacci ladder closure: \(\lim_{k\to\infty} \Delta_k = \tau = 2\) in \(\mathbb{Z}[\tau]\)-norm | chOmega, VI.G.2 | ⬡ Lean sketch · Omega chapter |
Construction Strategy for Aᵢ
3.1 The Linearization Approach
Each operator Aᵢ is defined as the Jacobian of the corresponding component of the LAW3M ODE \((\dot r, \dot\theta, \dot z)\) evaluated at the fixed point \((r_\star, \theta_0, z_\star)\). The ODE with \(\varepsilon = \tau = 2\) is:
\[\dot r = r(1-r^2) + 2(r-1)e^{-z}, \quad \dot\theta = 1, \quad \dot z = r^2 - 2(r-1)^2 e^{-z}\]
The Jacobian at the saddle \((r_\star, z_\star)\) has trace \(\text{tr}(J) = 2\cos(2\pi/7)\) (Theorem B.3) and determinant \(\det(J) = -\varepsilon_0 = -\tfrac{1}{3}\). Factoring this \(3\times3\) Jacobian into the ordered product \(A_U A_F A_K A_C\) is the main construction task of Vol VI.
3.2 The \(\mathbb{Z}[\tau]\) Requirement
We require all entries to lie in \(\mathbb{Z}[\tau] = \mathbb{Z}[2] = \mathbb{Z}\), i.e., the matrices have integer entries. This is a strong integrality constraint — it demands that the linearization be defined over the same ring as the embodiment threshold. The conjecture is that the ODE's algebraic structure forces this, with the exponential terms contributing only integer multiples of \(\tau = 2\) at the saddle point.
3.3 Lean 4 Target
Open Problems and Priority Queue
Three problems are flagged as priorities for UFRN collaboration and the LAW3M presentation window (October 2026):