z8Size_2cubed
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the group order from the Recognition Science functional equation.
- Does not address Pontryagin duality beyond the order statement.
- Does not compute the discrete Fourier transform on the group.
- Does not generalize the result to other cyclic orders.
Lean usage
def abstractHarmonicAnalysisCert : AbstractHarmonicAnalysisCert where five_groups := lcGroupCount z8_size := z8Size_2cubedformal statement (Lean)
29theorem z8Size_2cubed : z8Size = 2 ^ 3 := by decide
proof body
30