pith. machine review for the scientific record. sign in
theorem proved term proof

grayCover_eight_tick_min

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  71theorem grayCover_eight_tick_min {T : Nat} [NeZero T] (w : GrayCover 3 T) : 8 ≤ T := by

proof body

Term-mode proof.

  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`. -/

depends on (20)

Lean names referenced from this declaration's body.