exponential_residual
plain-language theorem explainer
The declaration defines the exponential residual as the difference between the geometric-seed exponential approximation to α^{-1} and the CODATA target value, parameterized by gap weight w8_val. Researchers refining the Recognition Science derivation of the fine-structure constant would cite this quantity to quantify the +6 ppm overshoot before adding voxel-seam corrections. It is a direct one-line definition that multiplies the seed by the exponential of the negative scaled gap and subtracts the experimental target.
Claim. Let α_seed = 4π × (passive edge count) be the geometric seed, f_gap(w_8) = w_8 ln φ with φ the golden ratio, and α^{-1}_CODATA = 137.035999206. The exponential residual is then α_seed ⋅ exp(−f_gap(w_8)/α_seed) − α^{-1}_CODATA.
background
In the Recognition Science framework the inverse fine-structure constant begins from a geometric seed α_seed = 4π × 11 ≈ 138.23, representing baseline spherical closure cost over 11-edge interaction paths. The gap weight f_gap(w_8) = w_8 ln φ arises from the DFT-8 projection on the eight-tick octave, with φ = (1 + √5)/2. Module AlphaHigherOrder formalizes higher-order voxel-seam corrections to close the residual between these approximations and the CODATA value 137.035999206, contrasting the additive formula α_seed − f_gap + δ_1 ≈ 137.035 with the exponential form α_seed exp(−f_gap/α_seed) ≈ 137.037.
proof idea
This is a direct definition that computes the residual by multiplying the geometric seed by the exponential of the negative scaled gap weight and subtracting the CODATA value. No lemmas are applied; it is a one-line algebraic expression using the imported definitions of the seed, gap weight, and CODATA target.
why it matters
The definition isolates the exponential overshoot above CODATA inside the series α^{-1} = α_seed − f_gap + Σ δ_n, where each δ_n is a combinatorial sum over n-fold face-wallpaper configurations on Q_3. It supports the module's framework for bounding the alternating convergent series of voxel-seam corrections and connects to the Recognition Science constants pipeline (T5 J-uniqueness, T7 eight-tick octave). The module status records that δ_2 computation remains open; this residual supplies the diagnostic needed to close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.