Masses Mass Genesis T10 Beat8 Holonomy Holonomy Trace Eq Trace Num Div8

The eight-beat holonomy trace

In geometry, a holonomy measures how much a vector or object is rotated after being carried around a closed loop. The declaration holonomyTrace_eq_traceNum_div8 is a formal statement in the Recognition Science framework's machine-checked library of formal theorems. It concerns walks of exactly eight steps along the edges of a three-dimensional cube, where each step is a quarter-turn rotation about one of the cube's three axes.

The framework models a ledger, a discrete record of events, as a sequence of postings. Each posting is a single unit addition to one of three accounts, which corresponds to moving along one edge of the cube. A cascade is a sequence of such postings. The declaration proves that for any closed cascade of eight postings, meaning one that returns to its starting vertex, the holonomy trace is exactly the integer trace numerator divided by 8. The trace numerator is the real part of the product of the eight quarter-turn quaternions, an integer. The theorem establishes that this trace can only be one of five values: -2, -1, 0, 1, or 2.

The proof is kernel-checked, meaning it is verified by a computer proof assistant. It uses only decidable enumeration of all 3^8 = 6561 possible axis sequences, with no reliance on external computational trust. The theorem also proves a sharper fact: two specific eight-step walks, xxxxxxyy and xxxxxyxy, have the same multiset of axis counts (six x's, two y's, zero z's) but different traces, 0 and 1. This shows the holonomy is not merely a function of how many times each axis is used, but depends on the order of the steps.

In Recognition Science, this result is part of a chain that derives physical constants. The eight-beat cycle and the three axes are not arbitrary; they are forced by the framework's foundational theorems. The exact trace values, being rational numbers, are significant because they are used in a later task to establish that the square root of 2 emerges from odd-length cascades, not from even-length ones. This distinction is a step toward deriving particle masses on a phi-power ladder.

What the declaration does not claim is that these walks represent actual physical particles or that the holonomy trace is a measurable physical quantity. It is a mathematical theorem about a specific combinatorial model. It does not claim that all closed cascades have the same trace, only that the trace falls within the five-value spectrum. It also does not claim that the order-dependence of the trace is a new physical principle; it is a property of the quaternion multiplication used in the model.

/-- The true SU(2) holonomy trace of a cascade: `trace = 2 · P.w / (√2)^n`,
restoring the `1/√2` normalization dropped in the integer product. -/
noncomputable def holonomyTrace (w : Walk) : ℝ :=
  2 * ((qProd w).w : ℝ) / (Real.sqrt 2) ^ w.length

/-- The exact rational trace of an 8-beat cascade. -/
def traceRat (w : Walk) : ℚ := (traceNum w : ℚ) / 8

/-- **Task 1(b), THEOREM (decidable computation).** Over all 1641 admissible
closed 8-beat cascades the holonomy trace numerator lands in
`{-16, -8, 0, 8, 16}`; in particular `√2` occurs zero times. -/
theorem trace_spectrum :
    closedWalks8.all (fun w => spectrumB (traceNum w)) = true := by decide

/-- The two witnesses share the axis multiset `(6 x, 2 y, 0 z)`. -/
theorem witness_same_multiset (a : Axis) : countAxis a walkA = countAxis a walkB := by
  fin_cases a <;> decide

/-- The witness traces differ: `xxxxxxyy` has trace numerator `0` (trace `0`),
`xxxxxyxy` has trace numerator `8` (trace `1`). -/
theorem witness_traces : traceNum walkA = 0 ∧ traceNum walkB = 8 :=
  ⟨by decide, by decide⟩

What this page does not claim

The walks represent actual physical particles or that the holonomy trace is a directly measurable quantity. All closed cascades have the same trace; only the five-value spectrum is proved. The order-dependence is a new physical principle; it is a property of the quaternion model.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10Beat8Holonomy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: