pith. sign in
theorem

delta_1_denominator_nat

proved
show as:
module
IndisputableMonolith.Constants.AlphaHigherOrder
domain
Constants
line
109 · github
papers citing
none yet

plain-language theorem explainer

The number of face-wallpaper pairs on the Q3 voxel lattice equals 102. Researchers computing the first-order curvature correction to the fine-structure constant in Recognition Science cite this integer when forming δ₁ = -103/(102 π^5). The count arises as the product of cube faces and wallpaper symmetry groups. The proof is a direct one-line wrapper applying the reflexivity equality on that product definition.

Claim. The number of face-wallpaper pairs on the three-dimensional cube lattice $Q_3$ equals 102: $|$face-wallpaper pairs$| = 102$.

background

Recognition Science expands α^{-1} = α_seed - f_gap + Σ_{n=1}^∞ δ_n, where each δ_n is a combinatorial sum over n-fold face-wallpaper configurations on Q3 weighted by the Z₂^5 half-period measure. The module defines face-wallpaper pairs as the product Q3_faces × wallpaper_groups. The upstream theorem face_wallpaper_pairs_eq records that this product evaluates to 102 by reflexivity on the definition.

proof idea

The proof is a one-line wrapper that applies the equality theorem face_wallpaper_pairs_eq, which itself holds by reflexivity on the product definition face_wallpaper_pairs := Q3_faces * wallpaper_groups.

why it matters

This supplies the explicit denominator 102 that appears in the first-order correction δ₁ = -103/(102 π^5) ≈ -0.00330, tightening the additive and exponential formulas toward the CODATA value 137.035999. It anchors the series framework for arbitrary-order voxel-seam corrections on Q3. The open deliverable remains the explicit computation of δ₂.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.