| Theorem | Statement | Key Step | Physical Consequence | Lean 4 |
|---|---|---|---|---|
| B.1 | rs = 2cos(3π/7) ≈ 0.4450 — unique root of r³−r²−2r+1=0 in (0,1) | Trigonometric method on depressed cubic; discriminant > 0 | Exact saddle location — safety margin for rotating EM systems known analytically | pending |
| B.2 | (1+rs−rs²)² = 2−rs | Expand and reduce modulo the minimal polynomial r³=r²+2r−1 | Fundamental algebraic identity connecting saddle coordinates | pending |
| B.3 ★ | tr(J)|saddle = 2cos(2π/7) ≈ 1.2470 | tr=1+rs−rs² (from B.1 cubic); √(2−rs)=2cos(2π/7) (from B.2) | Divergence at saddle is a 7th-root-of-unity cosine — exact stability rate | pending norm_num |
| B.4 | J22|saddle = rs² | ∂z(ż) = 2(r−1)²e−z; saddle condition gives 2(rs−1)²e−zs = rs² | Exact Jacobian entry; used in eigenvalue computation | ✓ simp |
| B.5 | λ± = cos(2π/7) ± ½√(32rs²+15rs−10) ≈ 1.1097, −0.2443 | Quadratic formula from tr(B.3) and det(J) reduced mod cubic | λ+>1: escape mode; λ−<0: stable saddle manifold decay rate | pending quadratic |
All five theorems are proved in closed form in
law3m.html,
Poster 2, and
GTCT Vol IV §6.5.
Lean 4 mechanisation of B.1–B.3 awaits Real.cos_pi_div_seven in Mathlib (gap, not a mathematical gap).
B.4 is machine-verified (0 sorrys).
Open Problem O.1 — Closed Form of the Whitney A₁ Basin Boundary r*
The basin boundary r* ≈ 0.77594059 (certified to 8 decimal places,
DOP853 integrator, rtol = 10⁻¹², bisection tol = 10⁻⁷) is the Whitney A₁ fold threshold of the
operator F in the dm³ chain G = U∘F∘K∘C. Below r*, trajectories escape; above r*, they converge
to the attractor Γ at r = 1.
Why no closed form is currently known. The fold F is irreversible — GTCT (Galilean Theory of Contact Transformations) proves that time flows strictly forward on contact manifolds. The pre-image of the fold is not unique, and backward integration is inadmissible as a matter of principle, not just numerical difficulty. r* cannot be recovered algebraically by inverting any map in the chain.
Note: r* is not the saddle rs = 2cos(3π/7) ≈ 0.445, which is resolved analytically by Theorems B.1–B.5. The saddle lies strictly inside the escape basin; the fold lies between saddle and attractor.
Candidate approach. Écalle resurgence theory applied to the Borel transform of the ODE may provide a transseries representation of r* and determine whether it is a period, a Gevrey-1 constant, or genuinely new. No such result currently exists in the literature.
| Result | Status | File |
|---|---|---|
| alternating_vanishes_beyond_dim | ✓ 4 lines | VolumeTwo.lean |
| N_J|Γ = 0 (Level 1) | ✓ dim arg | VolumeTwo.lean |
| N_J|ξ = 0 (Level 2) | ✓ d²=0 | VolumeTwo.lean |
| N_J|M = 0 (Level 3) | ✓ ι_R dα=0 | VolumeTwo.lean |
| B.4 — J₂₂ = rs² | ✓ simp | GTCT.lean |
| g₃₃ = 33 | ✓ decide | Orthogonality.lean |
| rank1_norm_eq | ✓ 0 sorrys | AXLE core |
| epsilon_zero_waddington | ✓ closed | AXLE core |
| Result | Status | Blocker |
|---|---|---|
| B.1 — saddle cubic root | ⊙ pending | Real.cos_pi_div_seven |
| B.2 — fundamental identity | ⊙ pending | ring / norm_num |
| B.3 — trace = 2cos(2π/7) | ⊙ pending | Real.cos_pi_div_seven |
| B.5 — eigenvalue formula | ⊙ pending | quadratic tactic |
| Lyapunov outer basin | ⊙ Issue #12 | convergence rate |
| r* closed form | ⊙ open problem | See O.1 above |
| Theorem 15.4 (RH rung) | ⊙ deferred | N–N on full TM |
Full AXLE repository: github.com/TOTOGT/AXLE ·
Active file: PrincipiaOrthogona_v2/VolumeTwo.lean