stellar_imf_implies_uhecr
plain-language theorem explainer
Stellar initial mass function structure derived from the ledger directly entails the ultra-high-energy cosmic ray structural input. Astrophysicists linking stellar populations to cosmic ray origins within Recognition Science would cite this connection when chaining ledger-based derivations. The proof is a one-line term wrapper that returns the hypothesis unchanged because the two propositions coincide definitionally.
Claim. If the stellar initial mass function structure follows from the ledger, then the ultra-high-energy cosmic ray input from the ledger holds, i.e., $0 < phi$ where $phi$ is the self-similar fixed point.
background
In the Astrophysics.StellarIMFStructure module the stellar initial mass function is introduced through the definition stellar_imf_from_ledger, which is set equal to uhecr_from_ledger. The proposition uhecr_from_ledger, imported from UHECRStructure, asserts simply that phi is positive. This local setting sits inside the Recognition Science framework where phi arises as the fixed point of the self-similar forcing chain (T6) and supplies the yardstick for mass ladders and the alpha band.
proof idea
The proof is a term-mode one-liner that returns the hypothesis h unchanged. Because stellar_imf_from_ledger is definitionally identical to uhecr_from_ledger by the upstream definition, the implication holds without further reduction or tactic steps.
why it matters
The declaration supplies the direct bridge from stellar initial mass function structure to ultra-high-energy cosmic ray input inside the Recognition Science astrophysics layer. It completes the ledger-to-structure step indicated by the module doc comment and relies on the positivity of phi that underpins the eight-tick octave and D=3 spatial dimensions. No downstream uses are recorded and no open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.