crCompositionCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the spectral index value from the phi-ladder.
- Does not predict knee or ankle energies.
- Does not assign physical abundances or fluxes to each category.
- Does not relate composition count to spatial dimension D = 3.
Lean usage
noncomputable def cosmicRayCert : CosmicRayCert where five_compositions := crCompositionCount spectral_index_band := spectralIndexBandformal statement (Lean)
28theorem crCompositionCount : Fintype.card CRComposition = 5 := by decide
proof body
Term-mode proof.
29
30/-- Spectral index γ = 1 + φ ∈ (2.61, 2.63). -/