z8Size
z8Size defines the natural number 8 as the order of the cyclic group ℤ/8ℤ. Analysts studying discrete Fourier transforms on cyclic groups or the eight-tick structure in Recognition Science would cite this constant when certifying harmonic analysis. The definition is a direct literal assignment, with the relation to 2 cubed established separately by a decision procedure.
claimThe cardinality of the cyclic group $ℤ/8ℤ$ is defined to be 8.
background
The module Abstract Harmonic Analysis from RS identifies five canonical locally compact groups (ℝ, ℤ, S¹, ℚ_p, GL_n(ℚ)) with configuration dimension D = 5. It treats DFT-8 as harmonic analysis on the cyclic group ℤ/8ℤ whose order is 8, equivalently 2 cubed, and notes Pontryagin duality relating the dual of ℤ to the circle group S¹. The Lean code confirms the group order by decision with zero sorries or axioms.
proof idea
This is a direct definition that assigns the literal constant 8 to z8Size. No lemmas are applied and no tactics are used.
why it matters in Recognition Science
z8Size supplies the group order required by the AbstractHarmonicAnalysisCert structure to assert equality with 2 cubed. It anchors the connection to the eight-tick octave (period 2^3) at forcing-chain step T7 and supports derivation of three spatial dimensions at T8. The module uses the definition to ground harmonic analysis in the RS framework.
scope and limits
- Does not prove that z8Size equals 2 cubed.
- Does not define or axiomatize the group ℤ/8ℤ.
- Does not count the five locally compact groups.
- Does not implement the full harmonic analysis certification.
Lean usage
example : z8Size = 8 := rflformal statement (Lean)
28def z8Size : ℕ := 8