reduced_configs_2
plain-language theorem explainer
The theorem establishes that the symmetry-reduced count of 2-fold face-wallpaper configurations on the 3-cube equals 217. Researchers assembling the series for higher-order corrections to the inverse fine-structure constant would cite this integer when evaluating the n=2 term in the δ_n summation. The proof is a direct native evaluation of the configuration-counting definition at input 2.
Claim. The symmetry-reduced number of 2-fold face-wallpaper configurations on the 3-cube equals 217.
background
The module develops higher-order voxel-seam corrections to α^{-1} that address the residual discrepancy with CODATA after the geometric seed, gap weight, and first-order curvature term. It defines combinatorial objects on the 3-cube Q₃ (faces, wallpaper groups, face-wallpaper pairs) together with the Z₂^5 half-period integration measure that weights each n-fold configuration. The upstream definition supplies the symmetry-reduced configuration count as n_fold_configs n divided by the automorphism order of Q₃ plus one, serving as an upper bound for the series α^{-1} = α_seed - f_gap + Σ δ_n.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression for the symmetry-reduced configuration count at n=2.
why it matters
This supplies the n=2 configuration count required by the alphaFramework certification of the cube combinatorics. It advances the Recognition Science program for arbitrary-order δ_n corrections in the α^{-1} derivation, where the series targets the CODATA value 137.035999206. The explicit computation of δ₂ itself remains the principal open deliverable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.