Ledger Parity Adjacency Coord Atomic Step One Bit Diff

The one-bit bridge

In the Recognition Science framework, a ledger is a discrete record of events, and one of the framework's core moves is to ask what kinds of change are allowed between one recorded state and the next. The declaration coordAtomicStep_oneBitDiff is a machine-checked theorem in the framework's library that answers a narrow, precise version of that question. It says: if you take an integer vector, change exactly one coordinate by either +1 or -1, and leave every other coordinate untouched, then the parity pattern of the vector, meaning the odd-or-even status of each coordinate, changes in exactly one bit. The other bits, the parities of all the untouched coordinates, stay the same.

The theorem is about integer vectors and parity, not about nature. It does not say that ledgers actually update this way, nor that any physical process obeys this rule. The library's own documentation is explicit on this point: this is a theorem about arithmetic, and turning it into a claim about ledgers requires a separate, unproved step. That step would need to show that the framework's ledger legality rules and its cost-minimization principle together force the single-coordinate ±1 update hypothesis. Until that separate theorem exists, the bridge from this arithmetic fact to a statement about recognition events remains open.

What the theorem does establish is a clean structural link between two ways of describing a change. One way is fine-grained: a single coordinate moves by one unit. The other is coarse: you look only at whether each coordinate is odd or even. The theorem says the coarse description cannot hide the fineness of the move. A one-unit change in one place shows up as exactly one flipped bit in the parity pattern, never as two, never as zero. That is the content of the declaration, and it is the content of nothing more.

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 theorem does not claim that ledgers actually update by single-coordinate ±1 steps. The theorem does not claim that the parity pattern is the only observation a ledger supports. The theorem does not claim that the bridge from arithmetic to ledger constraints is proved.

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: