`bits_bijection`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.ThreeGenerations on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  64    omega⟩
  65
  66/-- **THEOREM**: Bit decomposition is bijective. -/
  67theorem bits_bijection (t : TickIndex) : bitsToTick (tickToBits t) = t := by
  68  simp [tickToBits, bitsToTick]
  69  ext
  70  simp
  71  omega
  72
  73/-! ## Generation from Dimensional Parity -/
  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)

papers checked against this theorem

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