no_additive_response
plain-language theorem explainer
No dressing response equals the additive display ε ↦ 1−ε: that map fails factorization at loads (1,1). Anyone closing the discrete (E) versus (A) choice for the α dressing cites this exclusion. The proof is a direct contradiction from the structure's factorization field after rewriting.
Claim. Let $R$ be a dressing response: a map $g:\mathbb{R}\to\mathbb{R}$ that factorizes over independent gap loads ($g(x+y)=g(x)\,g(y)$) and has unit linear response at zero load. Then $g\neq(\varepsilon\mapsto 1-\varepsilon)$.
background
A dressing response is the surviving fraction of coupling budget after a gap load $\varepsilon$. Its two structural fields are inherited ledger premises: factorization over independent loads, and unit linear response at zero load (the dressing analog of T5 calibration).
Factorization is not an $\alpha$-specific choice. The same premise forces the T9 continuum measure: independent composition multiplies weights, because unpaid correlation between independent loads violates ledger additivity. Independent gap loads add in cost, so the survival fraction must multiply: $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1),g(\varepsilon_2)$.
This module (Alpha Genesis M1) shows the exponential form is the unique admissible response under those premises, and that the additive display $\varepsilon\mapsto 1-\varepsilon$ is not a factorizing response at all.
proof idea
Assume for contradiction that $g$ equals $\varepsilon\mapsto 1-\varepsilon$. Instantiate the structure's factorization identity at $x=y=1$: the left side is $g(2)=1-2=-1$, the right side is $g(1),g(1)=(1-1)^2=0$. Rewrite the assumed equality into that identity and discharge with norm_num. No other fields of the response are used.
why it matters
This lemma closes discrete choice (i) of the no-fit proposition for $\alpha$: resummation form (E) versus form (A). Form (A) is only the first-order truncation of the forced exponential, not a structural alternative. Downstream, AlphaGenesisCert bundles the claim that "the dressing response is forced to $\exp(-\varepsilon)$; the additive display is excluded (M1)."
Together with the uniqueness of the factorizing calibrated response, it feeds the unification corollary that the $\alpha$ dressing factor is the T9 forced measure evaluated at the spectral gap load per channel. That ties the fine-structure constant to the same recognition weight that fixes $\hbar=\varphi^{-5}$ and the rung-44 scale, with no CODATA input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.