  92/-- Canonical 3-bit Gray order as a function `Fin 8 → Fin 8`.
  93
  94Sequence: [0,1,3,2,6,7,5,4]. -/
  95def gray8At : Fin 8 → Fin 8
  96| ⟨0, _⟩ => 0
  97| ⟨1, _⟩ => 1
  98| ⟨2, _⟩ => 3
  99| ⟨3, _⟩ => 2
 100| ⟨4, _⟩ => 6
 101| ⟨5, _⟩ => 7
 102| ⟨6, _⟩ => 5
 103| ⟨7, _⟩ => 4
 104
 105/-- The 3-bit Gray-cycle path (period 8). -/
 106def grayCycle3Path : Fin 8 → Pattern 3 :=
 107  fun i => pattern3 (gray8At i)
 108
 109theorem gray8At_injective : Function.Injective gray8At := by
 110  intro i j h
 111  -- brute-force on the 8 cases
 112  fin_cases i <;> fin_cases j <;> cases h <;> rfl
 113
 114/-! ## A small helper: 3-bit patterns can be re-encoded as a Nat in [0,8) -/
 115
 116/-- Convert a 3-bit pattern to a Nat by the usual binary expansion. -/
 117def toNat3 (p : Pattern 3) : ℕ :=
 118  (if p ⟨0, by decide⟩ then 1 else 0) +
 119  (if p ⟨1, by decide⟩ then 2 else 0) +
 120  (if p ⟨2, by decide⟩ then 4 else 0)
 121
 122lemma toNat3_pattern3 (w : Fin 8) : toNat3 (pattern3 w) = w.val := by
 123  -- Only 8 cases; compute directly.
 124  fin_cases w <;> decide
 125

papers checked against this theorem

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