Title: Principia Orthogona, Volume I: The Mathematics of Generative Transitions

Principia Orthogona, Volume I: The Mathematics of Generative Transitions ## Principia Orthogona, Volume I: The Mathematics of Generative Transitions### Version 7 — August 2026 **Pablo Nogueira Grossi · G6 LLC, Newark NJ · ORCID: 0009-0000-6496-2186** **V7 (this version):** https://doi.org/10.5281/zenodo.22084842**Concept DOI** (resolves to latest): https://doi.org/10.5281/zenodo.19117399Prior versions: V6 10.5281/zenodo.21146416 · V5 10.5281/zenodo.21121980 ·V4 10.5281/zenodo.20784030 · V1 10.5281/zenodo.19117400AXLE: https://github.com/TOTOGT/AXLE · DM3-lab: https://github.com/TOTOGT/DM3-lab G6 LLC ### What V7 corrects Two things, one about tooling and one about mathematics. **1. The Lean file had drifted off its own pin.** V3–V6 described`PrincipiaVol1.lean` as *"30+ facts proved, 1 sorry (clearly scoped), 0 axiomsbeyond Mathlib4."* Built in August 2026 against the Mathlib revision therepository pins — v4.14.0, December 2024 — it produced 81 errors. That is drift, not neglect, and the error profile says so.`Ordinal.sup` and `Ordinal.lt_sup` were deprecated on 2024-08-27;`Ordinal.IsLimit.add_right` was renamed `isLimit_add` on 2024-10-11;`Set.finite_insert` is the Mathlib-3-era spelling of `Set.Finite.insert`.Those are the names the file uses — the names that were current when it waswritten and run. What happened afterwards is ordinary and, without CI,invisible: Mathlib moved, the pin was advanced past the code, some laterhand-edits were never rebuilt, and nothing re-ran the build. V7 brings the file up to the pin, and ships a runner so the next drift is notsilent. The build log is included as `v6-build-errors.txt`, and the V6 fileunchanged as `PrincipiaVol1-V6-as-deposited.lean.txt`. **2. The separation theorem was false as stated, not unfinished.** V3–V6carried it with one `sorry` attributed to a missing Mathlib eigenvalue API(open obligation O1, AXLE issue #12). In fact the deposited statement ```IsDm3Stable M := ∀ i ≠ 0, |M i i| ≤ exp (−2)separation_theorem (n < 33) (M) (IsDm3Stable M) : M.trace ≠ 33``` is refutable: `IsDm3Stable` constrains only the transverse diagonal and saysnothing about `M 0 0`, so at `n = 1` it holds vacuously and the 1×1 matrix`(33)` has trace 33. The refutation is now proved in Lean and kept in thefile as `v6_separation_statement_is_false`. No Mathlib API would have closedthat gap — a hypothesis was missing, not a lemma. The underlying result is real and V7 proves it. Book 2 Theorem 12.2 and bothancestor files in AXLE (`main_v7.lean` Part H, `AXLE_v6.lean` Part H) state**Tr(M⁶) ≠ 33** — the sixth power. The exponent was dropped in transcriptioninto this deposit, leaving a hypothesis about `M` and an argument about `M⁶`with nothing joining them. At the first power the intended bound isnumerically false (`31·e⁻² ≈ 4.195`, not `< 1`); at the sixth it holds withroom to spare (`31·e⁻¹² ≈ 1.9·10⁻⁴`). Readers who cited the separation theorem from V3–V6 should cite the V7 formand its hypotheses. Nothing else in the volume is affected. --- ### What this volume does This volume develops a unified mathematical framework for generativetransitions: localised geometric events in which a trajectory undergoescompression, curvature intensification, loss of injectivity, andstabilisation, governed by the operator sequence G = U ∘ F ∘ K ∘ C. The framework rests on six minimal assumptions and produces: constructiveoperator definitions with explicit formulas; five structural theoremsincluding existence, non-commutativity, and finite branching; seven analyticalinvariants; four normal forms; a singularity classification restricted to theWhitney A₁–A₃ hierarchy; a free-discontinuity variational principle; and asymplectic Hamiltonian structure with a distributional generator at the fold. The second edition added a fifth operator E (Generative Time Circuit) withż ≥ 0; a term-by-term structural correspondence with Perelman's proof of thePoincaré conjecture via Ricci flow with surgery (Conjecture 15.1); and thedimensional threshold N = 3 as the minimum dimension for non-trivial contactgeometry, connecting it to c = 3 in the Collatz map (Conjecture 16.1). None of that mathematical content is withdrawn by this correction. Whatchanged is what can be said about the machine verification of it. --- ### What is machine-checked, exactly `PrincipiaVol1.lean` in this deposit now compiles and every theorem in it iskernel-checked. ```toolchain leanprover/lean4:v4.14.0Mathlib v4.14.0 rev 4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84theorems 58sorry 0axioms propext, Classical.choice, Quot.sound — nothing elseverified 24 August 2026``` Reproduce it with the small companion repository, which exists so that thisone file can be checked without building all of AXLE: https://totogt.github.io/vol1-proofs/ (webpage - V3) ```git clone https://github.com/TOTOGT/vol1-proofscd vol1-proofsbash tools/run.sh``` Three stages: `lake build`, then `#print axioms` over all 58 theorems, then agate that refuses on `sorryAx` or on any axiom outside the allowlist above.The same file lives in AXLE at`PrincipiaOrthogona1/PrincipiaVol1.lean`(https://github.com/TOTOGT/AXLE/blob/main/PrincipiaOrthogona1/PrincipiaVol1.lean). **What "machine-checked" covers, and what it does not.** Four things V3–V6said, or implied, that V7 withdraws: - **Theorems A–D are structures, not theorems.** `CompressionOp`, `CurvatureOp`, `FoldOp`, `UnfoldOp` are Lean *structures* — bundles of hypotheses — and `GenerativeOp` is a `def`. Declaring them proves nothing about them. What is machine-checked is that they are *inhabited*: twelve concrete instances over ℤ. V6's abstract already put this correctly; the machine-checked list did not.- **Two of their fields are weaker than their names, and V7 proves it.** `UnfoldOp.stable_branch` is satisfied by `n = 0` for every map on every type — it constrains nothing (`unfold_stable_branch_is_vacuous`). So "Theorem D (stability)" has no content beyond Φ-decrease. `CompressionOp.contractive` says `d(fx,fy) ≤ d(x,y)` — *non-expansive*; the identity satisfies it (`compression_permits_identity`). Assumption 3 should read "non-expansive".- **One theorem is withdrawn as an unfalsifiable guard.** V3–V6 counted `g6_equals_schumann : g6_layer_count_nat = schumann_4th_harmonic_integer := rfl`, where both sides are `def … := 33`. It is `33 = 33` and cannot fail. A kernel cannot check a claim about the ionosphere.- **A physical prediction was reported as machine-checked.** The Factor-of-3 Prediction (τ_grav < τ_dec/3) carried the words *"this is machine-checked (Lean: `basin_asymmetry`: 1/3 < 4/5)"*. `basin_asymmetry` is an inequality between two rationals. It says nothing about gravitational decoherence. The claim is withdrawn; the prediction stands as physical argument. The 58 theorems are arithmetic and structural: the Whitney conditions at thefold, the Gronwall radius, the contact sign, the Lyapunov exponent, thecanonical dm³ triple, the separation bound in the form stated below, theclub-filter and regeneration constructions, the crystal aspect ratio, and theTheorem 5.3 instances. They do **not** cover the analytic content of the book— the ODE integration, the variational principle, the symplectic argument, thePerelman correspondence. Those are argued in the paper and tracked as openobligations. Provenance lines of the form "*from `X.lean` — 0 sorry*" arewithdrawn from the Lean file's section banners: those files have not been builteither, and each claim returns when its file goes green. ### A new open obligation: the ε₀ instantiation (O7) ε₀ = 1/3 is the headline constant of this volume, and its instantiation asprinted does not close. §22 (Proof VII) states > ε₀ = |μ_max| / [2(1 + sup‖Hess V‖)] = 2/(2·3) = 1/3, where sup‖Hess V‖ = |L₂| = 3. Those three cannot all hold. The formula at H = 3 gives 2/(2·4) = **1/4**(`epsilon0_of_three`). The printed arithmetic `2/(2·3)` corresponds to1 + H = 3, i.e. H = 2 — which is also what the Lean line `2/(2*(1+2))` uses.`epsilon0_of_eq_third_iff` proves the choice is forced: for H ≥ 0, thisformula yields 1/3 for exactly one Hessian bound, H = 2. So either the formula is right and sup‖Hess V‖ = 2, or the bound is 3 and theformula should read |μ_max|/(2H) without the 1+. V7 does not choose. Itrecords that a choice is owed, and proves that one is. --- ### The separation theorem in V7 | theorem | content ||---|---|| `exp_neg_two_le` | `e⁻² ≤ 1/4`, from `1 + 1 ≤ e` alone — no interval arithmetic || `exp_neg_twelve_le` | `e⁻¹² ≤ (1/4)⁶` — the constant V6 asserted and could not prove || `transverse_sum_bound` | `\|Σ_{i≠0} λᵢ⁶\| ≤ 31·(1/4)⁶` — the step V6 admitted with `sorry` || `spectral_trace_ne_33` | `λ₀ = 1`, `\|λᵢ\| ≤ e⁻²` for `i ≠ 0`, `n < 33` ⟹ `Σ λᵢ⁶ ≠ 33` || `separation_theorem` | the same for a diagonal matrix: `Tr(M⁶) ≠ 33` || `separation_trace_first` | first-power form, carrying the normalisation `\|M₀₀\| ≤ 1` that V6 omitted || `spectral_trace_ne_33_upto` | the same conclusion to n = 131072 — the dimension bound is sufficient, not necessary || `separation_fails_in_high_dimension` | at ~1.7·10⁷ directions the trace does exceed 33 — so it cannot be dropped either || `coherent_directions_realise_33` | 33 *coherent* directions realise 33 — a statement about the coherent count, not about n || `v6_statement_false_at_dimension_five` | `diag(33,0,0,0,0)` satisfies V6's hypothesis and has trace 33 — not a dimension-1 technicality || `dm3_hypothesis_nonvacuous` | a witness satisfying the hypotheses, so the statement is not vacuously true || `v6_separation_statement_is_false` | the refutation of the V3–V6 statement, kept on the record | The margin is wide: under the hypotheses the sixth-power trace lies within31/4096 of 1, and misses 33 by more than 31. **One correction inside this correction.** A draft of V7 claimed `n < 33` wassharp, citing `Σ_{i