Ledger Parity Adjacency Parity Pattern

Parity as a one-bit fingerprint

Parity is the oldest binary distinction in arithmetic: a number is either odd or even. The declaration parityPattern lifts that idea from single numbers to whole vectors. Given a vector of integers, it reads each coordinate and writes down a Boolean value, true for odd and false for even. The result is a pattern, a string of bits with one entry per coordinate. This is a definition, a choice of how to observe a vector, not a claim about the world.

The definition earns its keep through a theorem about change. Suppose one vector becomes another by changing exactly one coordinate, and only by adding or subtracting 1. The theorem, proved in the machine-checked library of formal theorems, states that the parity pattern changes in exactly one bit. Adding 1 flips odd to even or even to odd, and subtracting 1 does the same, while every untouched coordinate keeps its parity. So a single atomic step in the vector produces a single-bit difference in the pattern. The proof is short and mechanical, and it holds for any dimension.

The idea matters because it gives a clean bridge between two vocabularies. A ledger, a discrete record of events, can be modeled as a vector of integer counts. A step in that ledger, one event changing one count by one, then corresponds to a one-bit change in the observable parity pattern. This is the mathematical core of a planned bridge: it connects the fine-grained world of integer updates to the coarse-grained world of bit patterns. The connection is exact, but it is also narrow.

In Recognition Science, this theorem is a scaffold, not a finished wall. The library proves the implication from atomic coordinate update to one-bit parity difference. It does not prove that a real ledger must obey that atomic update rule. That separate step, showing that ledger legality and cost minimization force the single-coordinate update, remains a target. The theorem is about integer vectors and parity, and it makes no claim about nature on its own.

What the reader can now see is a precise, checkable fact: a one-step change in a vector leaves a one-bit fingerprint in its parity pattern. This is the kind of small, solid result that larger structures can be built on, once the additional premises are supplied and proved.

/-- Parity (odd/even) as a `Pattern d` (a Bool at each coordinate). -/
def parityPattern {d : Nat} (x : Fin d → ℤ) : Pattern d :=
  fun i => Int.bodd (x i)

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 claim that any real ledger must follow the single-coordinate atomic update rule. The theorem does not claim that the parity pattern uniquely identifies a vector or a sequence of steps. The theorem does not claim anything about nature; it is a statement about integer vectors and 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: