labelInsertionDynamics_certified

Gap-2 asks for a carrier-enlarging label-insertion/removal dynamics that forces InsertionStationarity (equivalently the GluingLaw), hence inverse factorials and the Gauge Counting Principle, without presupposing $\mu$, $\mathrm{Aut}$, unit fugacity, or stationarity under a new name. InsertionStationarity is the local law: unit weight on the empty and singleton carriers, and $f(n+1)\cdot(n+1)=f(n)$ on every enlargement. The intended world is the inverse-factorial weight $f(n)=1/n!$.

Detailed balance for a size weight $f$ under birth-death rates $R$ is the identity $f(n+1),R_{\mathrm{death}}(n+1)=f(n),R_{\mathrm{birth}}(n)$. Equal per-slot rates equate every insertion slot with every deletion choice at unit rate; size-blind birth with per-label death is the counting-derived asymmetric alternative. The module is a necessary-reasons census (method plan 20260807): each candidate reason is proved, left OPEN, recorded as MODEL, or refuted.

Parent modules supply the stationarity structure, the factorial world, and the live full-theory ledger. The measure-derived benchmark flag is deliberately left unmoved by this scoped census.

Term-mode refine of a nine-way conjunction. Length of the reason table is reasonTable_length. Detailed balance of constant weight under equal per-slot rates is D02_equal_per_slot_balances_constant. Failure of insertion stationarity for that constant weight is the second projection of D03_equal_per_slot_fails_insertionStationarity. The factorial-world pair (detailed balance under size-blind birth/per-label death, plus insertion stationarity) is D04_factorial_is_stationary. Geometry inhabitance is D05_geometry_inhabited. Floor-plan and first-attack-block lengths are the corresponding length lemmas. The OPEN_RATE_ASYMMETRY status string is rfl. The measure flag is gap2_measure_derived_unmoved (itself rfl on the ledger).

Banks the honest Gap-2 dynamics census required before any claim that birth-death rates force the gluing law. Equal per-slot equirating is refuted as a selector: it balances only a constant weight and therefore cannot yield InsertionStationarity. The counting-derived asymmetric rates (size-blind birth, per-label death) do force stationarity once unit and atom are fixed, recovering inverse factorials without writing the stationary law into the rates by hand under a new name.

The open residue is explicit: derive, from recognition structure alone, that birth is size-blind (one creation opportunity per tick) while death is per existing label, or an equivalent asymmetry giving $\mu_{n+1}=(n+1)\lambda_n$. Until D07/D08 close that rate asymmetry, the measure-derived ledger flag stays put. No downstream consumer is wired yet; the certificate is the census endpoint for this module. Framework contact is the Gap-2 gluing/stationarity step toward continuum measure in the gravity seven-gaps program, not the T0–T8 forcing chain directly.