frb_from_ledger
plain-language theorem explainer
This definition equates the fast-radio-burst structural input to the ultra-high-energy-cosmic-ray ledger condition. Astrophysicists chaining Recognition Science assumptions across burst and cosmic-ray phenomena would cite it to maintain consistent ledger grounding. The construction is a direct alias to the upstream proposition 0 < phi.
Claim. The fast-radio-burst structural proposition is defined to coincide with the ultra-high-energy-cosmic-ray structural proposition, which asserts that the self-similar fixed point satisfies $0 < phi$.
background
Recognition Science encodes astrophysical structural inputs as propositions derived from the single ledger condition on the golden-ratio fixed point phi. The upstream definition uhecr_from_ledger states this ledger holds exactly when 0 < phi. The FRBStructure module imports UHECRStructure to allow direct reuse of that ledger proposition for fast-radio-burst modeling.
proof idea
One-line wrapper that aliases the upstream definition uhecr_from_ledger.
why it matters
The definition supplies the FRB-side ledger input required by cosmic_magnetic_fields_from_ledger and by the implication theorems frb_implies_uhecr and cosmic_magnetic_fields_implies_frb. It therefore sits inside the chain that grounds astrophysical structures in the T0-T8 forcing sequence and the phi-ladder. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.