pith. machine review for the scientific record. sign in
structure definition def or abbrev

RSLedger

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more