coordAtomicStep_oneBitDiff

proof body

Tactic-mode proof.

  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))
  71          have hodd : Int.bodd (-1) = true := by
  72            -- oddness is sign-invariant and `bodd 1 = true`
  73            simpa using (by
  74              calc
  75                Int.bodd (-1) = Int.bodd 1 := by simpa using (Int.bodd_neg (1 : ℤ))
  76                _ = true := by simp)
  77          cases hbx : Int.bodd (x k) <;> simp [hb, hodd, hbx]
  78        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
  79          simpa [hkminus] using this.symm
  80        exact this
  81    exact hxk
  82  · -- Uniqueness: if parity differs at i, then i = k.
  83    intro i hi
  84    by_contra hik
  85    have hEq : y i = x i := hrest i hik
  86    -- If i ≠ k then parity is equal, contradiction.
  87    have : parityPattern x i = parityPattern y i := by
  88      simp [parityPattern, hEq]
  89    exact hi this
  90
  91/-! ## Minimal “ledger vector” model (B1-style packaging) -/
  92
  93/-- A minimal ledger-state model: state is an integer vector, step is `coordAtomicStep`,
  94and the observation is parity. -/