lcGroupCount
plain-language theorem explainer
The theorem establishes that the inductive type LCGroup enumerating five canonical locally compact groups has cardinality exactly 5. Researchers formalizing abstract harmonic analysis in Recognition Science cite this to fix the configuration dimension at D = 5. The proof is a one-line decision procedure that evaluates the derived Fintype instance on the five constructors.
Claim. Let $LCGroup$ be the inductive type whose constructors are the real line, the integers, the circle group, the $p$-adic numbers, and the general linear group over the rationals. Then the cardinality of $LCGroup$ equals 5.
background
The module sets up abstract harmonic analysis from Recognition Science by enumerating five canonical locally compact groups whose count equals configDim D = 5. LCGroup is the inductive type with constructors real, integer, circle, pAdic, generalLinear, each deriving DecidableEq, Repr, BEq and Fintype. The surrounding text notes that DFT-8 performs harmonic analysis on ℤ/8ℤ of order 8 = 2^3 and recalls Pontryagin duality identifying the dual of ℤ with S¹.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the goal Fintype.card LCGroup = 5. The tactic succeeds directly from the Fintype derivation on the five-constructor inductive type.
why it matters
The result supplies the five_groups field of AbstractHarmonicAnalysisCert, which pairs it with the size of ℤ/8ℤ equal to 2^3. It anchors the mathematical layer of abstract harmonic analysis in the Recognition framework, aligning with the eight-tick octave (T7) and the group count matching configDim D = 5. No open scaffolding remains in the supplied dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.