DetailedBalance
plain-language theorem explainer
Detailed balance equates adjacent size-weights to birth-death rates: f(n+1)·death(n+1) = f(n)·birth(n) for every n. It is the stationary matching condition for one-kind label carriers in the Gap-2 insertion census. Anyone proving D01–D04 (ratio form, scaled-death recurrence, equal-per-slot refutation, asymmetric forcing) cites it. The body is a pure Prop abbreviation, not a proved statement.
Claim. A size weight $f:\mathbb{N}\to\mathbb{R}$ is in detailed balance with birth-death rates $R$ when, for every $n\in\mathbb{N}$, $$f(n+1)\,R_{\mathrm{death}}(n+1)=f(n)\,R_{\mathrm{birth}}(n).$$ Here $R_{\mathrm{birth}}(n)$ is the total forward rate $n\to n+1$ and $R_{\mathrm{death}}(n+1)$ is the total backward rate $(n+1)\to n$, both strictly positive by the rate structure.
background
Gap-2 asks whether an explicit carrier-enlarging label insertion/removal dynamics forces InsertionStationarity (equivalently the GluingLaw), and thus inverse factorials and the Gauge Counting Principle, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under another name. This module runs a necessary-reasons census of that forcing.
BirthDeathRates packages size-indexed totals: birth $n$ is the forward rate $n\to n+1$; death $n$ is the backward rate $n\to n-1$ (read at $n=m+1$), with positivity on every birth and every death at $n+1$. The weight $f$ is the size-dependent density on the one-kind label carrier (orbit size over sector relabeling count in the gauge-volume language).
Detailed balance is the classical stationary edge condition for that birth-death chain: probability flux $n\to n+1$ equals flux $n+1\to n$. It is the typed hinge between rate laws and the weight recurrence used by insertion stationarity.
proof idea
Definition, not a theorem. The Prop is the universal quantification $\forall n,, f(n+1)\cdot R.\mathrm{death}(n+1)=f(n)\cdot R.\mathrm{birth},n$. No tactics or lemmas; downstream theorems either unfold it (D01_balance_ratio is literally the hypothesis applied at $n$) or discharge it by simp/field_simp on concrete rate constructors (constantWeight with equalPerSlotRates; bakedFromWeight).
why it matters
This is the typed stationary matching law for the Gap-2 label-insertion dynamics census. Parent results include D01_balance_ratio (weight ratio equals rate ratio under positivity), D01_balance_of_scaled_death (if death$(n+1)=(n+1)\cdot$birth $n$, balance collapses to $f(n+1)\cdot(n+1)=f(n)$, the insertion-stationarity recurrence), D02/constantWeight_detailedBalance_equalPerSlot, and the D03 refutation that equal per-slot rates balance only the constant weight and therefore fail InsertionStationarity at $n=1$. D04 uses the same Prop to show asymmetric (size-blind birth, per-label death) rates force stationarity and the GCP once unit/atom are fixed.
In the module honesty ledger it is THEOREM infrastructure: balance equates weight ratio to rate ratio; symmetric equirating is REFUTED as a selector; the OPEN item is deriving the physical rate asymmetry from recognition structure rather than baking the stationary law into the rates. It does not move gap2_measure_derived. Landmark contact is local to Gap-2 gluing/insertion stationarity, not T5–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.