dressedCoupling
plain-language theorem explainer
Defines the form-(E) dressed coupling as seed times exponential attenuation of the normalized gap load: $S\,e^{-\delta/S}$. Alpha-genesis and fine-structure work cite it as the unique admissible dressing once factorization and unit linear response are imposed. The body is a one-line arithmetic definition, not a derived equality.
Claim. For real seed $S$ and gap load $\delta$, the dressed coupling is $S\,\exp(-\delta/S)$: the seed multiplied by the forced exponential response at the normalized load $\delta/S$.
background
Module Alpha Genesis M1 (Resummation Forcing) shows that exponential dressing of the $\alpha$ seed is not a convention. Any dressing response that factorizes over independent gap loads and has unit linear response at zero load is exactly $\varepsilon \mapsto \exp(-\varepsilon)$. The additive display $\varepsilon \mapsto 1-\varepsilon$ fails factorization (witness $\varepsilon_1=\varepsilon_2=1$).
Factorization is inherited from MeasureForcing: independent composition multiplies weights, both at the lattice layer (RecognitionWeightRule.factorizes) and in the continuum premise of continuum_weight_forced. Surviving coupling after paying gap cost $\varepsilon$ is a recognition weight; independent loads add in cost, so the response must satisfy $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1),g(\varepsilon_2)$. Calibration $g'(0)=-1$ is the dressing analog of T5 unit log-curvature at the identity.
Here $S$ is the bare seed coupling and $\delta$ the gap load; the normalized argument is $\delta/S$. The definition packages seed times that forced response into a single real-valued map.
proof idea
Pure definition: expand as the product of the seed $S$ with $\mathrm{Real.exp}$ of the negated normalized load $-(\delta/S)$. No lemmas, tactics, or hypotheses. Downstream theorems rewrite a general DressingResponse into this closed form via response_forced.
why it matters
Anchors the unique form-(E) object that discharges discrete choice (i) of the no-fit proposition: exponential resummation versus additive truncation. Parent theorem dressedCoupling_forced states that every admissible dressing response yields exactly this map: $S\cdot R.g(\delta/S)=\mathrm{dressedCoupling},S,\delta$, by rewriting with response_forced.
That identity feeds the unification corollary alphaInv_eq_seed_mul_forced_weight: certified $\alpha^{-1}$ is the channel budget of $\partial Q_3$ attenuated by the T9 forced continuum weight at spectral gap load per channel ($w_8/(44\pi)$ in rung units). Same measure that fixes $\hbar=\varphi^{-5}$, $\theta=\varphi^{-4}$, and the rung-44 scale. Places $\alpha$ dressing inside the Recognition Composition / measure-forcing chain rather than as a free resummation choice. STATUS target: theorem file with zero sorry and no CODATA.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.