bakedFromWeight
plain-language theorem explainer
Manufactures birth-death rates from any positive size weight so detailed balance holds by pure algebra: birth is constantly one, death at size n+1 is the weight ratio f(n)/f(n+1). Gap-2 insertion auditors cite it as the canonical decoy that bakes the stationary law into the rates instead of counting moves. Construction is a structure instance; positivity follows from the weight hypothesis and division of positives.
Claim. Given a positive weight $f:\mathbb{N}\to\mathbb{R}$ with $f(n)>0$ for all $n$, define size-indexed birth-death rates by $\mathrm{birth}(n)=1$ for every $n$, $\mathrm{death}(0)=1$, and $\mathrm{death}(n+1)=f(n)/f(n+1)$. The resulting rates are strictly positive.
background
Gap-2 label-insertion dynamics asks which facts force InsertionStationarity (equivalently the GluingLaw), hence inverse-factorial weights and the GaugeCountingPrinciple, without smuggling those conclusions into the hypotheses. The module runs a necessary-reasons census: each candidate reason is proved, left open, marked MODEL, or refuted.
BirthDeathRates packages two size-indexed maps: birth n is the total forward rate n→n+1, death n the total backward rate n→n−1 (used at n=m+1), both required positive. Detailed balance for a weight f under such rates equates the weight ratio to the rate ratio. The ledger-side birth map (one fresh posting per tick, clipped at truncation) is the physical counting target this decoy deliberately fails to match.
The honesty block flags decoy rate laws that bake the stationary answer into the rates and therefore fail the derivation gate.
proof idea
Definitional structure instance, not a proof. Birth is the constant function 1; positivity is norm_num. Death is defined by cases: 1 at 0, and f n / f (n+1) at successors. Death positivity is div_pos applied to the two instances of the positivity hypothesis on f. No lemmas beyond elementary real arithmetic.
why it matters
This is the prompt's decoy rate law: it contains the stationary law, not a physical counting. Downstream, bakedFromWeight_balances shows DetailedBalance holds for every positive f by field simplification. D06_baked_rates_are_not_a_derivation packages that universal balance with the failure of InsertionStationarity on constantWeight, refuting "bake the weight into death" as a derivation route.
In InsertionAsymmetryInevitableReasons the same constructor scores the decoy: baking the inverse-factorial weight still satisfies CountingEquivalentRates, so the non-baked conjunct of RecognitionRateAsymmetry is load-bearing. Corrected floor plans (D06 rows) record the forced next step: asymmetric counting (size-blind birth vs per-label death) rather than renaming stationarity as a rate. Touches the OPEN item: derive the birth/death asymmetry from recognition structure without writing μ_{n+1}=(n+1)λ_n into the rates by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.