`generationTorsion`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.RSLedger on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  56
  57No raw numerals: every branch is a cube-combinatorial function of D=3.
  58-/
  59def generationTorsion : Generation → ℤ
  60  | .first => 0
  61  | .second => (passive_field_edges D : ℤ)
  62  | .third => (passive_field_edges D + cube_faces D : ℤ)
  63
  64@[simp] lemma torsion_first : generationTorsion .first = 0 := rfl
  65
  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

papers checked against this theorem

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