curvature_numerator
plain-language theorem explainer
Curvature numerator adds the count of face-wallpaper pairs to the count of active edges to produce the integer numerator for the first-order curvature correction δ₁. Workers on higher-order voxel-seam corrections to α⁻¹ cite this definition when assembling the series α⁻¹ = α_seed − f_gap + Σ δ_n that targets the CODATA value. The definition is a direct arithmetic sum of two constants from the Q₃ cube combinatorics.
Claim. The curvature numerator is the sum $N_c = N_{fw} + N_a$, where $N_{fw}$ is the number of face-wallpaper pairs on the cube and $N_a$ is the number of active edges.
background
The module develops higher-order voxel-seam corrections to α⁻¹ through the series α⁻¹ = α_seed − f_gap + Σ_{n=1}^∞ δ_n, with each δ_n a finite sum over n-fold face-wallpaper configurations on Q₃ weighted by the Z₂⁵ half-period measure. The curvature numerator enters the explicit first-order term δ₁ = -103/(102π⁵) that reduces the residual gap to CODATA 137.035999206(11). Upstream, active_edges is defined as 1 and face_wallpaper_pairs as the product Q3_faces × wallpaper_groups; the module doc states that the additive and exponential formulas using this correction yield values within a few ppm of experiment.
proof idea
The definition is a direct sum of the two upstream constants face_wallpaper_pairs and active_edges.
why it matters
This definition supplies the numerator 103 that appears in δ₁, the leading curvature correction that closes part of the ~8 ppm residual in the RS derivation of α⁻¹. It is referenced by AlphaFrameworkCert to certify that cube combinatorics, wallpaper groups, and the first correction are in place for the open δ₂ computation, and by the theorems delta_1_structure, delta_1_numerator, and delta_1_neg that fix the explicit rational form and negative sign of the correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.