IndisputableMonolith.Patterns.GrayCycle

   1import Mathlib
   2import IndisputableMonolith.Patterns
   3
   4/-!
   5# GrayCycle: a Hamiltonian cycle on the hypercube (adjacency + closure)
   6
   7This module upgrades the existing `Patterns` counting/coverage facts to an
   8explicit **adjacent** cycle notion:
   9
  10- state space: `Pattern d := Fin d → Bool`
  11- adjacency: patterns differ in exactly one coordinate
  12- cycle: a length-`2^d` closed walk visiting all patterns exactly once
  13
  14Why this matters (RS context)
  15----------------------------
  16`Patterns.period_exactly_8` proves a *cardinality/coverage* fact: there exists a
  17surjection `Fin 8 → Pattern 3`. That is enough to certify the `2^D` counting bound,
  18but it does not encode "one-bit" (Gray) adjacency.
  19
  20`GrayCycle` is the stronger object needed to align the "ledger-compatible adjacency"
  21story with a formal definition.
  22
  23Status note
  24-----------
  25This module is self-contained and does **not** rely on the Gray-code axioms in
  26`Patterns/GrayCodeAxioms.lean`. It uses the standard recursive BRGC construction.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Patterns
  31
  32open Classical
  33
  34/-! ## Basic definitions -/
  35
  36/-- Two patterns differ in exactly one coordinate (the Hamming distance is 1). -/
  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
  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
 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
 126theorem pattern3_injective : Function.Injective pattern3 := by
 127  intro a b hab
 128  apply Fin.ext
 129  have hNat : toNat3 (pattern3 a) = toNat3 (pattern3 b) := congrArg toNat3 hab
 130  simpa [toNat3_pattern3] using hNat
 131
 132theorem grayCycle3_injective : Function.Injective grayCycle3Path := by
 133  intro i j hij
 134  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
 135  exact gray8At_injective h0
 136
 137theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
 138  classical
 139  -- card(Fin 8) = 8
 140  have hFin : Fintype.card (Fin 8) = 8 := by simp
 141  -- card(Pattern 3) = 2^3 = 8
 142  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
 143    simpa using (Patterns.card_pattern 3)
 144  have hPow : (2 ^ 3 : Nat) = 8 := by decide
 145  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
 146  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
 147    -- rewrite both sides to 8
 148    calc
 149      Fintype.card (Fin 8) = 8 := hFin
 150      _ = Fintype.card (Pattern 3) := by simpa [hPat]
 151  -- injective + card equality ⇒ bijective
 152  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩
 153
 154theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
 155  (grayCycle3_bijective).2
 156
 157theorem grayCycle3_oneBit_step : ∀ i : Fin 8, OneBitDiff (grayCycle3Path i) (grayCycle3Path (i + 1)) := by
 158  intro i
 159  -- 8 explicit cases; each step flips exactly one of the three bits.
 160  fin_cases i
 161  · -- 0 -> 1 (flip bit 0)
 162    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 163    · simp [grayCycle3Path, gray8At, pattern3]
 164    · intro k hk
 165      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 166  · -- 1 -> 3 (flip bit 1)
 167    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
 168    · simp [grayCycle3Path, gray8At, pattern3]
 169    · intro k hk
 170      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 171  · -- 2 -> 3?  (i=2 means gray8At 2 = 3, next is gray8At 3 = 2; flip bit 0)
 172    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 173    · simp [grayCycle3Path, gray8At, pattern3]
 174    · intro k hk
 175      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 176  · -- i=3: 2 -> 6 (flip bit 2)
 177    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
 178    · simp [grayCycle3Path, gray8At, pattern3]
 179    · intro k hk
 180      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 181  · -- i=4: 6 -> 7 (flip bit 0)
 182    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 183    · simp [grayCycle3Path, gray8At, pattern3]
 184    · intro k hk
 185      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 186  · -- i=5: 7 -> 5 (flip bit 1)
 187    refine ⟨⟨1, by decide⟩, ?_, ?_⟩
 188    · simp [grayCycle3Path, gray8At, pattern3]
 189    · intro k hk
 190      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 191  · -- i=6: 5 -> 4 (flip bit 0)
 192    refine ⟨⟨0, by decide⟩, ?_, ?_⟩
 193    · simp [grayCycle3Path, gray8At, pattern3]
 194    · intro k hk
 195      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 196  · -- i=7: 4 -> 0 (wrap; flip bit 2)
 197    refine ⟨⟨2, by decide⟩, ?_, ?_⟩
 198    · simp [grayCycle3Path, gray8At, pattern3]
 199    · intro k hk
 200      fin_cases k <;> simp [grayCycle3Path, gray8At, pattern3] at hk ⊢
 201
 202/-- A rigorous Gray cycle for 3-bit patterns (the “8-tick” cycle). -/
 203def grayCycle3 : GrayCycle 3 :=
 204{ path := grayCycle3Path
 205, inj := grayCycle3_injective
 206, oneBit_step := grayCycle3_oneBit_step
 207}
 208
 209theorem grayCycle3_period : (2 ^ 3) = 8 := by decide
 210
 211/-- The 3-bit Gray cycle can be viewed as a GrayCover of period 8. -/
 212def grayCover3 : GrayCover 3 8 :=
 213{ path := grayCycle3Path
 214, complete := grayCycle3_surjective
 215, oneBit_step := grayCycle3_oneBit_step
 216}
 217
 218end Patterns
 219end IndisputableMonolith
 220