`Generation`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.RSLedger on GitHub at line 47.

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

  44/-! ## Generation Torsion -/
  45
  46/-- The three generations of fermions -/
  47inductive Generation : Type
  48  | first | second | third
  49  deriving DecidableEq, Repr, Inhabited
  50
  51/-- Canonical generation torsion from Q₃ cube geometry.
  52
  53- Gen 1 (ground state): τ = 0
  54- Gen 2 (passive-edge mode): τ = passive_field_edges(D) = 11
  55- Gen 3 (passive-edge + face mode): τ = passive_field_edges(D) + cube_faces(D) = 17
  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]

papers checked against this theorem

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