`TickIndex`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.ThreeGenerations
domain: Physics
line: 50 · 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 50.

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

used by

formal source

  47/-! ## The 8-Tick Structure -/
  48
  49/-- The 8-tick cycle, indexed by Fin 8 = Fin 2³. -/
  50abbrev TickIndex := Fin 8
  51
  52/-- Decompose a tick index into 3 bits (one per dimension). -/
  53def tickToBits (t : TickIndex) : Fin 2 × Fin 2 × Fin 2 :=
  54  (⟨t.val % 2, Nat.mod_lt _ (by norm_num)⟩,
  55   ⟨(t.val / 2) % 2, Nat.mod_lt _ (by norm_num)⟩,
  56   ⟨(t.val / 4) % 2, Nat.mod_lt _ (by norm_num)⟩)
  57
  58/-- Reconstruct tick index from 3 bits. -/
  59def bitsToTick (b : Fin 2 × Fin 2 × Fin 2) : TickIndex :=
  60  ⟨b.1.val + 2 * b.2.1.val + 4 * b.2.2.val, by
  61    have h1 : b.1.val < 2 := b.1.isLt
  62    have h2 : b.2.1.val < 2 := b.2.1.isLt
  63    have h3 : b.2.2.val < 2 := b.2.2.isLt
  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

papers checked against this theorem

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