abstractHarmonicAnalysisCert
plain-language theorem explainer
The definition constructs a certificate for abstract harmonic analysis in Recognition Science by assembling the count of five locally compact groups and the size of the cyclic group of order eight. Researchers working on harmonic analysis derivations from the RS framework would reference this to confirm the dimensional consistency with the eight-tick octave. The proof is a direct construction using two decide-based theorems for the group cardinality and the power-of-two size.
Claim. Let $LCGroup$ be the type of locally compact groups in the framework. The certificate $AbstractHarmonicAnalysisCert$ is defined by setting its $five_groups$ field to the statement that the cardinality of $LCGroup$ equals 5 and its $z8_size$ field to the statement that the size of the cyclic group of order 8 equals $2^3$.
background
The module derives abstract harmonic analysis from Recognition Science by identifying five canonical locally compact groups (reals, integers, circle, p-adics, and GL_n over rationals) whose count equals the configuration dimension 5. The cyclic group of order 8 serves as the domain for DFT-8, with its size fixed at 8 = 2^3 by the eight-tick octave. Upstream results include the theorem lcGroupCount, which states Fintype.card LCGroup = 5 and is proved by decide, together with z8Size_2cubed stating z8Size = 2^3 and likewise proved by decide.
proof idea
The definition is a direct construction that populates the AbstractHarmonicAnalysisCert structure by assigning the five_groups field to lcGroupCount and the z8_size field to z8Size_2cubed. Both source theorems are one-line wrappers proved by the decide tactic, which evaluates the finite cardinalities at compile time.
why it matters
This certificate anchors the abstract harmonic analysis layer in the Recognition Science mathematics module, feeding into derivations that connect the five groups to the eight-tick octave (T7) and spatial dimension D = 3 (T8). It closes the Lean verification for DFT-8 on Z/8Z with zero sorries or axioms, aligning with the module's claim that |Z/8Z| = 8 = 2^3. No open scaffolding questions are touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.