delta_1_neg
plain-language theorem explainer
δ₁ is shown negative as the leading curvature correction in the Recognition Science expansion of α^{-1}. Researchers computing the alternating series for the fine-structure constant cite this to fix the sign of the first term in the additive formula. The tactic proof unfolds the definition of δ₁ then applies simplification to confirm the numerator is positive while the denominator is positive.
Claim. $δ_1 < 0$, where $δ_1 = -N/D$ with numerator $N =$ face-wallpaper pairs plus active edges and denominator $D =$ face-wallpaper pairs times $π$ to the measure dimension.
background
The module develops higher-order voxel-seam corrections to α^{-1} within the Recognition Science framework. It defines the first-order term via cube combinatorics: face-wallpaper pairs equals the number of faces on Q₃ times the 17 wallpaper groups, active edges equals 1, curvature numerator equals their sum, and measure dimension supplies the exponent on π. The local setting is the series α^{-1} = α_seed − f_gap + Σ δ_n, with δ₁ supplying the curvature correction of order −0.00330. Upstream results include the crystallographic count of 17 wallpaper groups and the structure of nuclear densities on φ-tiers.
proof idea
The proof unfolds the definition of δ₁. It applies simp to the curvature numerator, face-wallpaper pairs, Q3 faces, wallpaper groups, and active edges to obtain strict positivity of the numerator. A second simp establishes positivity of face-wallpaper pairs. The denominator is shown positive by multiplying that quantity by the positive power of π. The final step invokes division of a negative quantity by a positive quantity.
why it matters
The result fixes the sign of the leading correction so that the additive formula yields approximately 137.035, consistent with the module's target near CODATA. It is a proved step in the series framework whose parent is the full expansion α^{-1} = α_seed − f_gap + Σ δ_n. The declaration closes the first term of the alternating series while the open question remains explicit computation of δ₂. It aligns with the eight-tick octave and D = 3 through the measure dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.