half_period_dim_eq
plain-language theorem explainer
The equality fixes the half-period dimension for the Z₂ measure on Q₃ voxel-seam corrections at exactly 5. Workers deriving higher-order terms δ_n in the α⁻¹ series cite this to anchor the integration weight over face-wallpaper configurations. The proof reduces directly by reflexivity to the definition of half_period_dim as measure_dimension.
Claim. The dimension of the half-period measure equals 5.
background
In the Recognition Science derivation of α⁻¹, higher-order corrections δ_n arise as finite combinatorial sums over n-fold face-wallpaper configurations on Q₃, weighted by the Z₂ half-period integration measure. The half-period dimension is introduced as the measure dimension in the AlphaHigherOrder module, which supplies the Z₂⁵ structure for the series α⁻¹ = α_seed − f_gap + Σ δ_n. Upstream results include the spectral emergence structure on Q₃ (forcing SU(3)×SU(2)×U(1) content, three generations, and 24 chiral flavors) and the phi-forcing derived J-cost structure.
proof idea
The proof is a one-line reflexivity wrapper that applies the definition of half_period_dim directly to the constant 5.
why it matters
This declaration anchors the integration measure for the higher-order voxel-seam corrections framework, which targets the ~8 ppm residual between the RS seed formula and CODATA. It supports the proved cube combinatorics and δ₁ structure while leaving the explicit δ₂ computation open. The result closes the Z₂ half-period sector count used in the alternating convergent series bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.