equalPerSlotRates
plain-language theorem explainer
Symmetric birth-death rates on a one-kind label carrier: total birth at size n is n+1 and total death at size n+1 is n+1, each insertion slot or label firing at unit rate. Gap-2 gravity census work cites this as the minimal equirated dynamics. The definition packages the two rate maps with positivity proved by casting successor positivity on naturals to the reals.
Claim. The equal-per-slot rate law is the birth-death dynamics with total birth rate $b(n)=n+1$ and total death rate $d(n)=n$ (hence $d(n+1)=n+1$), both strictly positive for every $n\in\mathbb{N}$.
background
Gap-2 label-insertion dynamics studies which birth-death rate laws force InsertionStationarity (equivalently the GluingLaw), and thus inverse factorials and the GaugeCountingPrinciple, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under a new name. The module is a necessary-reasons census: each candidate reason is proved, left open, recorded as model, or refuted.
A BirthDeathRates package is a pair of size-indexed maps: birth n is the total forward rate $n\to n+1$, and death n is the total backward rate $n\to n-1$ (consumed at size $n+1$), together with positivity. Detailed balance then equates the weight ratio to the rate ratio. The equal-per-slot law is the smallest symmetric choice: $n+1$ insertion slots and $n+1$ deletion choices, each at unit rate, so totals are both $n+1$.
proof idea
Structure instance, not a theorem. Birth is $\lambda n.,n+1$ and death is $\lambda n.,n$ on $\mathbb{R}$. Positivity of birth at every $n$ is Nat.succ_pos cast to $\mathbb{R}$. Positivity of death at $n+1$ is the same successor fact rewritten as $0<n+1$ and simplified into the death field.
why it matters
This is the decoy dynamics that the Gap-2 census refutes as a selector of InsertionStationarity. Downstream, detailed balance of constant unit weight under these rates is immediate (D02), and pairing that with failure of insertion stationarity at $n=1$ yields D03: counting insertion slots and deletion choices the same way balances a constant weight and does not force the gluing law.
Both facts feed labelInsertionDynamics_certified and the parallel reason table in InsertionAsymmetryInevitableReasons (D02, D03, D12). The corrected floor plan after D03 is explicit: force asymmetric counting (size-blind birth versus per-label death, or an equivalent $\mu_{n+1}=(n+1)\lambda_n$ from move counts) rather than baking the stationary law into the rates. That asymmetry remains OPEN in the module honesty block; this definition only banks the failed symmetric baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.