Ledger Parity Adjacency Ledger Vec Step

A one-bit step

A ledger, in the plainest sense, is a discrete record of events. Think of a row of counters, each holding an integer count. The Recognition Science declaration ledgerVecStep models one kind of change to such a record: exactly one counter moves by either plus one or minus one, and every other counter stays fixed. That is the entire definition. It is a mathematical object, an integer vector with a single coordinate adjusted by one.

The theorem attached to this definition is about parity, the odd-or-even character of each counter. If a ledger state changes by this single atomic step, then the pattern of odd and even entries changes in exactly one position. One counter flips from odd to even or even to odd; the rest keep their parity. The machine-checked library of formal theorems proves this as ledgerVecStep_oneBitDiff. The proof is short: it reduces the statement to the more general theorem coordAtomicStep_oneBitDiff, which says the same thing for any integer vector, not just the ledger-shaped one.

The declaration itself is only a packaging. It renames the general atomic-step relation to a ledger-flavored name and attaches the parity observation. It adds no new mathematics. What it establishes is a bridge lemma: a small, certain fact that connects a discrete record to a one-bit adjacency structure. The word adjacency here means two patterns differ in exactly one bit, a relation that shows up in coding theory and graph theory as the Hamming distance of one.

What the declaration does not claim is just as important. It does not say that real ledgers, or any physical system, actually evolve by such single-coordinate steps. That would require a separate theorem connecting ledger legality and cost-minimization to this atomic-update hypothesis. The library's own documentation is explicit on this point. The theorem is about integer vectors and parity, not about nature. It is a tool, not a law.

The payoff is a clean, checkable fact: a one-unit change in one coordinate produces a one-bit change in the parity pattern. This is the kind of lemma that lets a larger framework reason about discrete state spaces without re-proving the arithmetic each time. It gives a concrete, minimal example of how a ledger-like structure can induce a simple adjacency relation, and it does so with a proof that any reader can verify line by line.

/-- The canonical atomic step relation on a ledger-vector state. -/
abbrev ledgerVecStep (d : Nat) : LedgerVecState d → LedgerVecState d → Prop :=
  fun x y => coordAtomicStep (d := d) x y

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 {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 evolve by single-coordinate steps. The declaration does not claim that ledger constraints alone imply adjacency; a separate theorem is required. The declaration does not claim anything about the cost function or the forcing chain.

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: