Encyclopedia Ledger Ledger Parity Adjacency Coord Atomic Step

ARTICLE 3 claims 2 theorems 1 open

Ledger Parity Adjacency Coord Atomic Step

A single unit change in one coordinate of an integer vector flips exactly one parity bit; the framework proves this as pure mathematics, not as physics.

Verify this page

The atomic step

In mathematics, a vector of integers can be pictured as a row of counters, each holding a whole number. An atomic step is the simplest possible change: add one to exactly one counter, or subtract one from exactly one counter, leaving every other counter untouched. The declaration coordAtomicStep defines this relation precisely: two vectors are connected by an atomic step when there exists a coordinate k such that the k-th entry differs by exactly one and all other entries are identical.

The classical fact this definition serves is a parity observation. Reduce each integer to its parity, odd or even, and record the result as a pattern of bits, one bit per coordinate. If two vectors differ by an atomic step, their parity patterns differ in exactly one bit. Adding one to an odd number makes it even; subtracting one from an even number makes it odd; either way, only the parity of that single coordinate changes, and every other coordinate keeps its parity. The framework's machine-checked library of formal theorems proves this as coordAtomicStep_oneBitDiff: the atomic step hypothesis forces the one-bit parity difference. The proof is a result about integer vectors, not a claim about nature.

In Recognition Science, this result is a bridge lemma, a scaffold for a larger argument. The framework models a ledger, a discrete record of events, as a state vector of integers, and models an atomic update as exactly this kind of single-coordinate unit change. The result then says that a ledger moving by atomic steps induces a parity pattern that changes by one bit at a time, a property the framework calls adjacency. The minimal packaging in LedgerVecState and ledgerVecStep makes the model explicit: a state is an integer vector, a step is coordAtomicStep, and the observation is parity.

What the declaration does not claim is just as important as what it proves. The result does not say that real ledgers, physical systems, or recognition processes actually take atomic steps. It does not assert that ledger legality or cost minimization implies the single-coordinate update hypothesis. That implication would require a separate result, one the framework explicitly flags as still open. The bridge lemma supplies the mathematical core: if the atomic step hypothesis holds, then the one-bit parity conclusion follows. Whether the hypothesis itself holds in any particular setting is a question the declaration leaves untouched.

The consequence for a reader is a clean, checkable fact: a unit change in one coordinate flips exactly one parity bit. That fact is now machine-verified, so any future argument that needs this step can cite it without re-deriving it. The declaration establishes a precise conditional, and it names the missing premise, the implication from ledger rules to atomic steps, as the next thing to prove.

THEOREM coordAtomicStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean
coordAtomicStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean:40 
theorem coordAtomicStep_oneBitDiff {d : Nat} {x y : Fin d → ℤ}
    (h : coordAtomicStep (d := d) x y) :
    OneBitDiff (parityPattern x) (parityPattern y) := by
  classical
  rcases h with ⟨k, hkstep, hrest⟩
  refine ⟨k, ?diffAtK, ?unique⟩
  · -- Parity differs at the updated coordinate because ±1 flips odd/even.
    have hxk : parityPattern x k ≠ parityPattern y k := by
      -- unfold and split ±1
      dsimp [parityPattern]
      rcases hkstep with hkplus | hkminus
      · -- yk = xk + 1
        -- Show `bodd (xk) ≠ bodd (xk+1)`
        have : Int.bodd (x k + 1) ≠ Int.bodd (x k) := by
          -- `bodd (z+1) = xor (bodd z) true`, hence toggles.
          have hb : Int.bodd (x k + 1) = xor (Int.bodd (x k)) true := by
            simpa using (Int.bodd_add (x k) 1)
          -- cases on `bodd (xk)`
          cases hbx : Int.bodd (x k) <;> simp [hb, hbx]
        -- rewrite yk and use symmetry
        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
          -- `y k = x k + 1`
          simpa [hkplus] using this.symm
        exact this
      · -- yk = xk - 1
        have : Int.bodd (x k - 1) ≠ Int.bodd (x k) := by
          -- `bodd (z-1) = bodd (z + (-1)) = xor (bodd z) (bodd (-1)) = xor (bodd z) true`
          have hb : Int.bodd (x k - 1) = xor (Int.bodd (x k)) (Int.bodd (-1)) := by
            -- `x-1 = x + (-1)`
            have : x k - 1 = x k + (-1) := by ring
            simpa [this] using (Int.bodd_add (x k) (-1))
          have hodd : Int.bodd (-1) = true := by
            -- oddness is sign-invariant and `bodd 1 = true`
            simpa using (by
              calc
                Int.bodd (-1) = Int.bodd 1 := by simpa using (Int.bodd_neg (1 : ℤ))
                _ = true := by simp)
          cases hbx : Int.bodd (x k) <;> simp [hb, hodd, hbx]
        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
          simpa [hkminus] using this.symm
        exact this
    exact hxk
  · -- Uniqueness: if parity differs at i, then i = k.
    intro i hi
    by_contra hik
    have hEq : y i = x i := hrest i hik
    -- If i ≠ k then parity is equal, contradiction.
    have : parityPattern x i = parityPattern y i := by
      simp [parityPattern, hEq]
    exact hi this
