additive_residual
plain-language theorem explainer
The additive residual definition isolates the difference between the CODATA value of α^{-1} and the first-order additive approximation built from the geometric seed, gap weight, and initial curvature term. Researchers extending the Recognition Science series for the fine-structure constant would cite this quantity to size the total contribution still required from higher-order voxel-seam corrections. The definition is a direct algebraic subtraction of the partial sum from the fixed CODATA constant.
Claim. The additive residual is the real number given by $r(w_8) := 137.035999206 - (4π · p - w_8 ln φ + δ_1)$, where $p$ is the number of passive edges, $φ$ is the golden ratio, and $δ_1$ is the first-order curvature correction; this quantity equals the sum of all remaining higher-order terms needed to reach the experimental value.
background
The module AlphaHigherOrder develops higher-order voxel-seam corrections to the Recognition Science derivation of α^{-1}. The derivation begins with a geometric seed equal to 4π times the count of passive edges on the Q3 lattice, subtracts a gap weight obtained from the DFT-8 projection, and adds the first-order curvature correction δ_1 = -103/(102 π^5). The resulting partial sum lies approximately 8 ppm below the CODATA value 137.035999206, leaving an explicit residual that the infinite series of subsequent δ_n terms must close.
proof idea
The definition is a one-line wrapper that subtracts the partial additive expression (alpha_seed minus f_gap applied to the supplied w8_val, plus delta_1) from the constant CODATA_alpha_inv. No tactics or lemmas are invoked beyond direct reference to the four upstream definitions.
why it matters
This definition quantifies the exact shortfall that the remaining series Σ_{n≥2} δ_n must supply, thereby framing the open computation of δ_2 as the next required step in the module. It sits inside the higher-order correction framework whose goal is to derive α^{-1} from the Recognition Science constants (geometric seed, gap weight, and curvature terms) without external fitting. The parent series structure α^{-1} = α_seed − f_gap + Σ δ_n is stated explicitly in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.