Z2_sectors_eq
plain-language theorem explainer
Z2_sectors_eq fixes the number of Z₂ half-period sectors at exactly 32. Researchers assembling the combinatorial weights for the series expansion of α^{-1} cite this count when summing n-fold voxel-seam corrections on Q₃. The proof is a direct native evaluation of the power in the sector definition.
Claim. The number of ℤ₂ half-period sectors equals 32.
background
The module develops higher-order voxel-seam corrections to α^{-1} via the series α^{-1} = α_seed − f_gap + Σ δ_n, where each δ_n is a finite sum over n-fold face-wallpaper configurations on Q₃ weighted by the Z₂^5 half-period integration measure. Z2_sectors is defined as 2 raised to the half-period dimension and supplies the exact cardinality of those sectors. Upstream structures from ledger factorization and phi-forcing calibrate the J-cost and defect measures that enter the voxel-seam sums.
proof idea
The proof is a one-line term that applies native_decide to evaluate the power expression in the definition of the number of sectors.
why it matters
The result supplies the sector count required by alphaFramework, which certifies the cube combinatorics for the full series framework. It completes the proved portion of the higher-order corrections that target the ~8 ppm residual between the RS seed and CODATA. The open question it leaves is the explicit computation of the second-order term δ₂.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.