coordAtomicStep_oneBitDiff
If vector y differs from x by exactly one coordinate changed by ±1, then the parity patterns of x and y differ in exactly one bit. Ledger and cellular-automaton proofs cite this result to convert atomic updates into one-bit adjacency statements. The proof splits on the sign of the update, invokes the bodd toggle property for ±1, and closes uniqueness by contradiction on any other differing index.
claimIf $y$ is obtained from $x$ by changing exactly one coordinate by $+1$ or $-1$, then the parity vectors (componentwise odd/even) of $x$ and $y$ differ in precisely one position.
background
The module supplies the mathematical core of Workstream B2: a ledger-like integer vector changes by a single atomic ±1 update in one coordinate if and only if its parity pattern (the vector of Int.bodd values) changes in exactly one bit. coordAtomicStep is the predicate asserting that y differs from x at precisely one index k by ±1 while all other coordinates remain fixed. parityPattern maps each coordinate to its parity bit. OneBitDiff asserts that two vectors differ at exactly one index. The local setting is a minimal ledger-state model whose steps are required to be atomic coordinate updates; turning this into a physical claim still needs a separate theorem that RS ledger legality forces such atomic steps.
proof idea
The tactic proof begins with classical and rcases on the coordAtomicStep hypothesis to extract the changed index k and the sign of the update. It then splits into two cases. For +1 it applies Int.bodd_add to obtain the toggle bodd(z+1) = xor (bodd z) true and rewrites to show the parities differ at k. For -1 it rewrites z-1 as z+(-1), again uses bodd_add together with bodd(-1)=true, and obtains the same toggle. Uniqueness is proved by contradiction: if another index i differs in parity then the rest hypothesis forces y i = x i, hence equal parities, contradicting the OneBitDiff assumption.
why it matters in Recognition Science
The result is invoked directly by ledgerVecStep_oneBitDiff (which lifts it to LedgerVecState) and by parity_oneBitDiff_of_post (which reduces a unit debit/credit post to an atomic coordinate step). It therefore supplies the central bridge lemma for the B2 adjacency scaffold: atomic ledger updates imply one-bit parity flips. In the Recognition framework this supports the claim that ledger legality plus cost minimization yields adjacency in the parity graph, a prerequisite for the eight-tick octave and D=3 spatial structure. No open scaffolding remains inside this file.
scope and limits
- Does not assert that every ledger step is an atomic coordinate update.
- Does not address non-integer coordinates or non-vector states.
- Does not derive physical constants, phi-ladder masses, or the alpha band.
- Does not prove the converse implication from one-bit parity difference to atomic update.
Lean usage
simpa [ledgerVecStep, ledgerVecParity] using (coordAtomicStep_oneBitDiff (d := d) (x := x) (y := y) h)formal statement (Lean)
40theorem coordAtomicStep_oneBitDiff {d : Nat} {x y : Fin d → ℤ}
41 (h : coordAtomicStep (d := d) x y) :
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. -/