brgc_oneBit_step

formal source

 230    simpa [hi_inv, hj_inv] using this
 231  exact Fin.ext this
 232
 233lemma brgc_oneBit_step {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 234    ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1)) := by
 235  intro i
 236  classical
 237  -- split on whether `i.val + 1 < 2^d` (no wrap) or wrap case
 238  by_cases hstep : i.val + 1 < 2 ^ d
 239  · -- Use the Gray-code one-bit property at the Nat level.
 240    rcases GrayCodeAxioms.gray_code_one_bit_property (d := d) (n := i.val) hstep with
 241      ⟨k, hk, hkuniq⟩
 242    have hklt : k < d := hk.1
 243    let kk : Fin d := ⟨k, hklt⟩
 244    refine ⟨kk, ?diff, ?uniq⟩
 245    · -- Show the bit differs at coordinate kk.
 246      haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
 247      have hval : (i + 1).val = i.val + 1 :=
 248        Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
 249      dsimp [brgcPath, binaryReflectedGray, natToGray, kk]
 250      simpa [hval] using hk.2
 251    · intro j hj
 252      -- Uniqueness: any differing coordinate must be kk.
 253      haveI : NeZero (2 ^ d) := ⟨pow_ne_zero d (by decide : (2 : Nat) ≠ 0)⟩
 254      have hval : (i + 1).val = i.val + 1 :=
 255        Fin.val_add_one_of_lt' (n := 2 ^ d) (i := i) hstep
 256      have hjnat :
 257          ((i.val ^^^ (i.val >>> 1)).testBit j.val) ≠
 258            (((i.val + 1) ^^^ ((i.val + 1) >>> 1)).testBit j.val) := by
 259        dsimp [brgcPath, binaryReflectedGray, natToGray] at hj
 260        simpa [hval] using hj
 261      have : (j.val : Nat) = k := by
 262        exact hkuniq j.val ⟨j.isLt, hjnat⟩
 263      apply Fin.ext