BirthDeathRates
plain-language theorem explainer
A size-indexed pair of positive birth and death rates for a one-kind label carrier: total forward rate at size n and total backward rate at size n+1. Downstream Gap-2 lemmas cite it as the ambient dynamics for detailed balance, equal-per-slot laws, and counting-derived insert/delete rates. It is a plain structure with positivity side conditions, not a proved claim.
Claim. A birth-death rate package is a pair of maps $\mathrm{birth},\mathrm{death}:\mathbb{N}\to\mathbb{R}$ such that $\mathrm{birth}(n)>0$ for every $n$ and $\mathrm{death}(n+1)>0$ for every $n$. Here $\mathrm{birth}(n)$ is the total forward rate $n\to n+1$ and $\mathrm{death}(n)$ is the total backward rate $n\to n-1$ (evaluated at size $n=m+1$).
background
Gap-2 label-insertion dynamics studies whether an explicit carrier-enlarging insert/remove process forces InsertionStationarity (equivalently the GluingLaw), and thereby inverse factorials and the GaugeCountingPrinciple, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under another name.
The ambient object is a one-kind label carrier whose size $n\in\mathbb{N}$ changes by single-label birth or death. Rates are totals, not per-slot micro-rates: birth at $n$ is the aggregate $n\to n+1$ intensity; death at $n+1$ is the aggregate $(n+1)\to n$ intensity. Positivity is required so that detailed-balance identities may be rearranged into weight ratios.
Upstream, ledger-counted birth already appears as a truncated one-posting-per-tick probability, and several weight classes (gauge volume, quotient-first, holographic cell weight) supply the size densities that balance will constrain. This structure only packages the rate side of that comparison.
proof idea
No proof: a structure declaration. Four fields fix the data (two real sequences) and the two positivity hypotheses used by every later balance lemma. Instantiations such as equal-per-slot rates or size-blind birth with per-label death fill the fields and discharge positivity by elementary arithmetic.
why it matters
This is the typed carrier for the Gap-2 necessary-reasons census. DetailedBalance is defined directly on it; D01 equates weight ratios to rate ratios under that balance; the companion D01 form recovers the insertion recurrence $f(n+1)\cdot(n+1)=f(n)$ when death is $(n+1)$ times birth.
Concrete rate laws live here: equalPerSlotRates (symmetric $n+1$ insert and delete choices), sizeBlindBirthPerLabelDeath (counting-derived asymmetry: one creation opportunity, $n$ removable labels), and bakedFromWeight (the decoy that algebraically encodes a desired stationary weight). Downstream InsertionAsymmetryInevitableReasons reuses the same package for counting-equivalent rates and factorial-world balance.
In the module honesty ledger, the structure enables the THEOREM half (balance, constant-weight failure of InsertionStationarity, counting rates forcing stationarity once unit/atom are fixed) while leaving OPEN the recognition-structural derivation that birth is size-blind and death is per label. It does not move gap2_measure_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.