Z2_sectors
plain-language theorem explainer
The declaration defines the number of Z₂ half-period sectors as two raised to the half-period dimension. Researchers assembling combinatorial weights for voxel-seam corrections to α⁻¹ in Recognition Science would reference this count when forming the integration measure over Q₃ configurations. The definition is a direct power expression that inherits its value from the upstream measure dimension.
Claim. Let $Z_2$ denote the number of half-period sectors. Then $Z_2 = 2^d$, where $d$ is the half-period measure dimension.
background
The module formalizes higher-order voxel-seam corrections to α⁻¹ to close the ~8 ppm residual in the RS derivation. The series is α⁻¹ = α_seed − f_gap + Σ_{n=1}^∞ δ_n, where each δ_n is a finite sum over n-fold face-wallpaper pairs on Q₃ weighted by the Z₂⁵ half-period integration measure. The upstream half-period dimension is defined as the measure dimension and supplies the exponent for the sector count.
proof idea
This is a one-line definition that directly computes two to the power of the half-period dimension supplied by the upstream result.
why it matters
This definition supplies the Z₂ sector count that enters the AlphaFrameworkCert structure and the equality theorem proving the count equals 32. It supports the series framework for computing δ_n corrections to α⁻¹, addressing the open ~8 ppm residual. The module leaves δ₂ computation as the key open deliverable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.