grayCover_eight_tick_min

formal source

  68theorem grayCover_min_ticks {d T : Nat} [NeZero T] (w : GrayCover d T) : 2 ^ d ≤ T :=
  69  Patterns.min_ticks_cover (d := d) (T := T) w.path w.complete
  70
  71theorem grayCover_eight_tick_min {T : Nat} [NeZero T] (w : GrayCover 3 T) : 8 ≤ T := by
  72  simpa using (Patterns.eight_tick_min (T := T) w.path w.complete)
  73
  74/-!
  75### A fully explicit, fully decidable 3-bit witness (the actual “octave”)
  76
  77This gives a *rigorous* Gray cycle for `d=3` (period 8) without any axioms.
  78We deliberately start here because it is the “octave” case used throughout RS.
  79-/
  80
  81/-- Convert a `Fin 8` codeword into a 3-bit pattern via `testBit`. -/
  82def pattern3 : Fin 8 → Pattern 3
  83| ⟨0, _⟩ => fun _ => false
  84| ⟨1, _⟩ => fun j => decide (j.val = 0)
  85| ⟨2, _⟩ => fun j => decide (j.val = 1)
  86| ⟨3, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 1)
  87| ⟨4, _⟩ => fun j => decide (j.val = 2)
  88| ⟨5, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 2)
  89| ⟨6, _⟩ => fun j => decide (j.val = 1 ∨ j.val = 2)
  90| ⟨7, _⟩ => fun _ => true
  91
  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