THEOREM coordAtomicStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean
coordAtomicStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean:40 
theorem coordAtomicStep_oneBitDiff {d : Nat} {x y : Fin d → ℤ}
    (h : coordAtomicStep (d := d) x y) :
    OneBitDiff (parityPattern x) (parityPattern y) := by
  classical
  rcases h with ⟨k, hkstep, hrest⟩
  refine ⟨k, ?diffAtK, ?unique⟩
  · -- Parity differs at the updated coordinate because ±1 flips odd/even.
    have hxk : parityPattern x k ≠ parityPattern y k := by
      -- unfold and split ±1
      dsimp [parityPattern]
      rcases hkstep with hkplus | hkminus
      · -- yk = xk + 1
        -- Show `bodd (xk) ≠ bodd (xk+1)`
        have : Int.bodd (x k + 1) ≠ Int.bodd (x k) := by
          -- `bodd (z+1) = xor (bodd z) true`, hence toggles.
          have hb : Int.bodd (x k + 1) = xor (Int.bodd (x k)) true := by
            simpa using (Int.bodd_add (x k) 1)
          -- cases on `bodd (xk)`
          cases hbx : Int.bodd (x k) <;> simp [hb, hbx]
        -- rewrite yk and use symmetry
        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
          -- `y k = x k + 1`
          simpa [hkplus] using this.symm
        exact this
      · -- yk = xk - 1
        have : Int.bodd (x k - 1) ≠ Int.bodd (x k) := by
          -- `bodd (z-1) = bodd (z + (-1)) = xor (bodd z) (bodd (-1)) = xor (bodd z) true`
          have hb : Int.bodd (x k - 1) = xor (Int.bodd (x k)) (Int.bodd (-1)) := by
            -- `x-1 = x + (-1)`
            have : x k - 1 = x k + (-1) := by ring
            simpa [this] using (Int.bodd_add (x k) (-1))
          have hodd : Int.bodd (-1) = true := by
            -- oddness is sign-invariant and `bodd 1 = true`
            simpa using (by
              calc
                Int.bodd (-1) = Int.bodd 1 := by simpa using (Int.bodd_neg (1 : ℤ))
                _ = true := by simp)
          cases hbx : Int.bodd (x k) <;> simp [hb, hodd, hbx]
        have : Int.bodd (x k) ≠ Int.bodd (y k) := by
          simpa [hkminus] using this.symm
        exact this
    exact hxk
  · -- Uniqueness: if parity differs at i, then i = k.
    intro i hi
    by_contra hik
    have hEq : y i = x i := hrest i hik
    -- If i ≠ k then parity is equal, contradiction.
    have : parityPattern x i = parityPattern y i := by
      simp [parityPattern, hEq]
    exact hi this

What this page does not claim

The declaration does not claim that real ledgers or physical systems take atomic steps. The declaration does not prove that ledger legality or cost minimization implies the atomic step hypothesis.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/LedgerParityAdjacency.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND