D04_asymmetric_rates_give_kernel
plain-language theorem explainer
Packages a size weight under size-blind birth and per-label death detailed balance, with unit and atom fixed, into a full label-insertion kernel (geometry plus stationarity). Anyone citing the conditional Gap-2 closure path would use this. One-line constructor: inhabited succ-above geometry plus the D04 stationarity theorem.
Claim. Given a weight $f:\mathbb{N}\to\mathbb{R}$ in detailed balance with size-blind birth (forward rate $1$) and per-label death (backward rate $n$), and with $f(0)=f(1)=1$, construct a label-insertion kernel for $f$: the standard order-preserving skip geometry together with unit, atom, and insertion stationarity $f(n+1)\cdot(n+1)=f(n)$ for all $n$.
background
Gap-2 asks for an explicit carrier-enlarging label-insertion/removal dynamics that forces InsertionStationarity (equivalently the GluingLaw), hence inverse factorials and the Gauge Counting Principle, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under a new name.
A label-insertion kernel is the missing ledger object: a combinatorial geometry of $n+1$ insertion slots plus a weight $f$ with unit $f(0)=1$, atom $f(1)=1$, and stationarity $f(n+1)\cdot(n+1)=f(n)$. The geometry half is already inhabited by the order-preserving skip map (Fin.succAboveEmb). Detailed balance for birth-death rates equates weight ratios to rate ratios: $f(n+1),R_{\mathrm{death}}(n+1)=f(n),R_{\mathrm{birth}}(n)$.
Size-blind birth with per-label death sets birth rate $1$ (one creation opportunity per tick) and death rate $n$ ($n$ removable labels). Under that law, detailed balance plus unit/atom is exactly InsertionStationarity (D04). The rate asymmetry itself remains OPEN as a recognition-structure derivation.
proof idea
One-line wrapper. Apply the kernel constructor that takes a geometry and an InsertionStationarity witness: feed the inhabited succ-above geometry and the theorem that size-blind birth / per-label death detailed balance plus unit/atom yields InsertionStationarity. No new algebra; pure packaging of D04 with the already-proved geometry half.
why it matters
Closes the conditional Gap-2 package: asymmetric counting rates + unit/atom + geometry give a full label-insertion kernel, and therefore (via the next theorem) the Gauge Counting Principle on the product class mass. Downstream D04_asymmetric_rates_give_gcp applies the kernel-to-GCP bridge to this object.
Doc-comment is explicit: this is conditional closure, not a derivation of the rates. The census honesty block keeps OPEN the recognition-structure origin of size-blind birth versus per-label death (or any equivalent asymmetry yielding $\mu_{n+1}=(n+1)\lambda_n$ without writing stationarity into the rates). Equal-per-slot rates are already refuted as a selector; they force constant weight and fail stationarity. No Target Research job invents the missing physical asymmetry; this def only banks the typed dynamics once the rates are assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.