additive_map_not_factorizing
plain-language theorem explainer
The additive display g(ε)=1−ε fails multiplicative factorization over independent loads: g(x+y)=g(x)g(y) is false on ℝ. Cited when ruling out the linear truncation as a structural alternative to exponential dressing of the α seed. Proof is a direct numerical counterexample at (1,1).
Claim. It is not the case that for all real $x,y$ one has $1-(x+y)=(1-x)(1-y)$.
background
In Alpha Genesis M1 (resummation forcing), the surviving coupling fraction after paying gap cost ε is treated as a recognition weight. Independent gap loads compose additively in cost, so any admissible response must factorize: $g(\varepsilon_1+\varepsilon_2)=g(\varepsilon_1)\cdot g(\varepsilon_2)$, the same factorization premise that forces the T9 continuum measure.
Two candidate displays appear in the no-fit proposition: the exponential form (E), $g(\varepsilon)=e^{-\varepsilon}$, and the additive truncation (A), $g(\varepsilon)=1-\varepsilon$. The module shows (E) is the unique response that factorizes and has unit linear response $g'(0)=-1$. Before uniqueness, one must check that (A) is not even a factorizing map.
This lemma isolates that purely algebraic failure, with no derivative or response-structure hypotheses.
proof idea
Assume the universal identity $1-(x+y)=(1-x)(1-y)$. Specialize to $x=y=1$ to obtain $1-2=(1-1)(1-1)$, i.e. $-1=0$. norm_num discharges the numerical contradiction. No external lemmas are required.
why it matters
Closes discrete choice (i) of the no-fit proposition on resummation form: form (A) is not a structural competitor to form (E), only its first-order display. The module theorem then forces the dressing response to be exactly $\varepsilon\mapsto e^{-\varepsilon}$, so that $\alpha^{-1}$ equals the seed times the T9 forced continuum weight at the spectral gap load. That unification ties the fine-structure dressing to the same measure that fixes $\hbar=\varphi^{-5}$ and the rung-44 scale. No downstream Lean users are wired yet; the lemma is local scaffolding for no_additive_response and response_forced in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.