`torsion_diff_21`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.RSLedger
domain: RecogSpec
line: 76 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.RSLedger on GitHub at line 76.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

torsionDiff IndisputableMonolith.RecogSpec.RSLedger

formal source

  73def torsionDiff (g1 g2 : Generation) : ℤ :=
  74  generationTorsion g1 - generationTorsion g2
  75
  76@[simp] lemma torsion_diff_21 : torsionDiff .second .first = 11 := by
  77  simp [torsionDiff]
  78
  79@[simp] lemma torsion_diff_31 : torsionDiff .third .first = 17 := by
  80  simp [torsionDiff]
  81
  82@[simp] lemma torsion_diff_32 : torsionDiff .third .second = 6 := by
  83  simp [torsionDiff]
  84
  85/-! ## Fermion Sectors -/
  86
  87/-- The three fermion sectors -/
  88inductive FermionSector : Type
  89  | leptons | upQuarks | downQuarks
  90  deriving DecidableEq, Repr
  91
  92/-- Base rung for each sector.
  93
  94These are derived from the charge structure Z:
  95- Leptons: base = 2
  96- Up quarks: base = 4
  97- Down quarks: base = 4
  98-/
  99def sectorBaseRung : FermionSector → ℤ
 100  | .leptons => 2
 101  | .upQuarks => 4
 102  | .downQuarks => 4
 103
 104/-! ## RSLedger Structure -/
 105
 106/-- A ledger with the full φ-tier structure needed for mass derivation.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.