does
plain-language theorem explainer
Posting dynamics on the recognition ledger do not force the counts-only premise behind Gap 2's measure. From the balanced zero ledger every nonnegative column state is reachable by unit debit/credit posts, so every integer imbalance, including the incidence and index countermodels, is dynamically generable. Gravity and RS measure workers on the Seven Gaps chain cite this as the sharp negative at the dynamics layer. Packaged as a structure (definition interface), not a proved theorem.
Claim. Ledger posting dynamics do not constrain charges to be counts-only. A posting step raises one account's debit or credit by one quantum; a run is a finite schedule of such steps. From the balanced zero ledger, every ledger with nonnegative columns is reachable, hence every integer imbalance arises as the image of some reachable ledger (including incidence-reading and index-reading configurations that fail counts-only). Magnitude is untouched: the bare ledger has no magnitude field.
background
Gap 2's measure rests on a chain of named premises. The weight is size-blind if the cost is kind-only; the cost is kind-only if its charge is counts-only (ChargesCountsOnly); the charge is counts-only if lattice imbalance and magnitude are (LatticeChargesCountsOnly). Prior arcs showed none of those is forced at its own layer. This module is the fifth arc: it asks whether the posting dynamics that produce ledger states force the counts-only premise.
The dynamics are elementary. LedgerPostingAdjacency.post / PostingStep increments one debit or credit column by one quantum; a run is a schedule of steps. Posts only raise columns, so the reachable set from the zero ledger is exactly the nonnegative orthant (forward reachability, not ergodicity). The fourth arc's dual premise therefore has two conjuncts to kill: imbalance and magnitude.
Upstream siblings in the Gap 2 stack record parallel negatives: class-pushforward does not equate $Z$ with the inequivalent-class sum weighted by $1/|\mathrm{Aut}|$, and the kind-rule layer does not supply the counts-only case on its own.
proof idea
Definition-level structure with empty body: it records the committed negative answer rather than proving a Prop. The mathematical content is carried by the module's reachability and countermodel lemmas (named in the module doc, not in this declaration): postReachable_zero_of_nonneg (every nonnegative ledger is reachable from zero), imbalance_realized / imbalance_realized_by_schedule (every integer imbalance is $\phi$ of a reachable ledger, via an explicit schedule), schedule_countermodel_not_countsOnly (a two-bridge schedule whose one-tick imbalance is not kind-constant), and dynamics_produces_incidence_countermodel (any nonnegative magnitude can be attached via DualEntryStrainState.ofLedger). Magnitude falls by silence: posting never mentions a mag field.
why it matters
Closes the dynamics arc of Gap 2 with the sharpest negative in the stack: the dynamics exclude nothing, so they cannot force counts-only. That blocks any hope of discharging ChargesCountsOnly / LatticeChargesCountsOnly from posting rules alone; the premise remains an independent hypothesis at the measure layer. In the broader RS gravity program this keeps Gap 2 honest about what the ledger calculus actually entails versus what must still be assumed.
Downstream graph edges fan into action convexity, Noether momentum, and chemistry proxies, but those uses are name-level on a short identifier and should not be read as semantic consumers of the Gap 2 negative. The real parent is the Seven Gaps measure development that must either keep counts-only as an open hypothesis or find a forcing argument outside posting dynamics. No T5–T8 landmark is discharged here; the result is a scope restriction on the ledger side of the gravity gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.