z8Size_2cubed
plain-language theorem explainer
The equality establishing that the cyclic group ℤ/8ℤ has cardinality 8, equivalently 2 cubed, is recorded as a theorem. Researchers assembling the abstract harmonic analysis certificate in Recognition Science would cite it to confirm the order of the cyclic group of order 2^D. The proof is a one-line decision procedure that verifies the numerical identity directly from the preceding definition.
Claim. The cardinality of the cyclic group $ℤ/8ℤ$ equals $2^3$.
background
The module develops abstract harmonic analysis from Recognition Science by identifying five canonical locally compact groups (ℝ, ℤ, S¹, ℚₚ, GL_n(ℚ)) whose configuration dimension is 5. Within this setting the discrete Fourier transform on the cyclic group ℤ/8ℤ is treated as DFT-8, with the order of that group fixed at 8. The upstream definition records that ℤ/8ℤ has 8 elements = 2^3, supplying the concrete natural-number value used by the present theorem.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality between the defined size and the power 2^3.
why it matters
The theorem supplies the z8_size field inside the abstractHarmonicAnalysisCert definition that certifies the five groups together with the order of ℤ/8ℤ. It directly instantiates the eight-tick octave (T7) of the forcing chain, where the period is 2^3, and supports the emergence of D = 3 spatial dimensions (T8). The certificate thereby closes the Lean verification of the harmonic-analysis component with zero sorries or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.