Encyclopedia Ledger Ledger Parity Adjacency Ledger Vec Step One Bit Diff

ARTICLE 2 claims 2 theorems

Ledger Parity Adjacency Ledger Vec Step One Bit Diff

A single change in a ledger's entries flips exactly one bit of its parity pattern, a machine-checked bridge between discrete states and their observable patterns.

Verify this page

One-bit adjacency

A ledger is a discrete record of events, and in Recognition Science a state of that record is modeled as a vector of integers, one entry per coordinate. The declaration ledgerVecStep_oneBitDiff proves a simple fact about such vectors: if you change exactly one coordinate by adding or subtracting 1, then the parity pattern, the odd-or-even status of each entry, changes in exactly one bit. The theorem is a statement about integer vectors and parity, not a claim about nature.

The proof is direct. The definition coordAtomicStep states the hypothesis: one coordinate changes by ±1, all others stay fixed. The definition parityPattern maps each integer to a Boolean, true for odd, false for even. The theorem coordAtomicStep_oneBitDiff shows that under the atomic step, the two parity patterns differ in exactly one position. The declaration ledgerVecStep_oneBitDiff packages this result for the minimal ledger-vector model, where the state is the vector and the step is the atomic update.

The theorem does not claim that real ledgers obey this step rule. It does not prove that Recognition Science's cost-minimization forces such single-coordinate updates. That would require a separate theorem linking ledger legality and cost to the atomic-step hypothesis. The bridge lemma is a scaffold, not the full bridge.

THEOREM ledgerVecStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean
ledgerVecStep_oneBitDiff · IndisputableMonolith/LedgerParityAdjacency.lean:105 
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)
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

This does not claim that real ledgers obey the atomic step rule. This does not claim that Recognition Science forces single-coordinate updates from its cost function. This does not claim that the parity pattern is the only observable of a ledger state.

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