legalAtomicTick_implies_PostingStep
plain-language theorem explainer
A legal atomic tick on a d-dimensional ledger, defined as a monotone update with total L1 cost exactly 1, is necessarily a single posting step that increments exactly one coordinate on either the debit or credit side. Researchers modeling recognition via ledger states would cite this to link the legality predicate to the explicit post constructor. The proof splits the L1 cost into debit and credit sums, applies add_eq_one_iff to isolate the changed side, locates the unique coordinate via exists_unique_of_sum_univ_eq_one, and verifies fieldwise
Claim. Let $L, L'$ be ledger states in dimension $d$. If the update is monotone in both debit and credit counts and the L1 cost equals 1, then there exists a coordinate $k$ and a side $s$ such that $L'$ equals the result of posting one unit to account $k$ on side $s$.
background
The module upgrades Workstream B to an explicit ledger-shaped model in which a LedgerState d consists of debit and credit vectors over d accounts. LegalAtomicTick requires the update to be monotone and to satisfy ledgerL1Cost exactly 1. PostingStep asserts existence of $k$ and side such that $L'$ equals post L k side. This supplies the missing glue between the legality predicate and the parity one-bit adjacency lemma in LedgerParityAdjacency. Upstream lemmas on sums equaling one and integer equalities from ArithmeticFromLogic and IntegersFromLogic are invoked to handle the coordinate uniqueness and sign constraints.
proof idea
The tactic proof begins with classical and rcases to separate monotonicity from the cost hypothesis. It defines separate debit and credit L1 sums, proves their total equals 1 via simpa on ledgerL1Cost, then applies Nat.add_eq_one_iff to obtain two cases. In each case exists_unique_of_sum_univ_eq_one locates the changed coordinate while sum_eq_zero_iff_of_nonneg shows the other side is identically zero. Case analysis on the LedgerState constructors followed by funext, int_eq_of_natAbs_eq_zero, int_natAbs_eq_one_of_nonneg and linarith establishes that $L'$ matches the post update.
why it matters
This theorem supplies the forward direction of the equivalence PostingStep iff LegalAtomicTick, which is used directly in postingStep_iff_legalAtomicTick and in legalAtomicTick_oneBitDiff to obtain OneBitDiff on the parity vectors. It bridges the ledger posting model to the parity adjacency results that support the eight-tick octave and D=3 in the forcing chain. The module doc notes that deriving why nature must adopt this posting model remains a separate MECH/AXIOM step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.