LCGroup
The inductive enumeration of five canonical locally compact groups supplies the type for abstract harmonic analysis in Recognition Science. Researchers working on DFT-8 over the cyclic group of order eight or Pontryagin duality would cite this enumeration. The definition lists the reals, integers, circle, p-adics, and general linear group over the rationals, then derives decidable equality and finiteness instances automatically.
claimLet $G$ be the inductive type with 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})$, equipped with decidable equality and finiteness.
background
The module sets up abstract harmonic analysis from Recognition Science by enumerating five canonical locally compact groups that realize configuration dimension five. These groups are the real numbers, integers, circle, p-adics, and general linear group over the rationals. The construction connects to the eight-tick octave through the fact that the cyclic group of order eight has eight elements equal to two cubed, and invokes Pontryagin duality with the dual of the integers identified with the circle. The definition imports Mathlib solely to obtain the derived instances.
proof idea
The declaration is a direct inductive definition that lists the five constructors explicitly. Lean's deriving clause then generates the DecidableEq, Repr, BEq, and Fintype instances with no further steps or lemmas required.
why it matters in Recognition Science
This enumeration feeds the AbstractHarmonicAnalysisCert structure, which records that the cardinality of the group type equals five and that the cyclic group of order eight has size two cubed. It realizes the module claim of five groups for configuration dimension five and supports the zero-sorry certification. The definition thereby anchors the link to the eight-tick octave (period two cubed) inside the Recognition framework.
scope and limits
- Does not claim these five groups exhaust all locally compact groups.
- Does not derive any Fourier analysis identities or dualities.
- Does not fix the integer n appearing in the general linear group.
- Does not connect to the spatial dimension three from the forcing chain.
- Does not prove the Pontryagin duality correspondence.
formal statement (Lean)
21inductive LCGroup where
22 | real | integer | circle | pAdic | generalLinear
23 deriving DecidableEq, Repr, BEq, Fintype
24