IndisputableMonolith.LedgerParityAdjacency

   1import Mathlib
   2import IndisputableMonolith.Patterns.GrayCycle
   3
   4/-!
   5# Ledger → Parity → One-Bit Adjacency (bridge lemma scaffold)
   6
   7This file implements the **mathematical core** of Workstream B2:
   8
   9> If a ledger-like state changes by a *single atomic ±1 update in exactly one coordinate*,
  10> then the induced parity pattern (mod 2 / odd-even) changes in **exactly one bit**.
  11
  12Claim hygiene:
  13- This is a **THEOREM** about integer vectors and parity, not a claim about nature.
  14- Turning this into “ledger constraints ⇒ adjacency” still requires a *separate* theorem that
  15  RS ledger legality + cost-minimization implies the “single-coordinate ±1 update” hypothesis.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace LedgerParityAdjacency
  20
  21open Classical
  22open IndisputableMonolith.Patterns
  23
  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)`
  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. -/
  95abbrev LedgerVecState (d : Nat) : Type := Fin d → ℤ
  96
  97/-- The canonical atomic step relation on a ledger-vector state. -/
  98abbrev ledgerVecStep (d : Nat) : LedgerVecState d → LedgerVecState d → Prop :=
  99  fun x y => coordAtomicStep (d := d) x y
 100
 101/-- The canonical parity observation on a ledger-vector state. -/
 102abbrev ledgerVecParity (d : Nat) : LedgerVecState d → Pattern d :=
 103  fun x => parityPattern x
 104
 105theorem ledgerVecStep_oneBitDiff {d : Nat} {x y : LedgerVecState d} (h : ledgerVecStep d x y) :
 106    OneBitDiff (ledgerVecParity d x) (ledgerVecParity d y) := by
 107  simpa [ledgerVecStep, ledgerVecParity] using
 108    (coordAtomicStep_oneBitDiff (d := d) (x := x) (y := y) h)
 109
 110end LedgerParityAdjacency
 111end IndisputableMonolith
 112