ledgerMoveCount_eq_kernel
plain-language theorem explainer
Ledger-counted move multiplicities between carrier sizes m and n equal the carrier step weight evaluated at the size-blind birth / per-label death rates. Gravity and Gap-2 auditors cite it to pin D14: the insertion kernel is not a hand table but the cardinality of a size-partitioned ledger move set. The proof is a three-way case split on up-step, down-step, and off-diagonal, reducing each arm by the corresponding move-count lemma and simplifying the rate pair.
Claim. For all natural numbers $m,n$, the real-valued ledger move multiplicity from size $m$ to size $n$ equals the carrier step weight of the rate law with one creation opportunity per tick and one deletion choice per existing label, evaluated at $(m,n)$.
background
Gap-2 Room B is a necessary-reasons census for insertion asymmetry: recognition structure is asked whether it forces the asymmetric carrier-enlarging rate law (one birth opportunity per tick, one death choice per live label), or a counting-equivalent law $\mu(n+1)=(n+1)\lambda n$ that is not baked from a weight. The target is a search directive, never a premise.
Earlier rows bank existence of those counting rates inside the recognition-rate-asymmetry interface (D10), assembly of the insertion kernel from any rates obeying the counting law (D11), a scoped wall that bare posting reachability cannot select the asymmetric rates over equal-per-slot (D12), and a rate-sensitive carrier-enlarging kernel whose up-step weight out of size one selects the counting rates (D13).
D14 sharpens provenance: multiplicities must be cardinalities of a size-partitioned ledger move set on tick-tagged carriers (one posting pinned to the next tick, one settlement per live quantum), not a hand-placed table. The fundamental tick is the RS time quantum $\tau_0=1$. The carrier step weight is the kernel that turns a rate pair into up/down/off transition weights on carrier sizes.
proof idea
Term-mode proof by unfolding the carrier step weight, then case-splitting on the adjacency of $m$ and $n$.
If $n=m+1$, substitute and rewrite by the up-step move-count identity, then simplify against the size-blind birth / per-label death rates.
If $m=n+1$, rewrite by the down-step move-count identity, discharge the negated up-case and the positive down-case in the weight definition, push casts, and finish by ring.
Otherwise both adjacencies fail: rewrite by the off-diagonal move-count identity (zero multiplicity) and simplify the weight to zero on the same negated hypotheses. No external gravity lemmas beyond the three move-count arms and the rate-pair definition.
why it matters
This equality is the counting half of D14. Downstream, D14_theorem packages it as the countsKernel field of the ledger-schedule provenance record: move multiplicities equal the filtered cardinality of ledger moves of target size, and those multiplicities reproduce the carrier step weight exactly. The module doc scores the rate-readoff decoy as pre-scored and the tick pinning as load-bearing; deriving that pinning on actual recognition-ledger states is deferred to D15.
The certified insertion-asymmetry reasons table consumes D14 together with D10–D13, D15, and D16 freshness forcing. In the broader RS gravity stack this closes the claim that the asymmetric insertion kernel is ledger-counted rather than stipulated, which is the provenance needed before any measure or galactic-dynamics readout can treat the kernel as forced structure rather than a free ansatz. It does not yet move the measure flag or select rates by bare dynamics (D12 wall remains).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.