alpha_abs_le_half

Recognition cost is $J(x)=(x+x^{-1})/2-1$ (T5 unique cost, also written $\cosh(\log x)-1$). The module builds a concrete perturbative step for lepton $\alpha$-correction channels: specialize the proved small-strain expansion of $J$ at $x=1+\varepsilon$ to $\varepsilon=\alpha$, then decompose into a leading quadratic channel $\alpha^2$ and a cubic channel scaling with edge count times $\alpha^3$.

Here $\alpha$ is the electromagnetic fine-structure constant ($\alpha_{\mathrm{EM}}=1/\alpha_{\mathrm{inv}}$ in the constants layer). The $J(1+\varepsilon)$ expansion used in JcostCore needs $|\varepsilon|\le 1/2$ for remainder control. Upstream electron-mass necessity already supplies quantitative bounds placing $\alpha$ near $1/137$, well inside that disk.

Pull Physics.ElectronMass.Necessity.alpha_bounds, which gives a strict lower estimate $\alpha>0.007297$ (and a matching upper bound). Transitivity with the numeric fact $0<0.007297$ yields $\alpha\ge 0$, so $|\alpha|=\alpha$ by abs_of_nonneg. A final linarith step discharges $\alpha\le 1/2$ from those bounds. No expansion identity is proved here; only the radius hypothesis.

Gate lemma for jcost_one_plus_alpha_expansion, which specializes the proved $J(1+\varepsilon)$ quadratic-plus-cubic expansion to $\varepsilon=\alpha$ and obtains $J(1+\alpha)=\alpha^2/2+c\alpha^3$ with $|c|\le 2$. That feeds the doubled form, edge-aggregated two-$J$ channels, the unique cubic coefficient, and the O4 mass-layer closure (Masses.JCostPerturbation).

Module intent: remove ad-hoc handling of correction orders and tie lepton $\alpha$-channels to the existing $J$-cost calculus surface (RCL / T5 $J$-uniqueness). The $\alpha$ band used across RS constants (including the $\alpha^{-1}\in(137.030,137.039)$ window) is thereby connected to a certified expansion radius rather than an informal smallness claim.