lcGroupCount
plain-language theorem explainer
The theorem establishes that the inductive type enumerating five canonical locally compact groups has finite cardinality exactly five. Researchers certifying abstract harmonic analysis setups in Recognition Science would cite this count when fixing the configuration dimension at five. The proof is a one-line decision procedure that evaluates the derived Fintype instance on the enumerated constructors.
Claim. The finite cardinality of the type enumerating the five canonical locally compact groups (reals, integers, circle, p-adics, general linear) equals five: $ |LCGroup| = 5 $.
background
The module Abstract Harmonic Analysis from RS identifies five canonical locally compact groups whose count equals the configuration dimension D = 5. These groups are listed by the inductive type LCGroup with constructors real, integer, circle, pAdic, and generalLinear; the type derives DecidableEq, Repr, BEq, and Fintype to support cardinality computation. The local setting ties this enumeration to discrete Fourier transform on the cyclic group of order eight, which equals 2^3, and invokes Pontryagin duality relating the dual of the integers to the circle group.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality of the finite type LCGroup directly from its derived Fintype instance.
why it matters
This theorem supplies the five_groups field inside the abstractHarmonicAnalysisCert definition, which certifies the overall harmonic analysis construction together with the separate z8 size result. It fills the explicit count of five groups matching configDim D = 5 and the DFT-8 link to the eight-tick octave of period 2^3 in the Recognition Science framework. The parent structure is the certification of abstract harmonic analysis properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.