Ledger Parity Adjacency Ledger Vec Parity

One-bit parity steps

A row of counters, each holding an integer. Mark each counter as odd or even. Now change exactly one counter by adding or subtracting one. The theorem says your odd-or-even pattern changes in exactly one position: the counter you touched flips its parity, and every other counter keeps its mark. That is the entire content of the declaration ledgerVecParity in the Recognition Science library.

The statement is a pure fact about integer vectors and parity, proved in the machine-checked library of formal theorems. It defines a ledger-like state as a vector of integers, an atomic step as changing one coordinate by plus or minus one, and the observation as the parity pattern. The theorem then derives that an atomic step produces exactly a one-bit difference in the parity pattern. The proof is short and direct, a bridge lemma scaffold for a larger workstream.

In Recognition Science, the framework models a ledger as a discrete record of events. The theorem is a mathematical core: if a ledger-like state changes by a single atomic plus-or-minus-one update in exactly one coordinate, then the induced parity pattern changes in exactly one bit. It is a statement about the algebra of integers, not about nature.

The declaration does not claim that real ledgers obey this rule. Turning the theorem into a physical claim would require a separate, unproved hypothesis: that ledger legality plus cost-minimization forces the single-coordinate update. That step remains open. The theorem only establishes the conditional link between the atomic update and the one-bit parity change.

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

No claim that real ledgers or physical states obey the single-coordinate update rule. No derivation that ledger constraints imply adjacency without a separate unproved hypothesis. No statement about the cost function or the forcing chain; this theorem is purely about integer parity.

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: