Masses Mass Genesis T10 Beat8 Holonomy Holonomy Not Count Visible

The nonabelian witness

In geometry, a holonomy is the difference between where you expect to be and where you actually are after moving around a loop. Imagine carrying an arrow along a path on a curved surface: even if you return to your starting point, the arrow may point a different way. The declaration holonomy_not_count_visible concerns a discrete version of this idea, where movement happens in eight steps along the edges of a three-dimensional cube, and each step is a quarter-turn of the arrow.

The framework's library of machine-checked theorems proves a specific fact about two such eight-step paths. The paths, written as xxxxxxyy and xxxxxyxy, each use the same number of steps along each of the cube's three axes: six steps on one axis and two on another. If the final orientation depended only on these counts, the two paths would end with the arrow pointing the same way. The theorem shows they do not: the first path leaves the arrow with a trace of 0, the second with a trace of 1, where the trace is a number that records the arrow's final orientation. The transport is not count-visible; the order of the steps matters.

This result is not a numerical approximation. The library enumerates all 3^8, or 6561, possible eight-step paths and checks the claim by exact integer arithmetic, with no reliance on a compiler's floating-point shortcuts. The proof also establishes that among the 1641 closed paths, those that return to their starting point, the holonomy trace always lands in the small set {-2, -1, 0, 1, 2}. The two witness paths are both closed, so the difference in their traces is not an artifact of ending elsewhere.

Within Recognition Science, this fact is load-bearing. The framework treats the universe as storing a discrete record of recognition events, and it models a cascade of such events as a walk on a cube. The nonabelian mechanism, where the order of operations changes the outcome, is what the framework needs to generate the structure of particle masses. The declaration bundles the witness paths and their differing traces into a single certificate, a machine-checked object that the framework can carry forward into later stages of the mass-genesis derivation.

The declaration does not claim that the framework has derived the mass spectrum, nor that this holonomy fact alone explains any measured particle mass. It establishes a precise, local fact about a model of cascades: two specific paths with the same step counts have different holonomies. What that difference means for the full mass-genesis story remains a target for later work in the framework's library.

/-- **Task 1(c), THEOREM.** Same rung-and-axis multiset, different holonomy
traces: the transport is not count-visible. -/
theorem witness_not_count_visible : traceRat walkA ≠ traceRat walkB := by
  rw [witness_traceRat.1, witness_traceRat.2]
  norm_num

/-- **Task 1(a), THEOREM.** The number of admissible closed 8-beat cascades
per start vertex is exactly `1641`. -/
theorem closed_cascades_1641 : closedWalks8.length = 1641 := by decide

/-- **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

theorem witness_closed : isClosedB walkA = true ∧ isClosedB walkB = true :=
  ⟨by decide, by decide⟩

What this page does not claim

The declaration does not claim that the framework has derived any measured particle mass. The declaration does not claim that this holonomy fact alone explains the mass spectrum. The declaration does not claim that the framework's model of cascades is a physical theory of the universe.

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: