Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.FRBStructure

show as:
view Lean formalization →

Module packaging the Recognition Science structural account of Fast Radio Bursts and their link to ultra-high-energy cosmic rays. It defines FRB structure from the ledger, states the FRB structural predicate, and records that FRB structure supplies UHECR-side input. Downstream cosmic-magnetic-field work imports this bridge. Argument is definitional plus a short implication, not a long derivation.

claimThe module introduces FRB structure on the Recognition ledger and asserts that this structure yields the structural input required on the UHECR side: if a source satisfies the FRB structural predicate, then the corresponding UHECR structural hypotheses hold.

background

Fast Radio Bursts (FRBs) are millisecond radio transients whose energetics and repetition patterns sit awkwardly in standard astrophysics. In Recognition Science they are read as ledger events: discrete recognition ticks on the phi-ladder, constrained by the eight-tick octave and the same J-cost geometry that forces the rest of the framework.

The module sits in the Astrophysics layer and imports the UHECR structure module. Ultra-high-energy cosmic rays (UHECR) are the charged-particle counterpart; the shared claim is that FRB and UHECR channels are two faces of one ledger process rather than unrelated source classes.

Sibling names indicate three pieces: construction of FRB data from the ledger, the FRB structural predicate itself, and the implication that FRB structure feeds UHECR-side hypotheses.

proof idea

Definition-heavy module. FRB structure is introduced from ledger data; the main claim is the implication that FRB structure supplies UHECR structural input. That implication is a short bridge into the imported UHECRStructure module, not a multi-step analytic derivation. No deep tactic scripts are required beyond discharging the structural hypotheses.

why it matters in Recognition Science

Gives CosmicMagneticFieldsStructure a clean FRB-to-UHECR bridge so magnetic-field and propagation arguments can assume a single ledger origin for both channels. Aligns with the Recognition program of reading high-energy astrophysical transients as discrete recognition events on the phi-ladder (eight-tick octave, J-cost geometry) rather than as ad hoc source populations. Closes a structural gap between radio and charged-particle sides before field-strength and deflection estimates are layered on.

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)