PostReachable
plain-language theorem explainer
Ledger reachability is the reflexive-transitive closure of single posting steps: L₂ is reachable from L₁ if a finite sequence of debit/credit increments turns L₁ into L₂. Gravity Gap-2 arguments cite it to state that every nonnegative ledger (hence every integer imbalance) arises from the balanced zero ledger. The definition is an inductive Prop with refl and one-step constructors; no proof body.
Claim. For ledgers $L_1,L_2$ on the discrete carrier $\Lambda$, write $L_1 \rightsquigarrow L_2$ when $L_2$ is obtained from $L_1$ by a finite sequence of posting steps. The relation is the smallest predicate closed under: (i) $L \rightsquigarrow L$ for every ledger $L$; (ii) if $L_1 \rightsquigarrow L_2$ and one posts a single quantum to account $k\in\Lambda$ on the debit or credit side, then $L_1 \rightsquigarrow L_2'$.
background
Gap 2 asks whether posting dynamics force the counts-only premise behind the kind-only cost. Earlier arcs reduced kind-only cost to counts-only charge and then to lattice imbalance/magnitude; none of those layers forced the premise. This module treats the dynamics themselves: a posting step increments one account's debit or credit column by one quantum on a Recognition.Ledger over the discrete carrier (units $\Lambda$, total relation).
The one-step map postAt lifts adjacency posting from a finite index type to an arbitrary decidable finite carrier: given ledger $L$, account $k$, and side (debit or credit), it returns the ledger with that column raised by one and the other column unchanged. A foundational ledger is a double-entry collection of recognition events; here the working object is the debit/credit column pair on $\Lambda$.
Reachability is defined as the inductive closure of that step so later theorems speak about the step relation itself, not a particular schedule device. Downstream results then show every nonnegative ledger is reachable from the zero ledger, and every integer imbalance is realized as the $\phi$ of some reachable ledger.
proof idea
No proof: this is an inductive proposition. Two constructors generate the relation. refl seeds identity. step takes a prior reachability witness $L_1 \rightsquigarrow L_2$, an account $k$, and a side $s$, and concludes $L_1 \rightsquigarrow \mathrm{postAt}(L_2,k,s)$. Induction on this Prop is the standard proof pattern for all downstream reachability lemmas (mass induction via predecessors, schedule extraction, run inclusion).
why it matters
This is the primitive relation for the Gap-2 dynamics arc. The module's committed answer is that dynamics exclude nothing among nonnegative ledgers, so they cannot force counts-only. Downstream, postReachable_zero_of_nonneg proves every nonnegative ledger is reachable from balance; imbalance_realized lifts that to every integer imbalance pattern (incidence and index readings included); exists_schedule_of_reachable and postReachable_run equate the inductive closure with explicit schedules; dynamics_produces_incidence_countermodel attaches arbitrary nonnegative magnitude and exhibits the incidence countermodel as dynamically generable.
The same predicate is reused outside the module as the dynamics half of WorldReachable (gluing-law stationarity) and RatedWorldReachable (insertion-asymmetry reasons). In the Gap-2 index it is the named witness that dynamics reach every nonnegative ledger. Framework role: it closes the forcing question at the posting layer by making "excludes no imbalance" a theorem about a single inductive closure rather than an informal schedule story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.