DressingResponse
plain-language theorem explainer
Packages the two ledger premises that force exponential dressing of the fine-structure seed: a survival fraction g of gap load that multiplies on independent loads and has unit slope −1 at zero load. Cited by anyone proving that form-(E) resummation is unique and that the additive display is excluded. Definition only; uniqueness is proved downstream from these fields.
Claim. A dressing response is a map $g:\mathbb{R}\to\mathbb{R}$ such that $g(x+y)=g(x)\,g(y)$ for all real $x,y$ (factorization over independent gap loads) and $g'(0)=-1$ in the sense of a derivative at zero (unit linear response / calibration).
background
Module Alpha Genesis M1 (Resummation Forcing) shows that exponential dressing of the $\alpha$ seed is not a convention: any response that factorizes over independent gap loads and has unit linear response at zero is exactly $\varepsilon\mapsto\exp(-\varepsilon)$. The additive display $\varepsilon\mapsto 1-\varepsilon$ fails factorization (witness $\varepsilon_1=\varepsilon_2=1$) and is only a first-order truncation.
Factorization is inherited from the same premise that forces the T9 continuum measure: independent composition multiplies weights (RecognitionWeightRule / Factorizes in MeasureForcing). Surviving coupling after paying gap cost $\varepsilon$ is a recognition weight; independent loads add in cost by ledger additivity, so $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1)g(\varepsilon_2)$. The calibration $g'(0)=-1$ is the dressing analog of T5 unit log-curvature at the identity.
Zero load implies $g(0)=1$: the alternative $g(0)=0$ collapses $g$ to zero and contradicts unit response.
proof idea
No proof body: this is a structure bundling two fields. The map $g$ is the survival fraction; factorizes is the Cauchy multiplicative equation on additive loads; unit_response is HasDerivAt g (-1) 0. Downstream lemmas (response_forced, no_additive_response, dressedCoupling_forced) discharge uniqueness and exclusion from these axioms alone.
why it matters
This is the M1 interface that discharges discrete choice (i) of the no-fit proposition: form (E) versus (A). Downstream, response_forced identifies every such $g$ with $\exp(-\varepsilon)$; no_additive_response excludes $1-\varepsilon$; dressedCoupling_forced says any response yields the form-(E) dressed coupling; response_is_forced_measure equates the dressing to the T9 forced measure via $g(\ln\varphi\cdot t)=\mathrm{contWeight}(t)$.
It feeds AlphaGenesisCert (item 4: dressing forced to $\exp(-\varepsilon)$) and CalibrationForcingCert / natural_display (M1 calibrated response as natural-units display of self-similar dressing). Unification corollary: $\alpha^{-1}$ is the channel budget attenuated by the unique recognition weight—the same measure that fixes $\hbar=\varphi^{-5}$ and related scales. STATUS target: theorem, zero sorry, no CODATA in-file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.