int_eq_of_natAbs_eq_zero
The lemma states that an integer z vanishes whenever its natural absolute value is zero. Ledger modelers invoke it inside the conversion of a legal atomic tick into an explicit posting step. The argument is a direct application of the library equivalence between natAbs zero and the integer being zero.
claimIf $z$ is an integer satisfying $|z|=0$, then $z=0$.
background
The module models ledger states as pairs of debit and credit vectors. Each atomic tick posts exactly one unit to one account, changing the phi-vector (debit minus credit) by exactly one coordinate. Integer differences arise when comparing pre-tick and post-tick entries; the present lemma supplies the elementary fact that a vanishing natural absolute value forces the underlying integer difference to be zero. It is invoked inside the classical case split that converts a legal atomic tick into a posting step.
proof idea
The proof is a one-line wrapper that applies Int.natAbs_eq_zero.mp to the hypothesis.
why it matters in Recognition Science
This lemma supports legalAtomicTick_implies_PostingStep, which shows every legal atomic tick corresponds to a posting step. It closes the gap between the parity one-bit adjacency result and the concrete debit-credit mechanics of the ledger model. The eight-tick octave and phi-ladder structures rely on such exact integer equalities to preserve the one-bit change property.
scope and limits
- Does not extend to real or rational numbers.
- Does not handle signed natural numbers or other encodings.
- Does not prove uniqueness of representations beyond the zero case.
- Does not address computational complexity or implementation.
formal statement (Lean)
773private lemma int_eq_of_natAbs_eq_zero {z : ℤ} (hz : Int.natAbs z = 0) : z = 0 := by
proof body
One-line wrapper that applies exact.
774 exact (Int.natAbs_eq_zero.mp hz)
775