hasDerivAt_neg_self
plain-language theorem explainer
Any factorizing dressing response g with unit linear response at zero satisfies g'(x) = -g(x) at every real x. Factorization moves the calibrated derivative from the origin to an arbitrary basepoint. Cited by the resummation-forcing theorem that pins g(ε) = exp(-ε). The proof is a chain-rule plus constant-multiple argument that rewrites g via the Cauchy functional equation.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be a dressing response that factorizes, $g(a+b)=g(a)g(b)$, and has unit linear response $g'(0)=-1$. Then for every $x\in\mathbb{R}$, $g$ is differentiable at $x$ with $g'(x)=-g(x)$.
background
This module forces the exponential dressing of the fine-structure seed: any response that factorizes over independent gap loads and has unit linear response at zero load is exactly $\varepsilon\mapsto\exp(-\varepsilon)$. Factorization is inherited from the T9 measure-forcing premise (independent composition multiplies weights; unpaid correlations between independent loads violate ledger additivity). The calibration $g'(0)=-1$ is the dressing analog of T5 unit log-curvature at the identity.
A dressing response $R$ packages a map $g$ together with the factorization identity and the unit-response derivative at zero. The present lemma propagates that single calibrated derivative to every basepoint. Downstream, the product $g(x)\exp(x)$ is shown to have vanishing derivative, hence is constantly 1, which forces $g=\exp(-\cdot)$.
proof idea
Fix $x$. The shift $y\mapsto y-x$ has derivative $1$ at $x$. Compose with $g$: at the image point $0$, unit response gives $g'(0)=-1$, so the chain rule yields derivative $-1$ for $y\mapsto g(y-x)$. Multiply by the constant $g(x)$ to get derivative $-g(x)$ for $y\mapsto g(x),g(y-x)$. Factorization rewrites the product as $g(y)$ (after a ring cleanup of the arguments). Convert the derivative statement along that functional equality.
why it matters
Feeds response_forced, the main resummation-forcing theorem: any factorizing unit-response dressing is exactly $\exp(-\varepsilon)$, so there is no resummation freedom between exponential form (E) and additive display (A). That discharges discrete choice (i) of the no-fit proposition for $\alpha$: form (E) is the unique admissible response; form (A) is only its first-order truncation.
The unification corollary then identifies the $\alpha$ dressing factor with the T9 forced continuum weight evaluated at the spectral gap load per channel. Thus $\alpha^{-1}$ is the channel budget of $\partial Q_3$ attenuated by the same recognition measure that fixes $\hbar=\varphi^{-5}$ and the rung-44 scale. This lemma is the differential step that makes the uniqueness argument go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.