LCGroup
LCGroup enumerates the five locally compact groups that realize configDim D = 5 for abstract harmonic analysis in Recognition Science. A researcher working on DFT-8 over the cyclic group of order 8 or on Pontryagin duality would cite this enumeration to fix the base set. The declaration is a direct inductive construction that automatically derives DecidableEq, Repr, BEq, and Fintype instances.
claimThe inductive type $LCGroup$ consists of five constructors corresponding to the real line $mathbb{R}$, the integers $mathbb{Z}$, the circle group $S^1$, the $p$-adic numbers $mathbb{Q}_p$, and the general linear group $GL_n(mathbb{Q})$.
background
The module AbstractHarmonicAnalysisFromRS sets out abstract harmonic analysis derived from Recognition Science. It identifies five canonical locally compact groups (ℝ, ℤ, S¹, ℚₚ, GL_n(ℚ)) with configDim D = 5. DFT-8 denotes harmonic analysis on ℤ/8ℤ, whose order equals 8 = 2^3, while Pontryagin duality pairs ℤ with S¹ as duals.
proof idea
The declaration is a direct inductive definition that lists the five groups and derives the required type-class instances via the deriving clause. No lemmas are applied; the construction is self-contained.
why it matters in Recognition Science
LCGroup supplies the finite set whose cardinality is asserted equal to 5 in AbstractHarmonicAnalysisCert and proved by lcGroupCount. It anchors the RS model of five groups for harmonic analysis and supplies the cyclic group of order 2^3 that realizes the eight-tick octave. The definition closes the enumeration step required before cardinality and duality statements can be stated.
scope and limits
- Does not assign a concrete value to n in GL_n(ℚ).
- Does not prove any group operations or duality statements.
- Does not reference the spatial dimension D = 3 from the forcing chain.
- Does not include the definition of z8Size or its relation to 2^3.
formal statement (Lean)
21inductive LCGroup where
22 | real | integer | circle | pAdic | generalLinear
23 deriving DecidableEq, Repr, BEq, Fintype
24