This four-page paper is kept as a negative control: a paper whose claims outrun its proofs, used to test whether the series' checks can say so. It claimed that nuclear matter is the dm³ cycle iterated along a Reeb flow, with a Tribonacci fractal measure and a g = 33 lock-in. This chapter reads it one claim at a time.
Orthogenesis/Eta/EtaChecks.lean compiled clean at Lean v4.32.0 in 294 s (bash tools/leancheck.sh --audit). The axiom gate found 18 declarations, all within the three permitted axioms (propext, Classical.choice, Quot.sound; two of them, trib_six and trib_seven, use none). The report, tools/verify-audit/2026-10-22/geometry__Orthogenesis__Eta__EtaChecks.axioms.txt, is identical to the 2026-10-01 report. A clean compile is not enough, so the cited statements were also read (R20): eta_exists_and_contracts takes its witness from isTribonacci_nonvacuous, an intermediate-value argument on [1, 2]; eta_inv_pow_strictAnti assumes only the defining equation of η, not its conclusion; T3_eigen_iff is a true “if and only if”. What these prove is stated in the table. What they do not prove is in the Foundations section.
NuclearControl.lean compiled clean at Lean v4.32.0 / Mathlib v4.32.0 in 320 s (bash tools/leancheck.sh --audit, author's run). The axiom gate found 7 declarations, none using sorryAx or an axiom outside the permitted three; the report is tools/verify-audit/2026-10-23/Downloads__NuclearControl.axioms.txt. What the three headline statements say, read per R20: stable_branch_vacuous holds for every map with n = 0; stability_at_threshold_false refutes the companion's statement by an explicit three-point model; trib_inv_sum is the identity η−1 + η−2 + η−3 = 1 only. An earlier run (2026-10-22 and an earlier 2026-10-23 run) failed with 13 errors because a stale copy of the file was checked; the failing text is not the file that passed.
Source. TOTOGT/AXLE, AnuclearPhysics/NuclearPhysicsB_latex.pdf (4 pages, 271,149 bytes, md5 7961116c2967103990c5a4fac3fc5f45), the file this chapter reads; LaTeX source beside it as TOGTnuclearPhysicsB.latex. The paper's Lean companion is grossi-ops/cajueiro/lean/NuclearPhysicsB/ (nine files; TribonacciMeasure.lean is byte-identical to AXLE/TribonacciMeasure.lean). By R22, Lean outside geometry is a claim nobody here can check until it moves in.
“Topographical Orthogenetic Generative Theory in Strong Interactions: Contact Geometry, dm³ Operator Cycle, and Fold Events in Nuclear Matter”, P. N. Grossi, G6 LLC, 4 pages, dated 11 April 2026. It is a different paper from the Version 4 TOGT paper (“seven proofs of the Tribonacci constant”); this one applies the framework to quarks, gluons and quark-gluon plasma.
Its argument: model the nuclear medium as a contact 3-manifold with a Reeb field Rα; let the cycle G = U ∘ F ∘ K ∘ C act along it; get the recurrence w(k+3) = w(k+2) + w(k+1) + w(k) with dominant root η ≈ 1.839; weight by η−k; read hadronization as fold events; state four falsifiability conditions.
| Claim in the paper | Status | What stands behind it |
|---|---|---|
| The cycle G = U∘F∘K∘C, acting along the Reeb flow, produces w(k+3) = w(k+2) + w(k+1) + w(k) | stated, not derived | The Lean companion says it in docstrings (Operators.lean, TribonacciMeasure.lean: “arises from iterated G-applications”). I did not find a theorem that derives it, by reading all nine files of the companion and by searching geometry and AXLE for the recurrence. NbonacciLadder.lean says so of itself: “That identification is made in the chapter prose and is not a theorem.” The paper never says why three terms. |
| The recurrence's dominant root η is a root of x³−x²−x−1, η > 1 | proved | eta_exists_and_contracts (kernel-audited 2026-10-22); companion matrix T3 has det 1 and (η², η, 1) is an eigenvector iff η is Tribonacci (T3_det, T3_eigen_iff). Script blocks [1] and [3] agree numerically. |
| The weights η−k contract | proved | eta_inv_pow_strictAnti. The companion has the same fact as weight_strictAnti. Script block [4]: they sum to η/(η−1) ≈ 2.1915. |
| “η ≈ 1.839 (plastic number)” | wrong name | The plastic number is the real root of x³ = x+1, ≈ 1.3247. 1.839 is the Tribonacci constant. Script block [2]. |
| Figure 1: ring radii scale as ηk | checked | Read from the PDF's vector drawing: the five rings are 24.938, 45.867, 84.363, 155.168, 285.398 units wide; every successive ratio is 1.8393. The drawing is faithful to its labels. It plots no measurement. |
| The weight η−k “induces a fractal measure μη on ker α” | not a measure; natural reading is Lebesgue | In the companion, μη is the sequence weight k = η−k on ℕ (and foldAmplitude, its alias). No MeasureTheory measure on any space appears in the files I read. The only measure-like fact in the companion is a finite sum over indices. Built properly it is Lebesgue measure, not a fractal: see the next section and graph C. |
| g = 33 “emerges naturally” as a lock-in scale, “consistent with lattice-QCD” | false as stated (finite counterexample) | In the companion, g_threshold : ℕ := 33 is a definition, and the lock-in itself, stability_at_threshold (every G-orbit reaches a fixed point within 33 generations), ends in sorry and is labelled an open obligation. Its hypotheses bound no orbit length by 33 (UnfoldOp.stable_branch allows any n), and a three-point counterexample satisfies every hypothesis while the orbit never reaches a fixed point (verify script block [7], graph D). The Lean statement of that counterexample, stability_at_threshold_false in NuclearControl.lean, compiled clean at Lean v4.32.0 on 2026-10-23 (author's run; report tools/verify-audit/2026-10-23/Downloads__NuclearControl.axioms.txt). No lattice-QCD number is compared anywhere I looked. |
| Fold events are confinement or hadronization | interpretation | The companion defines a fold as a non-injective map with a finite branch locus, and labels it “nuclear analog: hadronization” in a docstring. No computation connects a fold to a QCD observable. The shared thing is a threshold shape, not a shared mechanism (R10). |
| W.1, F.1, Φ.1: deviations in multiplicity spectra, flow harmonics, dilepton spectra | stated, unregistered | The companion writes all three as definitions (W1, F1, Phi1 in FoldEvents.lean): predicates, not theorems. Under R30 each needs a pre-registration and a detection test before any data is read; none exists, so none can count for or against the framework. |
| “All operator algebra is verified in the AXLE engine (Lean 4)” | overstated | The companion's own closing note says the operator compositions and measure definitions are “formally stated”. The files carry 7 sorry (Chain 3, Conformal 3, FoldEvents 1, by grep), a declaration poincare_collatz : True := trivial that its docstring calls a placeholder, and 13 theorems flagged by tools/textual_conclusion_scan.py on 2026-10-22 (96 scanned; the scanner finds candidates and a human read is still owed on each). The library lives in grossi-ops and AXLE, not in geometry (R22), and I have not compiled it. |
A negative control is only worth keeping if the checks can fail on it. Of the ten rows above, three hold: the Tribonacci root and the contracting weights (kernel-audited) and Figure 1's scale (read from the drawing). Seven are flagged: one identification stated and not derived, one wrong name, one overstated verification claim, one “measure” that is a sequence, one threshold whose own Lean statement ends in sorry, one interpretation with no computation, and one set of predictions that cannot count until it is pre-registered. So the checks did fail on it, in each of the ways the series says it looks for: a true theorem attached to a claim it does not support, a number carrying the wrong name, and a prediction with no test of its own power.
How the absences were looked for (R15). “Not derived” and “not a measure” rest on reading all nine files of the Lean companion, searching geometry and AXLE by content for the recurrence and for Tribonacci in any case, and listing every file named for it on the Desktop. They are statements about what I found, not proof that no derivation exists elsewhere.
What the control does not show is that the framework is false. The held rows are true and the flagged rows are untested or unsupported, which is a different thing. A positive control, a paper whose claims all hold, would be the other half of the pair, and none is claimed here.
R21 says an evidence tag on a chapter that stands on an untagged assumption is decoration, so the base comes first. Everything proved above is a fact about the cubic x³ = x² + x + 1 and the sequence it governs. None of it is a fact about quarks, gluons or a contact manifold. What the paper needs underneath:
GenerativeManifold (a metric carrier, a functional Φ, a field) and a ContactPair, but no nuclear medium is an instance of either. The paper's “effective contact form on the QCD vacuum” is therefore a name for a hypothesis, not an object.Operators.lean as structures that bundle their own properties as fields (C contractive and injective, K non-increasing in Φ, F with a finite branch locus, U decreasing Φ with a stable branch). That makes the composite G a well-formed statement and nothing more: the properties are assumed of any instance, and no instance is given. The paper itself describes the four in words only.Until these are discharged, the tags in the table above apply to the arithmetic only.
The figure shows five rings stacked along the Reeb axis, each wider than the last by the factor η. Reading the vector drawing directly, the factor is 1.8393 on every step, so the figure does what its caption says. Two cautions. It is a schematic, so the rings carry no data. And the rings are levels along the Reeb direction, not orbits: a Reeb flow holds its angle fixed and preserves contact volume, so the picture must not be read as an advancing helix. That is the same reason the series withdrew its “helical phase” prediction.
The April paper left several parts it could not defend. Looking through the series for each one:
| Part April could not defend | What can be done now | Result |
|---|---|---|
| A measure μη from the weights η−k | Build one. Dividing η³ = η² + η + 1 by η³ gives η−1 + η−2 + η−3 = 1, so cutting [0,1] into pieces of those lengths tiles it exactly. | With mass equal to length the measure is Lebesgue measure and has dimension 1, so it is not fractal. A fractal measure would need other weights, and the paper names none. Identity: trib_inv_sum in NuclearControl.lean, kernel-audited 2026-10-23 (standard axioms only); it proves the identity and nothing about a measure. Numbers: verify script block [6]. |
| The g = 33 lock-in | Test the companion's own statement. | False as stated, by a three-point counterexample (graph D, block [7]). Its hypothesis stable_branch is satisfied by n = 0 for any map, the defect already fixed in Theorem53NonCommutativity.lean but still present in Operators.lean. Lean: stable_branch_vacuous (no axioms) and stability_at_threshold_false (standard axioms only), kernel-audited 2026-10-23 in NuclearControl.lean. These restate the companion's definitions with one change (an attribute [instance] line, because the verbatim structure does not elaborate under v4.32.0); the companion's own files, pinned to v4.14.0, were not run. So the result is about the restated statement. |
| Why g = 33 at all | Look for a derivation in the series. | I did not find one. The series carries χ(H*(X⁶)) = 33 as an open conjecture (book6/g6-crystal.html), and Version 4 already labels the link to a nuclear multiplicity analogical. |
| Why three terms (n = 3) | Look for a selection argument. | Version 4 says the three-step traversal that selects n = 3 “is not examined”. I did not find one elsewhere; NbonacciLadder.lean proves bounds for every k, which treats 3 as one case, not a selection. |
| The contact space for nuclear matter | Nothing new. | Version 4 calls αQCD conjectural. Still a name for a hypothesis. |
| W.1, F.1, Φ.1 against data | Pre-register, then test (R30). | Not started. I have not looked for the public datasets. Under R30 the pre-registration is committed first, and the test is shown able to detect the effect, on synthetic worlds, before any real data is read. Until then these rows cannot move. |
Net: of the parts April could not defend, one can be settled in the negative today (the lock-in), one can be replaced by a precise and less flattering statement (the measure), and the rest are unchanged. None of it moves a row up. It moves two rows from “stated” to “disproved as stated” and “constructed, not fractal”, which is what a negative control is for.
Each graph recomputes from the definitions on this page when you move a slider. Nothing is a stored image. The numbers are the ones the verify script prints.
It does not prove or disprove that nuclear matter follows the cycle. The proved part is the arithmetic of the Tribonacci constant. Everything that would make it physics, a measure on a real space, a proof of the 33-generation lock-in, a connection to a QCD observable, is still open (in the files I read), and the paper's own falsifiability conditions cannot be tested until they are pre-registered.
python3 ch-negative-control-strong-interactions-verify.py ../AXLE/AnuclearPhysics/NuclearPhysicsB_latex.pdf bash tools/leancheck.sh --audit Orthogenesis/Eta/EtaChecks.lean
Without the PDF, block [5] prints SKIP, not PASS.