CRComposition
CRComposition enumerates the five canonical cosmic ray species in Recognition Science spectrum models. Astrophysicists verifying phi-ladder predictions for the knee and ankle would cite this enumeration to confirm the composition count equals configDim D = 5. The declaration is an inductive type whose Fintype instance follows directly from the five constructors and the deriving clause.
claimThe set of cosmic ray composition categories consists of five elements: protons, helium nuclei, the CNO group, iron nuclei, and ultra-heavy nuclei.
background
The module models the cosmic ray energy spectrum as a power law E^{-γ} with observed index near 2.7-3.0 and breaks at the knee (~3×10^{15} eV) and ankle (~3×10^{18} eV). Recognition Science predicts these breaks occur at phi-rung energies and that the spectral index satisfies γ ≈ 1 + φ ≈ 2.618, lying inside the interval (2.61, 2.63). Five composition categories are introduced to match the configuration dimension D = 5.
proof idea
The declaration is an inductive definition with five constructors. The deriving clause supplies the DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters in Recognition Science
This definition supplies the finite type required by CosmicRayCert, which asserts that the cardinality equals five and that the spectral index lies in (2.61, 2.63). It implements the module claim that the five categories realize configDim D = 5, closing the interface for downstream certification theorems on the phi-ladder cosmic ray spectrum.
scope and limits
- Does not assign energies or masses to individual composition types.
- Does not derive the spectral index from the Recognition Composition Law.
- Does not model propagation effects or interaction cross sections.
- Does not locate the knee or ankle energies inside the type.
formal statement (Lean)
24inductive CRComposition where
25 | protons | helium | CNO | iron | ultraHeavy
26 deriving DecidableEq, Repr, BEq, Fintype
27