uhecr_structure
plain-language theorem explainer
UHECR structure follows from positivity of phi in the Recognition ledger. Astrophysicists deriving cosmic-ray flux bounds from the phi-ladder would cite this when linking ultra-high-energy events to the foundational J-cost minimum. The proof is a one-line wrapper that applies the phi_pos lemma to discharge the uhecr_from_ledger proposition.
Claim. The structure of ultra-high-energy cosmic rays entails the positivity of the golden ratio, i.e., $0 < phi$.
background
In the UHECRStructure module, uhecr_from_ledger is the proposition $0 < phi$. This sits inside the Recognition Science derivation in which physical quantities occupy discrete phi-tiers, with nuclear density scaling as phi to an integer power times the Planck density. Upstream structures supply the ledger factorization of positive reals under multiplication, the convex J-cost function whose unique minimum is at unity, and the spectral emergence that forces SU(3) x SU(2) x U(1) gauge content together with three generations.
proof idea
The proof is a one-line wrapper that applies the phi_pos lemma to establish uhecr_from_ledger.
why it matters
This theorem supplies the UHECR-side structural input required by the FRB structure and stellar IMF structure theorems. It closes the positivity of phi in the astrophysical sector, consistent with T5 J-uniqueness and the eight-tick octave of the forcing chain. It touches the open question of matching observed UHECR cutoffs to specific rungs on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.