Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.CosmicMagneticFieldsStructure

show as:
view Lean formalization →

The module organizes results showing that cosmic magnetic field structures supply structural inputs to FRB models in Recognition Science. It imports the FRBStructure module and lists sibling declarations for ledger-derived fields and implications. Astrophysicists modeling fast radio bursts under RS constraints would cite the module. The module itself contains no proofs and functions as an import and declaration container.

claimCosmic magnetic field structure implies FRB-side structural input.

background

The module sits in the Astrophysics domain and imports only Mathlib plus IndisputableMonolith.Astrophysics.FRBStructure. FRBStructure supplies the base definitions for fast radio burst structural modeling. The local setting follows the Recognition Science forcing chain (T0-T8) and Recognition Composition Law, with constants fixed in RS-native units (c=1, ħ=ϕ^{-5}). Sibling declarations handle cosmic_magnetic_fields_from_ledger, cosmic_magnetic_fields_structure, and cosmic_magnetic_fields_implies_frb.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the implication from cosmic magnetic fields to FRB structural input, feeding downstream FRB results. It fills the astrophysics slot in the Recognition framework by linking magnetic structure to the phi-ladder and eight-tick octave. No used_by edges are recorded, indicating it acts as an intermediate bridge rather than a terminal theorem.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)