CorrectedInsertionDynamicsResidual
plain-language theorem explainer
Bundles the surviving Gap-2 residual: a named recognition prior that forces size-blind birth with per-label death, is not equal-per-slot counting, does not bake the stationary ratio into the rates, and still yields InsertionStationarity on the physical size weight. Downstream D12 cites this package as the selector target. Pure structure definition; no proof content.
Claim. A residual package of four propositions: (1) a named recognition prior forcing size-blind birth and per-label death; (2) that prior is not equal-per-slot insert/delete counting; (3) that prior does not encode the stationary weight ratio into the rates by hand; (4) from the prior, insertion stationarity holds for the physical size weight.
background
Gap-2 asks for an explicit carrier-enlarging label-insertion/removal dynamics that forces InsertionStationarity (equivalently the GluingLaw), hence inverse factorials and the GaugeCountingPrinciple, without assuming $\mu$, Aut, unit fugacity, or stationarity under a new name.
The module runs a necessary-reasons census. Proved facts include: birth-death detailed balance equates weight ratio to rate ratio; equal per-slot insert and delete rates force a constant weight and therefore fail InsertionStationarity; size-blind birth with per-label death forces InsertionStationarity once unit/atom are fixed. Refuted selectors include equirating the $n+1$ insertion slots with the $n+1$ deletion choices at equal unit rate.
What remains open is deriving, from recognition structure or the posting schedule nature executes, that birth is size-blind (one creation opportunity per tick) while death is per existing label, or any counting-equivalent that yields $\mu_{n+1}=(n+1)\lambda_n$ without writing the stationary law into the rates.
proof idea
Definitional structure only: four Prop fields with no constructors, instances, or proofs. It packages the census residual named in the module honesty block (OPEN: derive size-blind birth / per-label death from recognition structure). Sibling lemmas already settle the surrounding gates (detailed balance, equal-per-slot failure, decoy bake-in rejection); this declaration does not discharge any of them.
why it matters
Closes the census bookkeeping for Gap-2 insertion dynamics by naming the single surviving residual after proved and refuted reasons are stripped away. Downstream D12 uses the package as the target of a selector that respects present recognition dynamics: it must pick the asymmetric counting rates and reject the equal-per-slot decoy.
In the broader RS gravity stack this residual sits under Gap-2 gluing-law stationarity and the unit-fugacity selector. Filling it would force InsertionStationarity from recognition structure alone, unlocking inverse-factorial weights and the GaugeCountingPrinciple without smuggling $\mu$ or Aut. The module is explicit that Cambrian Target Research can grind lemmas once the dynamics is typed but cannot invent the missing physical rate asymmetry; gap2_measure_derived is not moved by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.