phi_zeroLedger
plain-language theorem explainer
The imbalance of the balanced zero ledger is identically zero at every account. Gap 2 dynamics proofs cite this when simplifying runs that start from empty debit and credit columns. The equality is definitional: both columns are the zero function, so the imbalance reading collapses by rfl and is marked simp.
Claim. For every account index $i$ on the discrete carrier $\Lambda$, if $L_0$ is the balanced zero ledger (debit and credit columns identically zero), then the imbalance reading satisfies $\varphi(L_0)(i)=0$.
background
Gap 2's fifth arc asks whether posting dynamics force the counts-only premise on charges. A posting step increments one account's debit or credit by one quantum; runs are schedules of such steps. The module's committed answer is that the dynamics exclude nothing among nonnegative ledgers, so they cannot force counts-only imbalance laws.
The balanced zero ledger is the initial condition: every debit and credit column is empty. Upstream it is the state canonical histories pin to, now read as the start of the dynamics rather than a selection among states. The imbalance reading $\varphi$ of a ledger is the pointwise debit-minus-credit map on accounts; nonnegative reachability from balance then realizes every integer imbalance configuration.
This declaration records the base case of that reading: on the zero ledger, $\varphi$ vanishes everywhere. Downstream schedule arguments rewrite runs that begin at balance against this fact.
proof idea
One-line definitional proof. The zero ledger sets both debit and credit to the constant-zero function on the discrete carrier, so the imbalance $\varphi$ is $0-0$ at every index and equals zero by rfl. The @[simp] attribute exposes the fact to the simplifier in later schedule calculations.
why it matters
Feeds schedule_countermodel_not_countsOnly, the module's headline negative result: after one tick from balance, an explicit posting schedule on the two-bridge witness yields imbalance $1$ on one edge letter and $0$ on another letter of the same kind, so no counts-only law about schedules is derivable from the dynamics. The countermodel rewrite chain begins by identifying the run with a single debit post on the zero ledger; vanishing of $\varphi$ at the start keeps the bookkeeping clean.
In the broader Gap 2 forcing chain, earlier arcs showed that kind-only cost and counts-only charge are not forced at the state or lattice layers. This simp fact is a tiny but load-bearing base identity for the dynamics layer's sharper conclusion: posting reaches every nonnegative ledger, hence every imbalance, including the non-counts-only families already exhibited. It does not itself close a T0–T8 landmark; it supports the gravity-side gap analysis that the measure's counts-only premise is optional, not forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.