spectralIndexBand
plain-language theorem explainer
The Recognition Science model predicts the cosmic ray spectral index lies strictly between 2.61 and 2.63. Astrophysicists modeling power-law spectra near the knee would cite this bound to match the phi-ladder prediction against measured indices around 2.7. The proof reduces the claim to the definition of the index as one plus phi and invokes linear arithmetic on the established phi bounds.
Claim. $2.61 < 1 + φ < 2.63$, where $φ$ is the golden ratio.
background
In the Cosmic Rays from Phi-Ladder module the spectral index is defined as one plus the golden ratio phi. This implements the RS claim that the cosmic ray energy spectrum follows a power law with index approximately 2 + 1/φ, which equals 1 + φ ≈ 2.618. The module places the result in the setting of observed knee and ankle features together with five canonical composition categories that match configDim D = 5.
proof idea
The proof first unfolds the definition of spectralIndex to obtain the expression 1 + phi. It then applies the exact tactic with two linarith calls, one using the lemma phi_gt_onePointSixOne for the lower bound and one using phi_lt_onePointSixTwo for the upper bound.
why it matters
This theorem supplies the spectral_index_band field required by the cosmicRayCert definition, which certifies the five cosmic ray compositions and the index band. It directly implements the RS prediction γ ≈ 1 + φ from the module documentation, consistent with measured values around 2.7. The result closes a small link in the phi-ladder application to astrophysics, building on the phi bounds from Constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.