zeroLedger
plain-language theorem explainer
The balanced empty ledger on the discrete carrier: every debit and every credit column is identically zero. It is the canonical initial condition for posting dynamics in the Gap-2 arc, the state from which all nonnegative ledgers are reached by schedules of single-quantum posts. Downstream reachability, mass-zero uniqueness, and imbalance-realization theorems all pin histories to this origin. The definition is a two-field structure instance with constant-zero maps.
Claim. Let $\Lambda$ be a finite decidable carrier. The zero ledger is the recognition ledger on the discrete carrier of $\Lambda$ whose debit map and credit map are both the zero function: $\mathrm{debit}(i)=0$ and $\mathrm{credit}(i)=0$ for every account $i\in\Lambda$.
background
Gap 2 asks whether the measure behind the gravity gaps is forced to be counts-only. Earlier arcs reduced that question through kind-only cost and lattice imbalance; this module treats the ledger dynamics that produce states, not the state type alone. A recognition ledger on a discrete carrier is a pair of integer-valued columns (debit, credit) on each account. Posting increments one column of one account by one quantum; a run is a schedule of such steps.
The module's committed answer is that the dynamics excludes nothing among nonnegative ledgers: from balance, every nonnegative column configuration is reachable, hence every integer imbalance pattern arises as the $\phi$ of some reachable ledger. Magnitude is untouched by posting and can be attached freely afterward.
Upstream, Recognition.Ledger is the double-entry structure used throughout the foundation (events with balance, or debit/credit columns). The discrete carrier lifts the finite alphabet of a bounded complex so that posting adjacency applies uniformly. The zero ledger is the balanced origin those runs start from, reinterpreting the state that canonical histories pin to as an initial condition rather than a selection among states.
proof idea
Pure structure definition: instantiate Recognition.Ledger on discreteCarrier Λ by setting both debit and credit to the constant-zero function. No lemmas, no tactics; the body is the two field assignments.
why it matters
This is the origin point for the entire Gap-2 dynamics arc. Reachability is stated as PostReachable zeroLedger L; every nonnegative ledger is reachable from it, so every integer imbalance is realized (imbalance_realized, imbalance_realized_by_schedule). Mass-zero uniqueness (eq_zeroLedger_of_mass_zero) and the nonzero-column witness (exists_pos_of_ne_zero) characterize it algebraically. Schedules reconstruct reachable states from it (exists_schedule_of_reachable).
The parent theorem dynamics_produces_incidence_countermodel uses that origin explicitly: there exists a ledger reachable from the zero ledger whose imbalance is the incidence imbalance, and any nonnegative magnitude lifts along for free. That is the sharp negative answer of the arc: posting dynamics does not force counts-only, because it generates the incidence and index countermodel imbalances from balance one quantum at a time. In the Recognition forcing picture this sits under the gravity/gap layer rather than T0–T8, but it closes the dynamics premise that the lattice and kind-rule arcs left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.