CosmicRayCert
CosmicRayCert bundles the assertion of exactly five cosmic ray composition categories with the spectral index lying in (2.61, 2.63). Astrophysicists checking Recognition Science against observed power-law spectra would cite this record when confirming the index near 2.618. The definition assembles the two facts directly from the five-element enumeration of composition types and the explicit formula for the index as one plus the golden ratio.
claimLet the cosmic ray compositions be the five categories protons, helium, CNO, iron and ultra-heavy nuclei. Let the spectral index be the real number given by one plus the golden ratio. Then CosmicRayCert is the structure asserting that the number of these categories equals five and that the spectral index satisfies $2.61 < $ spectral index $ < 2.63$.
background
The module develops cosmic ray predictions by linking the energy spectrum to the phi-ladder. The spectral index is defined directly as one plus the golden ratio, which places it in (2.61, 2.63). The composition categories are given by an inductive type with five constructors, each matching a standard group in cosmic ray observations, and equipped with a Fintype instance.
proof idea
The structure is a direct record definition. One field records the cardinality of the composition inductive type, which equals five by its Fintype derivation. The second field records the open interval membership for the spectral index value, which follows immediately from its definition as one plus the golden ratio. No lemmas or tactics are invoked.
why it matters in Recognition Science
This structure supplies the certificate instantiated by the downstream cosmicRayCert definition, which witnesses the Recognition Science claims for cosmic ray spectra. It packages the module's stated predictions that the index approximates one plus the golden ratio and that five composition classes exist, aligning with the phi-ladder framework. The knee-to-ankle energy ratio discrepancy remains open for further work.
scope and limits
- Does not derive the golden ratio or spectral index from the forcing chain.
- Does not model the knee at approximately 3 times 10 to the 15 eV.
- Does not simulate propagation losses or source distributions.
- Does not compare predictions against specific observatory data sets.
formal statement (Lean)
38structure CosmicRayCert where
39 five_compositions : Fintype.card CRComposition = 5
40 spectral_index_band : (2.61 : ℝ) < spectralIndex ∧ spectralIndex < 2.63
41