face_wallpaper_pairs
plain-language theorem explainer
The definition computes the number of face-wallpaper pairs on the 3-cube as the product of its six faces and the seventeen wallpaper groups, yielding 102. Researchers assembling higher-order corrections to the inverse fine-structure constant cite this count when forming the denominator of the first curvature term δ1. It is introduced by direct multiplication of the two upstream constants.
Claim. Let $N_{fw}$ be the number of face-wallpaper pairs on the 3-cube $Q_3$. Then $N_{fw} := 6 × 17$, where the factor 6 is the number of faces of $Q_3$ and the factor 17 is the number of distinct two-dimensional wallpaper groups.
background
In the Recognition Science setting the 3-cube $Q_3$ supplies the geometric arena for voxel-seam corrections to α^{-1}. The module defines Q3_faces as 2 * 3 (hence 6) and imports wallpaper_groups as the fixed crystallographic count 17 established by Fedorov in 1891. These two integers multiply to give the base combinatorial factor for the n-fold configurations that appear in the series α^{-1} = α_seed − f_gap + Σ δ_n, with each δ_n a weighted sum over face-wallpaper pairs on Q3.
proof idea
The definition is a one-line wrapper that multiplies the value of Q3_faces by the value of wallpaper_groups.
why it matters
This definition supplies the denominator in the curvature correction δ1 = −(curvature_numerator) / (face_wallpaper_pairs ⋅ π^measure_dimension) and is required by the AlphaFrameworkCert structure that certifies all structural elements for the δ2 computation are in place. It closes the first-order combinatorial setup in the module's series expansion for α^{-1}, leaving explicit evaluation of δ2 as the remaining open task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.