crCompositionCount
plain-language theorem explainer
The theorem asserts that the inductively defined cosmic ray composition type has exactly five elements. Astrophysicists using Recognition Science to model power-law spectra cite this to fix the five-component breakdown at configDim D = 5. The proof is a one-line decision procedure that enumerates the five constructors of the finite inductive type.
Claim. The finite set of cosmic ray composition categories has cardinality five, consisting of protons, helium, the CNO group, iron, and ultra-heavy nuclei.
background
The Cosmic Rays from Phi-Ladder module models cosmic ray energy spectra as power laws E^(-γ) with γ derived from the golden ratio. It introduces five canonical composition categories that the framework equates to configDim D = 5. The sibling inductive definition CRComposition enumerates exactly these five cases and derives Fintype, DecidableEq, and related structures to support cardinality calculations.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Because CRComposition is an inductive type with five explicit constructors and already derives Fintype, decide computes the cardinality directly as 5.
why it matters
This result populates the five_compositions field of the downstream cosmicRayCert definition, which certifies the overall cosmic ray model. It directly implements the module statement that five categories equal configDim D = 5 and aligns with the phi-ladder structure used for spectral indices in the Recognition Science forcing chain. No open questions remain at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.