Ledger Parity Adjacency

The one-bit bridge

In mathematics and computer science, a ledger (a discrete record of events) is often modeled as a vector of integers, where each coordinate counts something. The parity of such a vector is the pattern of odd and even numbers at each position. Ledger parity adjacency is the relationship between two ledger states whose parity patterns differ in exactly one bit. The core question is simple: if a ledger changes in the smallest possible way, how does its parity pattern change?

The answer, proved as a theorem in the framework's machine-checked library of formal theorems, is that a single atomic update changes the parity in exactly one bit. An atomic update means changing exactly one coordinate by plus or minus one, leaving all others untouched. The theorem, named coordAtomicStep_oneBitDiff, states this for any dimension d. The proof is direct: adding or subtracting one to an integer flips its parity, and since only one coordinate changes, only that coordinate's parity bit flips. This is a theorem about integer vectors, not yet a claim about physical reality.

The framework also packages this result in a minimal ledger-vector model. A state is an integer vector, a step is an atomic coordinate update, and the observation is the parity pattern. The theorem ledgerVecStep_oneBitDiff restates the result in this model. This packaging is a definitional choice, a MODEL, not a new theorem. The model shows how the core theorem fits into a ledger-like setting, but it does not add physical content.

In Recognition Science, this theorem is a bridge lemma for a larger goal. The framework aims to show that ledger constraints imply adjacency, meaning that legal ledger states form a connected graph under single-coordinate updates. This theorem proves the parity half of that bridge: if the update hypothesis holds, the parity adjacency follows. The other half, proving that ledger legality and cost-minimization force the single-coordinate update hypothesis, remains open. The theorem is a clean, proved step, not the whole journey.

The practical consequence is a sharp, checkable fact: in any system modeled as an integer vector, the smallest possible change produces the smallest possible change in the odd-even pattern. This is a useful invariant for reasoning about discrete state spaces, independent of any particular physical interpretation. It is a theorem about the mathematics of parity, with a clear condition and a clear conclusion.

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 ledgerVecStep_oneBitDiff {d : Nat} {x y : LedgerVecState d} (h : ledgerVecStep d x y) :
    OneBitDiff (ledgerVecParity d x) (ledgerVecParity d y) := by
  simpa [ledgerVecStep, ledgerVecParity] using
    (coordAtomicStep_oneBitDiff (d := d) (x := x) (y := y) h)

What this page does not claim

The theorem does not prove that real ledgers obey the single-coordinate update hypothesis. The theorem does not establish any physical adjacency in Recognition Science. The minimal ledger-vector model is a definition, not a claim about nature.

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: