int_natAbs_eq_one_of_nonneg
plain-language theorem explainer
This lemma shows that any nonnegative integer whose absolute value equals one must equal one. It is invoked inside the proof that legal atomic ticks correspond to posting steps in the ledger model. The argument proceeds by case analysis on the integer representation, ruling out the negative successor case via the nonnegativity hypothesis.
Claim. If $z$ is an integer satisfying $|z|=1$ and $z$ is nonnegative, then $z=1$.
background
The module models ledger states as pairs of debit and credit vectors over dimension d, where an atomic tick posts exactly one unit to one account on one side. This produces a change of exactly ±1 in the phi vector at one coordinate, inducing a one-bit flip in the parity pattern. The lemma supplies a sign fact used when splitting monotonicity and cost conditions in the downstream equivalence between legal ticks and posting steps.
proof idea
The proof performs case analysis on z. In the ofNat case it extracts n=1 from the natAbs hypothesis by simplification. In the negSucc case it derives that negSucc n is strictly negative from the standard fact Int.negSucc_lt_zero, contradicting nonnegativity, and eliminates the resulting falsehood.
why it matters
The lemma enables legalAtomicTick_implies_PostingStep, which equates legal atomic ticks with explicit posting steps. This step connects the parity one-bit adjacency already established in LedgerParityAdjacency to the concrete debit-credit posting semantics required by the Recognition ledger model. It therefore supports the claim that single-unit updates produce exactly the one-bit parity changes needed for the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.