coordAtomicStep_oneBitDiff

formal source

  37
  38/-! ## Core theorem: atomic coordinate update ⇒ one-bit parity difference -/
  39
  40theorem coordAtomicStep_oneBitDiff {d : Nat} {x y : Fin d → ℤ}
  41    (h : coordAtomicStep (d := d) x y) :
  42    OneBitDiff (parityPattern x) (parityPattern y) := by
  43  classical
  44  rcases h with ⟨k, hkstep, hrest⟩
  45  refine ⟨k, ?diffAtK, ?unique⟩
  46  · -- Parity differs at the updated coordinate because ±1 flips odd/even.
  47    have hxk : parityPattern x k ≠ parityPattern y k := by
  48      -- unfold and split ±1
  49      dsimp [parityPattern]
  50      rcases hkstep with hkplus | hkminus
  51      · -- yk = xk + 1
  52        -- Show `bodd (xk) ≠ bodd (xk+1)`
  53        have : Int.bodd (x k + 1) ≠ Int.bodd (x k) := by
  54          -- `bodd (z+1) = xor (bodd z) true`, hence toggles.
  55          have hb : Int.bodd (x k + 1) = xor (Int.bodd (x k)) true := by
  56            simpa using (Int.bodd_add (x k) 1)
  57          -- cases on `bodd (xk)`
  58          cases hbx : Int.bodd (x k) <;> simp [hb, hbx]
  59        -- rewrite yk and use symmetry
  60        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
  61          -- `y k = x k + 1`
  62          simpa [hkplus] using this.symm
  63        exact this
  64      · -- yk = xk - 1
  65        have : Int.bodd (x k - 1) ≠ Int.bodd (x k) := by
  66          -- `bodd (z-1) = bodd (z + (-1)) = xor (bodd z) (bodd (-1)) = xor (bodd z) true`
  67          have hb : Int.bodd (x k - 1) = xor (Int.bodd (x k)) (Int.bodd (-1)) := by
  68            -- `x-1 = x + (-1)`
  69            have : x k - 1 = x k + (-1) := by ring
  70            simpa [this] using (Int.bodd_add (x k) (-1))