sizeBlindBirthPerLabelDeath
plain-language theorem explainer
Size-blind birth with per-label death: total forward rate is constantly 1 (one creation opportunity), total backward rate at size n is n (one removal per existing label). This is the counting-derived birth-death rate law used throughout the Gap-2 necessary-reasons census. Positivity is immediate from the constant 1 and from n+1≥1. Anyone citing D04, the label-insertion kernel, or the dynamics certificate uses this instance.
Claim. The size-blind birth / per-label death law is the pair of total rates $\lambda^{\mathrm{birth}}_n = 1$ and $\lambda^{\mathrm{death}}_n = n$ (for $n\ge 1$), both strictly positive, packaged as size-indexed birth-death rates on a one-kind label carrier.
background
In the Gap-2 label-insertion dynamics module, the corrected target is a carrier-enlarging birth-death process whose detailed balance forces InsertionStationarity (equivalently the GluingLaw), hence inverse factorials and the Gauge Counting Principle, without assuming $\mu$, Aut, or unit fugacity by hand.
BirthDeathRates packages two size-indexed total rates: birth $n$ is the forward rate $n\to n+1$, death $n$ is the backward rate $n\to n-1$ (used at $n=m+1$), with positivity. Detailed balance for a weight $f$ equates the weight ratio to the rate ratio. InsertionStationarity requires unit and atom normalizations $f(0)=f(1)=1$ and the local balance $f(n+1)\cdot(n+1)=f(n)$.
The module census lists every reason that would make that forcing unavoidable. This definition supplies the asymmetric counting rates D04 uses: one creation opportunity per tick, $n$ removable labels at size $n$. The factor $n+1$ never appears as a hand-written stationary coefficient.
proof idea
Definitional construction of a BirthDeathRates record. Birth is the constant function $1$; death is the identity on $\mathbb{N}$ (cast to $\mathbb{R}$). Positivity of birth is norm_num on $0<1$. Positivity of death at $n+1$ is the cast of Nat.succ_pos. No lemmas beyond elementary arithmetic are required.
why it matters
This rate law is the concrete asymmetric counting that D04 packages: under detailed balance plus unit/atom, it is exactly InsertionStationarity. Downstream results use it to force insertion stationarity, close the label-insertion kernel, obtain the Gauge Counting Principle, show the inverse-factorial weight is stationary, and feed the composite certificate labelInsertionDynamics_certified.
The module honesty block flags the residual OPEN item: derive from recognition structure that birth is size-blind while death is per existing label (or an equivalent asymmetry yielding $\mu_{n+1}=(n+1)\lambda_n$) without writing the stationary law into the rates by hand. The corrected floor plans note that the surviving residual after the census is exactly deriving this rate law from the posting schedule nature executes. It does not move gap2_measure_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.