  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
  81deriving DecidableEq, Repr
  82
  83/-- Number of generations is exactly 3. -/

papers checked against this theorem

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