Index
plain-language theorem explainer
Packages the fifth-arc Gap-2 audit as four propositional flags plus a premise name: reachability of every nonnegative ledger, schedule realization of every imbalance, dynamical production of the incidence countermodel, and the claim that dynamics forces counts-only schedules. Auditors of the Gap-2 premise chain cite it as the checklist that the arc audit pins together. Plain structure definition; no proof obligations.
Claim. An index record with four propositions and one string: (1) every ledger with nonnegative columns is reachable from the balanced zero ledger under posting dynamics; (2) every integer imbalance arises from an explicit posting schedule; (3) the dynamics produces a reachable ledger whose imbalance equals the incidence imbalance, liftable with any nonnegative magnitude; (4) every posting schedule on the two-bridge witness is counts-only; together with a string naming the premise under audit.
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; the charge is counts-only if lattice imbalance and magnitude are. None of those is forced at its own layer. The fourth arc pointed at ledger dynamics: posting rules that produce states, not the state type itself.
A posting step increments one account's debit or credit by one quantum. A run is a schedule of such steps. From the balanced zero ledger, every ledger with nonnegative columns is reachable (posts only raise columns, so negative columns stay unreachable). Consequently every integer imbalance is the imbalance of some reachable ledger, and is hit by an explicit schedule. Magnitude is silent under posting: the ledger type has no magnitude field, so any nonnegative magnitude can be attached after the fact.
The upstream theorem on dynamical production of the incidence countermodel states that on every complex's posting alphabet there is a ledger reachable from balance whose imbalance is exactly the incidence imbalance, and that ledger lifts with any nonnegative magnitude to a dual-entry strain state carrying that pair.
proof idea
No proof: this is a structure declaration. Each of the four Prop fields is a typed slot meant to hold the statement of the corresponding theorem (or its negation, for the counts-only schedule claim). The string field records the named premise under audit. Downstream audit code is expected to inhabit or refute these slots; the structure itself only fixes the shape of the checklist.
why it matters
This is the index of the fifth arc in the Gap-2 forcing chain. The module's committed answer is that dynamics forces nothing: it reaches every nonnegative ledger, realizes every imbalance by schedule, and produces the incidence-reading countermodel from balance one post at a time. The fourth flag is the premise in strongest schedule form ("every posting schedule on the two-bridge witness is counts-only"); the arc audit refutes that proposition with an exhibited countermodel schedule, so the negative entry is a real theorem rather than a constant falsehood.
The packaging lets a single audit object pin the four dynamical claims together against the named premise string. In the broader Recognition Gravity stack this closes the dynamics layer of Gap 2: the counts-only hypothesis is not forced by posting rules, matching the sharper negative already seen at the lattice and kind-rule layers. No downstream consumers are recorded in the graph yet; the intended consumer is the arc audit that discharges or refutes each flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.