`Generation`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.ThreeGenerations
domain: Physics
line: 77 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.ThreeGenerations on GitHub at line 77.

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

  74
  75/-- A generation is characterized by the parity pattern across dimensions.
  76    We define 3 "generation modes" from the bit patterns. -/
  77inductive Generation where
  78  | first : Generation   -- Pattern: (0,0,*) or (1,1,*)
  79  | second : Generation  -- Pattern: (0,1,*) or (1,0,*)
  80  | third : Generation   -- Pattern: special cases
  81deriving DecidableEq, Repr
  82
  83/-- Number of generations is exactly 3. -/
  84theorem three_generations : (List.length [Generation.first, Generation.second, Generation.third]) = 3 := rfl
  85
  86/-! ## The 3 from 8 = 2³ Argument -/
  87
  88/-- The key insight: 8 = 2³ gives us 3 "independent directions" in tick-space.
  89    Each direction corresponds to one generation. -/
  90def dimensionsFromTicks : ℕ := 3  -- log₂(8) = 3
  91
  92/-- **THEOREM**: The number of dimensions equals log₂(8). -/
  93theorem dimensions_from_log : dimensionsFromTicks = Nat.log 2 8 := by
  94  native_decide
  95
  96/-- The correspondence:
  97    - Dimension 0 (x) ↔ Generation 1 (lightest)
  98    - Dimension 1 (y) ↔ Generation 2 (medium)
  99    - Dimension 2 (z) ↔ Generation 3 (heaviest)
 100
 101    This is a structural correspondence, not a dynamical one. -/
 102def dimensionToGeneration : Fin 3 → Generation
 103  | 0 => Generation.first
 104  | 1 => Generation.second
 105  | 2 => Generation.third
 106
 107/-! ## Mass Hierarchy -/

papers checked against this theorem

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