lcGroupCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish any group operations or duality properties on the enumerated groups.
- Does not connect the count to physical constants, mass formulas, or forcing chain steps.
- Does not prove the equality of eight to two cubed beyond the separate z8Size theorem.
- Does not address whether these five groups exhaust all locally compact abelian groups.
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. -/