dressedCoupling_forced
plain-language theorem explainer
Any admissible dressing response applied to a seed S at gap load δ produces exactly the exponential form-(E) dressed coupling S·exp(−δ/S). Researchers assembling the fine-structure constant in Recognition Science cite this to kill resummation freedom: form (E) is forced, form (A) is only a first-order display. The proof is a one-line rewrite through the forced exponential response, then definitional equality.
Claim. For every dressing response $R$ (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 $g'(0)=-1$) and all real $S,\delta$, one has $S\cdot g(\delta/S)=S\cdot\exp(-(\delta/S))$.
background
Alpha Genesis M1 treats the exponential dressing of the α seed as forced structure, not a resummation convention. A dressing response is the fraction of coupling budget that survives a gap load ε. Its two fields are inherited ledger premises: factorization over independent loads (the same premise that forces the T9 continuum measure) and unit linear response at zero load (the dressing analog of T5 unit log-curvature at the identity).
Upstream, resummation forcing already proves every such response equals $g(\varepsilon)=\exp(-\varepsilon)$. There is no free choice of resummation form. The dressed coupling is defined as seed times that forced response at normalized load: $S\cdot\exp(-(\delta/S))$. The additive display $\varepsilon\mapsto 1-\varepsilon$ fails factorization (witness $\varepsilon_1=\varepsilon_2=1$) and is only the first-order truncation of the exponential.
The factorization premise is not α-specific. Independent gap loads compose additively in cost; unpaid correlation between independent channels is forbidden by ledger additivity, so survival fractions must multiply.
proof idea
One-line wrapper. Rewrite the left-hand side by the structure theorem that any dressing response satisfies $g(\varepsilon)=\exp(-\varepsilon)$, evaluated at $\varepsilon=\delta/S$. The resulting term $S\cdot\exp(-(\delta/S))$ is definitionally the dressed coupling, so rfl closes.
why it matters
Discharges discrete choice (i) of the no-fit proposition: exponential form (E) versus additive form (A). Every admissible dressing yields exactly form (E); form (A) is not a factorizing response at all. That is the local content of resummation forcing applied to the coupling assembly.
The immediate conceptual consumer is the unification corollary in the same module: certified $\alpha^{-1}$ equals the channel budget $4\pi\cdot 11$ times the T9 forced continuum weight at spectral gap load per channel $w_8/(44\pi)$ in rung units. The α dressing factor is not α-specific structure. It is the unique recognition weight forced by factorization plus self-similar calibration, the same measure lineage that fixes $\hbar=\varphi^{-5}$ and the rung-44 scale. The α band near $(137.030,137.039)$ is thereby tied to T9 rather than to a fit.
No recorded downstream dependents yet; the sibling identity equating α inverse to seed times forced weight is the natural landing site. Infrared boundary value $\alpha^{-1}(0)=137.035999$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.