pith. machine review for the scientific record. sign in
def definition def or abbrev high

coordAtomicStep

show as:
view Lean formalization →

coordAtomicStep defines the predicate on pairs of vectors in Z^d such that y differs from x by exactly one coordinate changed by +1 or -1. Ledger-to-parity bridge work in Recognition Science cites this as the atomic update relation that feeds one-bit difference theorems. The definition is introduced directly by the existential quantifier over the changed index k together with the agreement condition on all other coordinates.

claimFor vectors $x,y : {Z}^d$, the predicate holds precisely when there exists an index $k$ such that $y_k = x_k + 1$ or $y_k = x_k - 1$ and $y_i = x_i$ for every $i ≠ k$.

background

The module supplies the mathematical core of the ledger-to-parity bridge (Workstream B2). It treats integer vectors and their parity patterns (mod 2) as abstract objects; the claim that actual ledger states obey the atomic-step hypothesis is left to a separate theorem. Upstream, parity is the abbrev that applies parityPattern to the phi-vector of a LedgerState, while the various one constants supply the unit increments used in the ±1 clause.

proof idea

This is a definition, not a derived statement. It is introduced by the explicit existential quantifier over the single changed coordinate k, the disjunction for the ±1 difference at that coordinate, and the universal quantifier enforcing agreement elsewhere.

why it matters in Recognition Science

The definition supplies the hypothesis for the downstream theorem coordAtomicStep_oneBitDiff, which establishes OneBitDiff between the parity patterns of x and y. It also appears in the abbrev ledgerVecStep and in the posting lemma phiVec_coordAtomicStep_of_post. In the Recognition framework it closes the first half of the ledger-parity adjacency link; the second half (that RS ledger legality forces atomic steps) remains open.

scope and limits

formal statement (Lean)

  33def coordAtomicStep {d : Nat} (x y : Fin d → ℤ) : Prop :=

proof body

Definition body.

  34  ∃ k : Fin d,
  35    (y k = x k + 1 ∨ y k = x k - 1) ∧
  36    (∀ i : Fin d, i ≠ k → y i = x i)
  37
  38/-! ## Core theorem: atomic coordinate update ⇒ one-bit parity difference -/
  39

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.