RSLedger
The rich ledger structure packages a base ledger with generation torsion offsets and sector base rungs to compute full particle rungs on the phi ladder. Physicists deriving mass ratios from geometric torsion would reference this structure when computing generation mass ratios. The definition is a straightforward record extension with an auxiliary rung function defined by addition.
claimA rich ledger consists of an underlying ledger, a map assigning an integer torsion offset to each of the three fermion generations, and a map assigning an integer base rung to each of the three fermion sectors (leptons, up quarks, down quarks). The full rung for a given sector and generation is the sum of the sector base rung and the generation torsion offset.
background
In Recognition Science, particle masses occupy discrete rungs on the phi-ladder with ratios given by powers of phi. The rich ledger augments a minimal ledger by adding a torsion function for the three generations and base rungs for the three fermion sectors. Module documentation states that torsion values derive from D=3 cube combinatorics: generation 1 at 0, generation 2 at 11, generation 3 at 17, so that rung differences directly yield the observed mass ratios phi^11, phi^17 and phi^6.
proof idea
The structure is introduced by direct record construction of its three fields. The rung accessor is defined by adding the sector base rung to the generation torsion. The rung-difference theorem follows by simplification and ring arithmetic; the canonical-torsion theorem substitutes the generation torsion function and reduces by reflexivity.
why it matters in Recognition Science
This structure supplies the data needed to derive inter-generation mass ratios as phi to the power of torsion differences, directly supporting the mass formula of yardstick times phi to the rung. It connects to the geometric derivation of torsion from cube combinatorics and realizes the phi-ladder structure required after the phi fixed point in the forcing chain. It feeds into downstream mass-ratio calculations without itself proving the torsion values.
scope and limits
- Does not prove the specific torsion values 0, 11, 17.
- Does not derive the base rungs from charge structure Z.
- Does not compute explicit numerical masses.
- Does not address the implementation of the underlying ledger.
formal statement (Lean)
113structure RSLedger where
114 /-- The underlying ledger -/
115 toLedger : Ledger
116 /-- Generation torsion offsets -/
117 torsion : Generation → ℤ
118 /-- Base rung for each sector -/
119 baseRung : FermionSector → ℤ
120
121/-- The full rung assignment for a particle -/
122def RSLedger.rung (L : RSLedger) (sector : FermionSector) (gen : Generation) : ℤ :=
proof body
Definition body.
123 L.baseRung sector + L.torsion gen
124
125/-- Rung difference between two generations in the same sector -/
126def RSLedger.rungDiff (L : RSLedger) (sector : FermionSector)
127 (g1 g2 : Generation) : ℤ :=
128 L.rung sector g1 - L.rung sector g2
129
130/-- Rung difference equals torsion difference (base rung cancels) -/
131theorem RSLedger.rungDiff_eq_torsionDiff (L : RSLedger) (sector : FermionSector)
132 (g1 g2 : Generation) :
133 L.rungDiff sector g1 g2 = L.torsion g1 - L.torsion g2 := by
134 simp only [rungDiff, rung]
135 ring
136
137/-- For canonical torsion, rung difference is generation torsion difference -/
138theorem RSLedger.rungDiff_canonical (L : RSLedger) (sector : FermionSector)
139 (g1 g2 : Generation) (hL : L.torsion = generationTorsion) :
140 L.rungDiff sector g1 g2 = torsionDiff g1 g2 := by
141 rw [rungDiff_eq_torsionDiff, hL]
142 rfl
143
144/-! ## Mass Ratios from Rung Differences -/
145
146/-- Mass ratio between generations from rung difference.
147
148This is the key derivation: masses are φ^{rung}, so ratios are φ^{Δrung}.
149-/