postingMove_card
plain-language theorem explainer
The posting-move finset out of a size-$m$ tick-tagged carrier has cardinality $m+1$: the $m$ live tags plus the single next-tick posting. Gravity Gap-2 ledger-counting arguments cite this to pin move multiplicities. The proof unfolds the two finset definitions and applies the standard insert-and-range card lemmas.
Claim. For every natural number $m$, the finset of posting moves leaving the canonical size-$m$ tick-tagged carrier has cardinality $m+1$.
background
Gap-2 Room B is a necessary-reasons census for insertion asymmetry in Recognition gravity. The assumed target is a carrier-enlarging rate law (size-blind birth per label death, or a counting-equivalent $\mu(n+1)=(n+1)\lambda n$ not baked from a weight). This module banks D10–D14 as THEOREM or REFUTED without asserting composite GCP inhabitation.
The canonical tick-tagged carrier of size $m$ is the finset of live quanta tagged $0,\ldots,m-1$ by their posting ticks (the range finset of length $m$). The posting move out of that carrier is the same finset with the next tick $m$ inserted: tick discipline admits one posting per tick, and the new quantum is tagged by $m$.
D14 counts kernel move multiplicities from a ledger-typed move set on these tick-tagged carriers (one posting pinned to the next tick, one settlement per live quantum), aiming to reproduce the carrier step weight exactly.
proof idea
Term-style tactic proof. Unfold the posting-move and tick-carrier definitions so the goal is the card of $\mathrm{insert}, m,(\mathrm{range}, m)$. Rewrite by the insert-card lemma under the side goal that $m\notin\mathrm{range}, m$ (discharged by simp), then by the range-card lemma, which yields $m+1$.
why it matters
Feeds the three ledger move-count theorems that implement D14: one up-move (exactly one ledger move enlarges the carrier: the tick-pinned posting), $m+1$ down-moves out of size $m+1$ (one settlement per live quantum), and zero off-diagonal transitions. Those counts make the kernel's move multiplicities match the carrier step weight and score the rate-readoff decoy and tick pinning as load-bearing.
In the broader census, D10 shows the counting rates inhabit recognition-rate asymmetry and are not baked from weight; D12 scopes that bare posting reachability cannot select them; D13 shows the carrier-enlarging birth-death kernel is rate-sensitive and selects the counting rates via the observation that the up-step weight out of size one equals one. This card identity is the elementary finset fact that turns the ledger move set into those multiplicities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.