A working record, partly done. The preprint is cited as literature (J. L. Nielsen, “A Complete and Unified Gauge Theory with Gravity on the Complex Hopf Fibration”, preprint dated 14 Aug 2026). This chapter is about its claims and its Lean file, not its author. Two of the fifteen checklist items below are open. A checked box means a step was done and can be re-run, not that the theory is right or wrong.
The preprint claims that charge quantization and unification force one fibre bundle, and that the Standard Model gauge group, three generations, the particle masses and the cosmological constant then follow as theorems with no free parameter. Its abstract says five structural theorems are checked in Lean 4. It has about 300 lines containing the word “Theorem”; a count of distinctly numbered statements gives 140.
A full kernel check of everything cannot be done here or soon. Most of the statements concern objects the Lean library does not yet have: bundles with connections, spectra of the Beltrami operator, Ray–Singer torsion. So the work is sorted by what a kernel can reach.
Five steps are done. Seven are open.
propext, one on propext and Quot.sound. This matches what the paper reports. Report: tools/verify-audit/2026-10-26/.book26/nielsen-census.tsv.book26/nielsen-abstract-arithmetic.py) and checked in Lean (book26/NielsenAbstractArithmetic.lean; 6 theorems, standard axioms only, run 2026-10-26). Reproduced: 3/(4π) = 0.238732, which is 0.39σ from the Thomson-limit value the paper compares with; the neutrino masses sum to 59.282 meV; the boson masses sit within 0.23σ of PDG 2025; the cosmological-constant formula gives 2.940×10−122. Not reproduced as a prediction: at the Z pole, the abstract’s own masses give 1 − (mW/mZ)2 = 0.2232, which differs from 3/(4π) by more than 0.015, and the paper bridges the gap with a “dressing” equal to the residual. The larger neutrino splitting is compared with 2.453×10−3 eV2, which I believe, from memory and not yet verified, is the 3–2 splitting; against the 3–1 splitting from the one NuFit-6.0 block I could read it is −3.2σ. The H0 value is the cosmological-constant formula rearranged with the measured dark-energy fraction.book26/nielsen-algebra-six.py (11 checks, 2 controls). The census tiers exactly six statements as “2 algebra”. Read against the source: two are correct, one is not an algebra claim, three carry defects. Cor 1 (p. 16), Bianchi is geometric — correct. d∇Ω = dΩ + [ω,Ω] cancels term by term, cubic terms included. Prop 2 (p. 50), field lines are copies of the group — correct, and standard. Cor 14 (p. 97) is not an algebraic identity — it assigns particle types to shells; nothing to verify as algebra, carried to C6. Cor 2 (p. 21): the conclusion holds, the premise is false. It reads “the Standard Model group SU(3)×SU(2)×U(1), a genuine direct product”, while the paper’s own abstract gives the group as [SU(3)×SU(2)×U(1)]/ℤ₆, which is not a direct product. The curvature decomposition survives because it needs only the Lie algebra, which the discrete quotient leaves alone — but the statement as written is false of the group the paper says it is about. Lem 4 (p. 101): part (iii) does not follow from part (ii). (ii) bounds ∥v⊥∥²/∥v⊤∥² by 2(n−2)/3; (iii) asserts ∥v⊥∥ < ∥v⊤∥ on all physical shells. The paper’s shells are S³, S⁵, S⁷, S⁹, so n runs to 5 and the bound reads 0, 2/3, 4/3 and 2. On S⁷ and S⁹ it permits a ratio above 1, so the stated inequality is not implied there. (iii) may still be true; what fails is the proof offered for it. Cor 19 (p. 154): integer orbital quantization only. w ranges over π₁(S¹) ≅ ℤ, so Lz = ℏw admits no half-integer. The corollary is correct about orbital angular momentum; what it cannot do is supply spin-½, which every fermion in the theory needs. And the definition immediately after it is circular. Definition 13 derives ℏ = ℓP²c³/G and says ℏ “is not an independent input” because c and G are derived — but that formula is the definition ℓP := √(ℏG/c³) rearranged, and no value for the fiber cross-section is computed from the geometry anywhere; it is identified with ℓP by definition. So ℏ is obtained from ℏ. Table 16 lists it under Predictions (C8). Not established: that (iii) is false on S⁷ or S⁹, or that Cor 2’s conclusion fails.book26/ch08-inputs-verify.py (8 checks, 3 controls). The item’s suspicion holds, and the contradiction is between two pages of the same paper. p. 12, under the heading “Proof of zero dimensionless free parameters”: “The only dimensionful input is the electroweak VEV, v = 246 220 MeV (Axiom 1)”, and the paper “contains no fitting routine, no optimization loop, and no adjustable coefficient”. p. 216, Table 16 — whose stated purpose is to “distinguish what TUFT assumes from what it predicts” — puts under Predictions: “SM gauge group + GR; c, ℏ, e, α, G, v”. The same v is Axiom 1 on one page and an output on the other, and the Inputs row of that table lists only topological normalisations. A second mismatch on the same page. Table 16’s own reproducibility note sets masses by mj = (ℏ/c)(λj/reff) “with v/R fixed once across sectors”. Fixing a ratio once so that sectors agree is a calibration, and the formula consumes ℏ and c, which that same table calls predictions. A quantity cannot be an output of the calculation that uses it as an input. The p. 11 table is a third labelling. There v is marked “Input (v)”, while α = 1/137.036, G, c and e are all “Derived”. So the paper gives three accounts of its own inputs in eleven, twelve and two hundred sixteen pages, and they do not agree. Not established: that v cannot be derived, or that Theorem 68 (G) and Theorem 66 (α) fail — neither was read. What would settle C8: one table, stating for each of c, ℏ, e, α, G and v whether it is assumed or computed, and if computed, from what. The claim of zero free parameters is only as strong as that list.book26/ch08-sin2w-verify.py (6 checks, 4 controls). The scheme and the uncertainty. The 0.4σ is against the PDG Thomson-limit value sin²θW(0) = 0.23867 ± 0.00016; recomputed, 0.39σ. Against the MS-bar value at MZ, 0.23122 ± 0.00006, the same number is 125σ. The paper does not report that as a failure: it writes that the PDG value “implies” a spectral correction Δspec ≈ −0.0075, which is back-solved from the discrepancy rather than computed from the Hopf-shell spectrum. The same unquantified mechanism then absorbs a 5.0% offset in g and 3.0% in g′. The derivation against its own definition. Two lines above eq. (100) the paper writes sin²θW = g′²/(g²+g′²), where g′ is the hypercharge coupling; eq. (100) then identifies the numerator as the weight “carried by the SU(2) sector” and puts dim SU(2) = 3 on top. By the paper’s own formula the SU(2) fraction is cos²θW. And a generator count over a Gauss–Bonnet integral ∫K dA = 4π is not a ratio of gauge weights: carried out as the prose describes, the degree-of-freedom ratio is 1/4 or 3/4, neither of which is 0.2387. Two derived values of one symbol. The same page derives it again from the paper’s own Table 6 masses: 1 − mW²/mZ² = 0.223200, which reproduces exactly and matches the PDG on-shell value to 10−5. So the theory yields 0.238732 and 0.223200 for one quantity — 6.96% apart, 97σ in the very uncertainty used to claim 0.4σ — and each is compared to whichever PDG scheme value it lands on. Not reproduced: eq. (101) prints g ≈ 0.6205; 4π√(α/3) with α = 1/137.036 gives 0.6198. Their α comes from Theorem 66, unread, so this may be internal. What would settle it: a value of Δspec computed from the shell spectrum without reference to the measured number, and a statement of which scheme eq. (100) is a prediction of. Neither is in the paper. This is a finding about internal consistency, not a claim that 3/(4π) is wrong physics or that no derivation could exist.book26/nielsen-kernel2-gap.py (8 checks, 2 controls). Section 3 read the Lean as not proving “no product splitting of the bundle” and marked that a hand derivation. The reading holds, and the gap is not a missing line — it is three gaps, and the middle one cannot be closed at all. (1) The Lean never touches a space. Kernel 2 is MiniRing over an arbitrary type; the section contains no topology, no connectedness, no continuity, no manifold. The no-zero-divisor condition nzd enters as a hypothesis of domain_idempotents_trivial and is instantiated nowhere in the file. (2) The hypothesis is unsatisfiable for the ring that matters. The correct bridge is idempotents ↔ clopen sets: X is connected iff C(X) has only the idempotents 0 and 1. The Lean assumes instead that the ring has no zero divisors, which is strictly stronger and false for C(X) on every connected space larger than a point — two bump functions with disjoint supports multiply to zero and neither is zero. The script exhibits such a pair on ℝ and confirms f·g = 0 at every one of 20,001 sample points while max|f| = max|g| = 0.368. So nzd is not an unproved hypothesis in the intended application; it is an unsatisfiable one. (3) The conclusion is about the wrong product. The Lean’s prodRing is the direct product, multiplying componentwise, and a ring direct product corresponds to a disjoint union of spaces: C(X ⊔ Y) ≅ C(X)×C(Y). A Cartesian product of spaces gives a tensor product by Künneth. “No product splitting of the bundle” is a claim about ×; kernel 2 is a claim about ⊔. Even granting (1) and (2), it answers a different question. Not established: that the preprint’s physical claim is false, that no bundle argument exists, or that kernel 2 was ever intended to carry the bundle step — only that as written it cannot reach it.book26/nielsen-quark-boson-table.py (7 checks, 2 controls). Formulas transcribed verbatim from the preprint’s own Appendix A script, SECTION 3 (eq. 97) and SECTION 4 (eq. 122), with that script’s own PDG dictionary. The transcription reproduces the printed Λ₅ = 6.09144×10⁻², a₅ = 3.564112 and the p. 131 quark table (u = 2.160005 MeV). The uniform +0.23% offset is lepton-only. W −0.0026%, Z −0.0032%, H +0.017%; u +0.0003%, d −0.125%, s +0.177%, c +0.214%, b −0.186%, t +0.061% — mixed signs, every pull under 1.5σ. That is not a point in the paper’s favour. (i) The uncertainties are not comparable. The up quark is known to ±3.2%, the electron to ±3×10⁻⁸%. A 0.2% quark deviation is 0.06σ; the same relative deviation on the electron was over 10⁶σ. “Within experimental error” means something eight orders of magnitude weaker here. (ii) There is no uniform offset because there is no uniform formula. Each sector carries its own constants, and the quark exponent carries three separate expressions for λT, one per generation — 2/(3√3), 2/π + ζ(3)/(24π), 2/π − ζ(3)/(24π), with a sign flip between n = 2 and n = 3 — plus three torsion values τ(Kn) = (1, 4, 3) and a 2/3 prefactor applied to the first generation alone. Six quark masses rest on that many per-generation choices. The boson sector likewise uses three distinct TB expressions and an rf = r + ζB shift, and its ΛB is commented in the paper’s own script as a “post-absorption value”. And the appendix settles C14’s fork from the inside. SECTION 1 of that same script checks the identity zeta′(-2) = -z3/(4*pi**2) — exactly the constant C13 computed — and then SECTION 2, one section later, writes the lepton exponent as -z3*n**2 with the comment “Casimir det, from Nash-O’Connor lens space”. The correct coefficient is verified in the paper’s own verification script and not used. Not established: that the quark or boson numbers are wrong — they agree within the quoted errors; nor the couplings and anomalous moments, which this does not tabulate.book26/nielsen-lepton-table.py, run). The three masses come out 0.23% high, a uniform offset the script itself prints, which is more than 106, 105 and 40 standard deviations for the electron, muon and tau, so the abstract’s “within PDG uncertainties” does not describe them. The mass ratios agree to 0.002% and 0.006%, which is a one-parameter result anchored on one mass. The exponent has five terms; the one that distinguishes the tau, a trefoil “regularization”, acts on that lepton alone and moves it by about 1.1%. A Lean version of the deviation comparison is written (NielsenLeptonDeviation.lean) and was run on 2026-10-26: 363 s, three declarations, axioms within the permitted set, no sorryAx (receipt: tools/verify-audit/2026-10-26/geometry__book26__NielsenLeptonDeviation.axioms.txt). A clean axiom report is not a reading of the statement — per R20 a theorem can assume its conclusion and still report clean — so what this establishes is that three named declarations elaborate, not that they say the deviations exceed the quoted uncertainties.book26/nielsen-lens-determinant.py (6 checks). The preprint’s Sector Determinant Lemma asserts ln det′ Bn = L(n) − ζ(3)·n² + O(1) and uses exp(−ζ(3)n²) in the mass formula. The coefficient is ζ(3)/(4π²) = 0.030448, not bare ζ(3) = 1.202 — smaller by 4π² = 39.478 in the exponent. Method. On the unit S³ the coexact 1-form eigenvalues of ★d are ±N for N ≥ 2 in the SU(2)L×SU(2)R representations (N/2,(N−2)/2) and its swap; the ℤn is the Hopf U(1) in SU(2)L, so the invariant sector keeps weights 2mL ≡ 0 (mod n). The resulting multiplicity is quasi-polynomial of period 2n, so the spectral zeta is a finite sum of Hurwitz zetas and ln det′ = −ζ′(0) is exact: no cutoff, no truncation. Why the number holds, three ways. (i) At n = 1 the sector is all of S³, ζ(s) = 2[ζR(s−2) − ζR(s)], and the code reproduces the closed form ζ(3)/(2π²) − ln 2π = −1.776980152292558942 to 31 digits. This is also where the 4π² comes from: ζR′(−2) = −ζ(3)/(4π²) exactly, and the n² term inherits it. (ii) The quasi-polynomial multiplicities match a direct enumeration of SU(2) weights for n ∈ {1,2,3,5,7,8} and every N < 200. (iii) The coefficient was not fitted against a target: it converges as the window moves up (6×10−7 at n = 8–64, 5×10−8 at 32–64), and a local three-point solve with the target absent from the basis gives −0.030448471 at n = 48. Consequence. With the correct coefficient the Gaussian factor in m2/m1 is 0.913, not 0.027. It is then inert, and whatever generates the lepton hierarchy is not this term. Two further defects in the lemma as stated. The “+ O(1)” is too strong — there is a growing ln n term, fitted at ≈ 4/3. And Cheeger–Müller cannot confirm this coefficient: torsion is an alternating combination of determinants across all form degrees, in which a metric-dependent n² term cancels, so the second citation offered as support cannot bear on it. Not established: that the asymptotic follows from the preprint’s cited route through Nash–O’Connor; the ln n coefficient analytically; the non-trivial χn sectors; or sensitivity to radius and zeta normalisation. Worth separating out: the corrected statement is a small standalone result in spectral topology, refereeable without any physics.book26/nielsen-exponent-fork.py (6 checks, 2 controls). C12 established that the preprint’s own appendix script reproduces its lepton table using exp(−ζ(3)n²); C13 established that the lens-space determinant gives ζ(3)/(4π²). Substituting the second for the first, holding Λ, a, β, α and the trefoil factor fixed: me +223%, mμ +1.08×104%, mτ +3.81×106%. The spectrum does not shift; it is destroyed. And the escape route is closed by the paper’s own argument. The failure is in the ratios — μ/e comes out 6949.7 against the observed 206.77, a factor of 33.6; τ/μ comes out 5886.5 against 16.82, a factor of 350. p. 12 argues that v is a unit conversion because “changing v multiplies every mass by the same constant” and “leaves invariant every mass ratio”. That is correct, and it means the single empirical input cannot repair a ratio failure. Λshell cancels in m2/m1 and m3/m2. So exactly one of these holds, and both contradict “zero dimensionless free parameters”: (A) the Sector Determinant Lemma is right, and the mass formula is wrong by factors of 34 and 350 in the ratios; or (B) the mass formula is right, and the exponent ζ(3) is not the lens-space determinant coefficient — in which case its stated derivation does not support it, and the value that fits the data is precisely the one the derivation does not give. Not established: which branch holds; whether the lemma was ever meant to apply to this formula; or whether a and φn are right — both remain undefined in the text.book26/nielsen-sector-coefficients.py (6 checks, 2 controls). It does — with a different unexplained prefactor each time. Leptons (Thm 51, eq. 88) take −ζ(3)·n², called “Casimir determinant suppression”. Quarks (Thm 55, eq. 121) take +ζ(3)/12·n², called “the quadratic Casimir–determinant coefficient from the lens-space zeta evaluation on S⁵”. Torsion takes σ₃ = ζ(3)/(4π²) on S³ and σ₅ = ζ(3)/(16π²) on S⁵, the paper’s stated σ₃/4, which checks out. So one constant carries four different multipliers — 1, 1/12, 1/(4π²), 1/(16π²) — and two of them claim the same mechanism, a lens-space zeta determinant, while differing by a factor of 12 and in sign (leptons suppressed, quarks enhanced). The one case computable from first principles is S³, done exactly in C13, and it gives none of them: the lepton value is 4π² = 39.478 times it, the quark value 3.29 times it. The bosons are a fifth quantity under a confusing name. Eq. (96) dresses the tree-level factors by exp(aBn + ζBn²) with ζB = √3·α/(2π) = 0.002012 — not a zeta value at all, and numerically inert (exp(ζBn²) = 1.018 at n = 3). And the preprint shows its lepton table anchored. §8.15.4 on p. 122 prints the electron deviation as “0.00% (anchor)” with μ at +0.002% and τ at 0.0002%, while the paper’s own script prints a uniform +0.22–0.24% offset on all three (C12). The displayed table is the anchored presentation; the abstract’s “within PDG uncertainties” rests on it. Not established: that ζ(3)/12 is wrong for S⁵ — the S⁵ lens-space determinant was not computed, only the S³ one. What is established is that two sectors cite one mechanism, take values a factor of 12 and a sign apart, and that the checkable case matches neither. Taken with C14, this is the shape of a family of free multipliers on one constant, each asserted as derived.| Kernel | What the Lean proves | What it does not |
|---|---|---|
| 1. Charge quantization forces holonomy | If some charge is inadmissible, the holonomy is not trivial. A contrapositive in a setup where Charge, Phase and Loop are arbitrary types. | Nothing about U(1), a charge lattice or a connection. |
| 2. A domain has no product split | A ring with no zero divisors has only the idempotents 0 and 1, and a direct product of two nonzero rings has zero divisors. | A direct product of rings corresponds to a disjoint union of spaces (connectedness). A Cartesian product of spaces corresponds to a tensor product (Künneth). My reading, untested: the Lean does not prove “no product splitting of the bundle”. |
| 3. Completeness forces universality | Any two classifying objects for the same bundle functor are equivalent. The paper’s U1_forcing is this theorem renamed; an example that closes by rfl shows it. | That the complex projective space classifies anything. That is a hypothesis. |
| 4. Completeness as a theorem | Every bundle is a pullback of the universal one. This restates a field of the hypothesis Classifies, closed by that field. | That nature’s fields satisfy the hypothesis. |
| 5. Affine absorption | Adding a constant and a linear term does not change a second difference. Linear integer arithmetic. | Anything about spectra or masses. |
The Lean compiles and the axioms are standard, so these are real theorems. The gap is between what they state and what their names and the abstract claim.
This is an estimate. No statement has been timed, and it should be recalibrated after the first three.
| Piece | Statements | Hours (estimate) |
|---|---|---|
| Five kernels, compile and fix | 5 | 2–4 |
| Arithmetic claims | about 16 | 20–30 |
| Algebra statements | about 6 | 12–24 |
| Hypothesis audit, no kernel | about 99 | 30–40 |
| Full careful read | all | 15–25 |
| This chapter and its script | 1 | 6–10 |
| Total | about 85–130 |
Two working sessions in parallel could cover this in about three working days of elapsed time. Kernel-checking the statements that need missing definitions is a separate project of months, and is not in the table. Doing it before the end of October is not possible.
This section is about method, and applies to any large claim, including this project’s own. A kernel checks that conclusions follow from stated hypotheses. It cannot check that nature satisfies them. So the useful question is where each claim sits relative to the kernel.
One claim in this preprint is pure mathematics and independent of the physics: that a lens-space determinant yields a ζ(3)n² term. A topologist can referee it as it stands, which makes it the natural first piece to submit.