AlphaPrecisionHypothesis
plain-language theorem explainer
The AlphaPrecisionHypothesis structure packages a sequence of real corrections deltas such that deltas(1) equals the first-order curvature term delta_1 and the partial sums alpha_seed minus deltas(1) plus the sum of the first N deltas converge to the CODATA value of alpha inverse. Researchers refining the Recognition Science derivation of the fine-structure constant would cite this to close the residual gap with experiment. The declaration is a direct structure definition that encodes the convergence target using the existing partial_alpha and
Claim. Let $d : {N} {to} {R}$ be a sequence with $d(1) = delta_1$, where $delta_1$ is the first-order curvature correction. The partial sums $alpha_{seed} - d(1) + sum_{k=1}^N d(k)$ converge to the CODATA value $137.035999206$ as $N to infty$.
background
The module develops higher-order voxel-seam corrections to alpha inverse in Recognition Science. The geometric seed is defined as alpha_seed = 4 pi times 11 from the ledger structure. The first-order term is delta_1 = -curvature_numerator over (face_wallpaper_pairs times pi to the measure_dimension). The partial_alpha function returns the truncated series alpha_s minus f_g plus the sum of the first N deltas, and CODATA_alpha_inv is the explicit real 137.035999206. The module states that the full series takes the form alpha inverse equals alpha_seed minus f_gap plus sum delta_n, with the present structure supplying the convergence hypothesis for that series.
proof idea
This is a structure definition with no proof body. It directly assembles the three fields: the deltas function from naturals to reals, the equality delta_1_matches, and the Filter.Tendsto statement that the partial_alpha sequence converges to CODATA_alpha_inv at infinity. No lemmas or tactics are invoked; the declaration is a pure packaging of the hypothesis using the sibling definitions of partial_alpha, delta_1, and CODATA_alpha_inv.
why it matters
The definition supplies the explicit target hypothesis for the higher-order corrections developed in the AlphaHigherOrder module. It directly addresses the open delta_2 computation identified as the key deliverable in the module status. Within the Recognition Science framework it supports closure of the alpha inverse derivation inside the documented band (137.030, 137.039) by requiring the series to reach the experimental CODATA value. The structure rests on the upstream definitions of alpha_seed and delta_1 together with the partial_alpha summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.