g_zero
plain-language theorem explainer
Any factorizing dressing response with unit linear response at zero load satisfies g(0)=1: zero gap cost means no dressing. The resummation-forcing theorem cites this as the constant term before proving g(ε)=exp(−ε). Proof splits on g(0)=g(0)² from factorization; the zero root collapses g everywhere and contradicts the calibrated derivative g′(0)=−1.
Claim. Let $R$ be a dressing response: a map $g:\mathbb{R}\to\mathbb{R}$ that factorizes over independent loads, $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1)\,g(\varepsilon_2)$, and has unit linear response $g'(0)=-1$. Then $g(0)=1$.
background
Module Alpha Genesis M1 forces the exponential dressing of the fine-structure seed. A dressing response is a real map $g$ on gap load $\varepsilon$ that records the surviving coupling fraction after paying cost $\varepsilon$. Factorization $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1),g(\varepsilon_2)$ is inherited from the same ledger-additivity premise that forces the T9 continuum measure: independent gap loads compose additively in cost, so unpaid correlations are forbidden and weights multiply.
Unit linear response $g'(0)=-1$ is the dressing analog of T5 calibration (unit log-curvature at the identity). The module theorem is that any such $g$ equals $\varepsilon\mapsto\exp(-\varepsilon)$; the additive display $1-\varepsilon$ fails factorization outright. This lemma pins the value at the origin before the derivative-propagation argument runs.
proof idea
Factorization at $(0,0)$ yields $g(0)=g(0)\cdot g(0)$. Rearrange to $g(0),(g(0)-1)=0$. By the real zero-divisor law, either $g(0)=0$ or $g(0)=1$.
If $g(0)=0$, factorization at $(x,0)$ forces $g(x)=0$ for every $x$, so $g$ is the zero function. Unit response then says the zero function has derivative $-1$ at $0$. Uniqueness of derivatives against the constant-zero derivative gives $-1=0$, contradiction.
The remaining root is $g(0)=1$, finished by linarith on $g(0)-1=0$.
why it matters
Feeds response_forced, the main resummation-forcing theorem: any factorizing unit-response dressing is exactly $g(\varepsilon)=\exp(-\varepsilon)$. That result discharges discrete choice (i) of the no-fit proposition (form (E) vs (A)): the exponential is the unique admissible response; the additive display is only its first-order truncation.
Downstream, the forced weight unifies with T9: alphaInv_eq_seed_mul_forced_weight identifies the $\alpha$ dressing factor with the continuum recognition measure at the spectral gap load per channel. Same measure family that fixes $\hbar=\varphi^{-5}$ and the rung-44 scale. Without $g(0)=1$, the constant in the $h(x)=g(x)e^{x}$ argument of response_forced would be free and the exponential would not be pinned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.