OneBitDiff_symm

formal source

  37def OneBitDiff {d : Nat} (p q : Pattern d) : Prop :=
  38  ∃! k : Fin d, p k ≠ q k
  39
  40lemma OneBitDiff_symm {d : Nat} {p q : Pattern d} :
  41    OneBitDiff p q → OneBitDiff q p := by
  42  intro h
  43  rcases h with ⟨k, hk, hkuniq⟩
  44  refine ⟨k, ?_, ?_⟩
  45  · simpa [ne_comm] using hk
  46  · intro k' hk'
  47    -- rewrite hk' as p k' ≠ q k' to use uniqueness
  48    have hk'' : p k' ≠ q k' := by simpa [ne_comm] using hk'
  49    exact hkuniq k' hk''
  50
  51/-! ## The GrayCycle structure (adjacency + wrap-around) -/
  52
  53structure GrayCycle (d : Nat) where
  54  /-- Phase-indexed path through patterns (period is fixed to `2^d`). -/
  55  path : Fin (2 ^ d) → Pattern d
  56  /-- No repeats (Hamiltonian cycle candidate). -/
  57  inj : Function.Injective path
  58  /-- Consecutive phases differ in exactly one bit (with wrap-around). -/
  59  oneBit_step : ∀ i : Fin (2 ^ d), OneBitDiff (path i) (path (i + 1))
  60
  61/-- A Gray *cover* with an arbitrary period `T`: adjacency (one-bit steps) plus coverage (surjection). -/
  62structure GrayCover (d T : Nat) [NeZero T] where
  63  path : Fin T → Pattern d
  64  complete : Function.Surjective path
  65  oneBit_step : ∀ i : Fin T, OneBitDiff (path i) (path (i + 1))
  66
  67/-! Minimality: any cover of all `d`-bit patterns needs at least `2^d` ticks. -/
  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