parityPattern

formal source

  24/-! ## Parity projection -/
  25
  26/-- Parity (odd/even) as a `Pattern d` (a Bool at each coordinate). -/
  27def parityPattern {d : Nat} (x : Fin d → ℤ) : Pattern d :=
  28  fun i => Int.bodd (x i)
  29
  30/-! ## “Atomic coordinate update” hypothesis -/
  31
  32/-- `y` is obtained from `x` by changing exactly one coordinate by ±1. -/
  33def coordAtomicStep {d : Nat} (x y : Fin d → ℤ) : Prop :=
  34  ∃ k : Fin d,
  35    (y k = x k + 1 ∨ y k = x k - 1) ∧
  36    (∀ i : Fin d, i ≠ k → y i = x i)
  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)`