`torsion_third`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.RSLedger on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  66@[simp] lemma torsion_second : generationTorsion .second = 11 := by
  67  simp [generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, D]
  68
  69@[simp] lemma torsion_third : generationTorsion .third = 17 := by
  70  simp [generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]
  71
  72/-- Torsion difference between generations -/
  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 → ℤ

papers checked against this theorem

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