z8Size_2cubed
plain-language theorem explainer
The cardinality of the cyclic group ℤ/8ℤ equals 2 cubed. Researchers constructing DFT-8 within Recognition Science cite this to fix the group order to the eight-tick octave. The proof is a one-line decision procedure that evaluates the constant definition of the group size.
Claim. $|\mathbb{Z}/8\mathbb{Z}| = 2^3$
background
The module develops abstract harmonic analysis from Recognition Science by listing five canonical locally compact groups (ℝ, ℤ, S¹, ℚₚ, GL_n(ℚ)) whose configuration dimension equals D = 5. DFT-8 is harmonic analysis on the cyclic group ℤ/8ℤ of order 8 = 2^D, with Pontryagin duality supplying the recognition-phase link between ℤ and S¹. The upstream definition z8Size sets this cardinality to the natural number 8 and records that ℤ/8ℤ has 8 elements equal to 2 cubed.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the definition z8Size := 8, confirming equality with 2^3 by direct computation.
why it matters
This theorem supplies the z8_size field inside the AbstractHarmonicAnalysisCert record that certifies the five-group structure together with the order-8 group for DFT-8. It anchors the eight-tick octave (T7) and the spatial dimension D = 3 inside the forcing chain. The module records that the entire development has zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.