structure
definition
RSLedger
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.RSLedger on GitHub at line 113.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
110- Sector base rungs
111- Full rung assignment
112-/
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) : ℤ :=
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