lcGroupCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the five groups from the T0-T8 forcing chain.
- Does not prove Pontryagin duality or any Fourier-analytic properties.
- Does not address the order of ℤ/8ℤ or the z8Size theorem.
- Does not connect to mass formulas, Berry thresholds, or RS constants.
Lean usage
def abstractHarmonicAnalysisCert : AbstractHarmonicAnalysisCert where five_groups := lcGroupCount z8_size := z8Size_2cubedformal statement (Lean)
25theorem lcGroupCount : Fintype.card LCGroup = 5 := by decide
proof body
Term-mode proof.
26
27/-- ℤ/8ℤ has 8 elements = 2^3. -/