uhecr_from_ledger
plain-language theorem explainer
The declaration defines the UHECR ledger condition as the proposition that phi exceeds zero. Astrophysicists modeling ultra-high-energy cosmic rays in ledger-based frameworks cite it to establish the shared positivity prerequisite across related structures. It is a direct abbreviation of the inequality 0 < phi.
Claim. The ultra-high-energy cosmic ray ledger condition is the assertion that $0 < phi$.
background
In Recognition Science, phi is the self-similar fixed point forced at step T6 of the unified forcing chain. The module Astrophysics.UHECRStructure supplies this definition as a structural interface after importing Constants and Mathlib. Downstream modules copy the same proposition to link FRB and stellar IMF models to the same ledger input.
proof idea
This is a one-line definition that directly equates uhecr_from_ledger to the proposition 0 < phi.
why it matters
It supplies the base proposition for frb_from_ledger, stellar_imf_from_ledger, and uhecr_structure, the last of which discharges the claim via phi_pos. The definition ensures positivity of phi, a direct requirement from T6 of the forcing chain and the eight-tick octave. It closes the astrophysics interface without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.