`brgc_oneBit_step`

proved

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCycleBRGC
domain: Patterns
line: 209 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Patterns.GrayCycleBRGC on GitHub at line 209.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 206    _ = n - (i.val + 1) := hnat
 207    _ = (Fin.rev i).val := by simpa [hR]
 208
 209theorem brgc_oneBit_step : ∀ {d : Nat}, 0 < d →
 210    ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1))
 211  | 0, hdpos => (Nat.not_lt_zero _ hdpos).elim
 212  | 1, _ => by
 213      intro i
 214      -- dimension 1: the cycle is `0 → 1 → 0`, so the only bit flips each step
 215      fin_cases i
 216      · -- 0 → 1
 217        have : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
 218          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
 219        simpa [brgcPath] using this
 220      · -- 1 → 0 (wrap), use symmetry
 221        have h : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
 222          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
 223        have : OneBitDiff (snocBit (brgcPath 0 0) true) (snocBit (brgcPath 0 0) false) :=
 224          OneBitDiff_symm h
 225        simpa [brgcPath] using this
 226  | (d + 2), _ => by
 227      -- Inductive step: assume one-bit stepping for dimension `d+1`, prove for `d+2`.
 228      have ih :
 229          ∀ i : Fin (2 ^ (d + 1)), OneBitDiff (brgcPath (d + 1) i) (brgcPath (d + 1) (i + 1)) :=
 230        brgc_oneBit_step (d := d + 1) (Nat.succ_pos _)
 231      intro i
 232      classical
 233      let T : Nat := 2 ^ (d + 1)
 234      have hTT : 2 ^ (d + 2) = T + T := by
 235        simpa [T] using twoPow_succ_eq_add (d := d + 1)
 236      let left : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) k) false
 237      let right : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) (Fin.rev k)) true
 238      let i' : Fin (T + T) := i.cast hTT
 239

papers checked against this theorem

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