abstractHarmonicAnalysisCert
plain-language theorem explainer
abstractHarmonicAnalysisCert assembles a certificate confirming five locally compact groups and the order-8 cyclic group size of exactly 8 in the Recognition Science harmonic analysis setup. Mathematicians formalizing abstract harmonic analysis from RS principles would cite this to anchor the DFT-8 construction on ℤ/8ℤ. The definition is a direct structure literal that invokes two decide lemmas for the cardinality facts.
Claim. Let LCGroup be the finite type of the five canonical locally compact groups. The certificate asserts that the cardinality of LCGroup equals 5 and that the size of the cyclic group of order 8 satisfies $z8Size = 2^3$.
background
The module develops abstract harmonic analysis from Recognition Science by identifying five canonical locally compact groups (ℝ, ℤ, S¹, ℚₚ, GL_n(ℚ)) whose count equals configuration dimension D = 5. It encodes the discrete Fourier transform on the cyclic group ℤ/8ℤ of order 8 = 2^3, consistent with the eight-tick octave. Pontryagin duality appears as the dual of ℤ being S¹.
proof idea
The definition is a one-line structure constructor that supplies the five_groups field from lcGroupCount and the z8_size field from z8Size_2cubed.
why it matters
This definition completes the Lean encoding of the abstract harmonic analysis certificate in the Recognition Science mathematics module. It anchors the five-group count and 2^3 size for the cyclic group, linking directly to the eight-tick octave (T7) and the derivation of three spatial dimensions (T8). The structure closes the module's formalization of harmonic analysis on these groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.