z8Size_2cubed
plain-language theorem explainer
The cardinality of ℤ/8ℤ equals 8, hence 2^3. Researchers formalizing the Recognition Science derivation of discrete Fourier analysis on cyclic groups of order 2^D cite this when assembling the DFT-8 certificate. The proof is a one-line decision procedure that evaluates the constant definition of the group order.
Claim. $|ℤ/8ℤ| = 2^3$.
background
The module treats abstract harmonic analysis extracted from Recognition Science. It identifies five canonical locally compact groups (ℝ, ℤ, S¹, ℚₚ, GL_n(ℚ)) whose configuration dimension is D = 5. Within this setting, DFT-8 is harmonic analysis on the cyclic group ℤ/8ℤ of order 8 = 2^3, the eight-tick octave required by the forcing chain. The sibling definition z8Size simply records this order as the constant 8.
proof idea
One-line wrapper that applies the decide tactic to confirm the numerical equality after the definition of z8Size is unfolded.
why it matters
The result populates the z8_size field of AbstractHarmonicAnalysisCert, which certifies the five-group structure together with the DFT-8 size. It directly instantiates the eight-tick octave (period 2^3) and D = 3 spatial dimensions from the T7–T8 steps of the UnifiedForcingChain. No open question is left at this computational leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.