pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.FRBStructure

show as:
view Lean formalization →

This module organizes the structural link from Fast Radio Burst observations to Ultra-High-Energy Cosmic Ray inputs in the Recognition Science framework. Astrophysicists working on cosmic ray propagation or magnetic field modeling cite it to import FRB-derived constraints into UHECR analyses. The module consists of sibling definitions and an implication statement that directly supplies input to the downstream CosmicMagneticFieldsStructure module.

claimFRB structure $\implies$ UHECR structural input, via definitions frb_from_ledger, frb_structure, and the implication frb_implies_uhecr.

background

The module resides in the astrophysics domain and imports UHECRStructure to extend ledger-based structural inputs. It introduces frb_from_ledger (mapping ledger data to FRB properties), frb_structure (core FRB definition), and frb_implies_uhecr (the implication theorem). The local setting follows the Recognition Science forcing chain and Recognition Composition Law, treating FRB data as an additional structural constraint on the phi-ladder mass and defect distributions already present in UHECRStructure.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the FRB-to-UHECR implication required by the downstream CosmicMagneticFieldsStructure module. It completes the astrophysics pipeline step that converts FRB observations into UHECR-side structural input, consistent with the eight-tick octave and D=3 spatial dimensions of the foundation.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)