response_forced
plain-language theorem explainer
Any factorizing dressing response with unit linear response equals the pure exponential g(ε)=exp(−ε). Alpha-genesis and fine-structure work cite this to eliminate resummation freedom between forms (E) and (A). The proof shows that g(x)exp(x) has vanishing derivative everywhere, hence is constantly 1 by the zero-load normalization g(0)=1.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be a dressing response that factorizes, $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1)g(\varepsilon_2)$, and has unit linear response $g'(0)=-1$. Then $g(\varepsilon)=e^{-\varepsilon}$ for every real $\varepsilon$.
background
Module Alpha Genesis M1 (Resummation Forcing) treats the surviving coupling fraction after paying a gap cost ε as a recognition weight. Independent gap loads compose additively in cost; ledger additivity forbids unpaid correlations, so the response must factorize: $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1)\cdot g(\varepsilon_2)$. That premise is inherited from MeasureForcing (RecognitionWeightRule.factorizes and the continuum Factorizes hypothesis behind continuum_weight_forced), not invented for α.
Unit linear response $g'(0)=-1$ is the dressing analog of T5's IsCalibrated (unit log-curvature at the identity). Upstream, g_zero records that zero load means no dressing: $g(0)=1$ (the alternative $g(0)=0$ collapses $g$ identically and contradicts unit response). hasDerivAt_neg_self propagates the calibrated derivative from the origin: factorization yields $g'(x)=-g(x)$ at every point.
The module's target is to discharge discrete choice (i) of the no-fit proposition: resummation form (E) versus the additive display (A). Form (A) is only a first-order truncation of (E), not a structural alternative.
proof idea
Form the auxiliary $h(x)=g(x),e^{x}$. At each $x$, multiply hasDerivAt_neg_self (derivative $-g(x)$) by the standard derivative of exp; the product rule and a one-line ring cleanup give HasDerivAt $h$ $0$ $x$. Differentiability and vanishing derivative follow at once.
Apply is_const_of_deriv_eq_zero between $x$ and $0$ to obtain $g(x)e^{x}=g(0)e^{0}$. Feed g_zero so the right-hand side is $1$. Since $e^{x}\neq 0$, multiply by the inverse and rewrite via exp_neg to conclude $g(x)=e^{-x}$. The outer intro on ε is just specialization.
why it matters
This is the M1 closure: the exponential dressing of the α seed is forced, not a resummation convention. Downstream, dressedCoupling_forced rewrites any response into the unique form-(E) dressed coupling $S\cdot g(\delta/S)$. response_is_forced_measure and natural_display identify the calibrated M1 response with the T9 continuum weight in natural log units, so the α dressing factor is contWeight at the spectral gap load per channel.
AlphaGenesisCert bundles clause 4 as "the dressing response is forced to exp(−ε); the additive display is excluded (M1)." CalibrationForcingCert and alphaInvGenesis_from_selfSimilar sit one layer up, reading the same object as φ-ladder self-similar dressings. The unification corollary alphaInv_eq_seed_mul_forced_weight then states that the fine-structure constant is the channel budget of ∂Q₃ attenuated by the unique recognition weight — the same measure that fixes ℏ=φ⁻⁵ and the rung-44 scale. No CODATA enters the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.