cosmicRayCert
plain-language theorem explainer
The cosmicRayCert definition assembles a certificate verifying that cosmic ray compositions number exactly five and that the spectral index falls in the interval (2.61, 2.63). Researchers working on high-energy astrophysics within the Recognition Science framework would cite this when validating the phi-ladder predictions against observed power-law spectra. The construction proceeds by direct record field assignment from the crCompositionCount theorem and the spectralIndexBand theorem.
Claim. Let CosmicRayCert be the structure requiring that the cardinality of cosmic ray composition types equals five and that the spectral index satisfies $2.61 < γ < 2.63$. The term cosmicRayCert is the instance of this structure obtained by combining the composition count theorem with the spectral index band theorem.
background
In the Cosmic Rays from Phi-Ladder module the Recognition Science framework predicts that the cosmic ray energy spectrum follows a power law with index approximately 1 + φ, where φ denotes the golden ratio. Five canonical composition categories (protons, helium, CNO group, iron, ultra-heavy) correspond to configuration dimension D = 5. The upstream theorem crCompositionCount establishes the cardinality equality by decision, while spectralIndexBand proves the narrow interval around 2.618 using bounds on φ.
proof idea
The definition is a direct record constructor that populates the five_compositions field with the result of crCompositionCount and the spectral_index_band field with the result of spectralIndexBand. No additional tactics are applied beyond the field assignments.
why it matters
This definition supplies the Lean witness for the cosmic ray spectral properties derived from the phi-ladder in the Recognition Science framework. It completes the B12 Astrophysics Depth by providing a certified instance that matches the predicted index 1 + φ and the five compositions. No downstream theorems currently depend on it, leaving open the question of integrating the knee and ankle energy scales into the main forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.