half_period_dim
plain-language theorem explainer
The half-period measure dimension is set equal to the integration measure dimension. Researchers deriving higher-order voxel-seam corrections to α⁻¹ in Recognition Science cite it when weighting sums over Q₃ face-wallpaper pairs by the Z₂ integration measure. The definition is realized as a direct abbreviation of the upstream measure_dimension that sums three spatial dimensions with one temporal and one conservation contribution.
Claim. The half-period measure dimension is the natural number defined by the integration measure dimension $D + 1 + 1 = 5$, where $D = 3$ denotes the number of spatial dimensions.
background
The module develops the series structure for higher-order corrections to α⁻¹, with each δ_n formed as a finite sum over n-fold face-wallpaper configurations on Q₃ weighted by the Z₂ half-period integration measure. The upstream measure_dimension is defined as the integration measure dimension D + 1 (temporal) + 1 (conservation). This supplies the exponent for the sector count in the Z₂-weighted sums that appear in the additive and exponential formulas for α⁻¹.
proof idea
The declaration is a one-line abbreviation that directly aliases the upstream measure_dimension definition.
why it matters
This definition supplies the dimension parameter for the Z₂ half-period sectors used in the δ_n corrections. It is referenced by the theorem half_period_dim_eq, which establishes equality to 5, and by Z2_sectors, which defines the sector count as 2 raised to this power. It closes the counting step in the Recognition Science framework for the series α⁻¹ = α_seed − f_gap + Σ δ_n, linking to D = 3 and the eight-tick octave. The explicit computation of δ₂ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.