cosmic_magnetic_fields_structure
plain-language theorem explainer
Cosmic magnetic fields are shown to follow from the ledger by direct substitution of the fast radio burst structure theorem. Astrophysicists modeling fast radio bursts and cosmic magnetism would cite this to connect field origins to the underlying ledger without extra postulates. The proof is a one-line term that applies frb_structure once the definition equates cosmic_magnetic_fields_from_ledger to frb_from_ledger.
Claim. The proposition that cosmic magnetic fields arise from the ledger holds, proved by the fast radio burst structure theorem which establishes the equivalent fast radio burst input from the ledger.
background
Recognition Science derives structures from a single ledger. In this module the definition cosmic_magnetic_fields_from_ledger is set equal to frb_from_ledger, the fast radio burst input drawn from the ledger. The upstream theorem frb_structure asserts that frb_from_ledger follows from uhecr_structure, the ultra-high-energy cosmic ray structure, and carries the comment that FRB structure implies UHECR-side structural input.
proof idea
The proof is a one-line term wrapper that applies the frb_structure theorem directly; the goal is discharged because cosmic_magnetic_fields_from_ledger is definitionally identical to frb_from_ledger.
why it matters
This result places cosmic magnetic field structure inside the Recognition Science chain by equating it to the FRB structure that descends from the UHECR structure. It supports the framework claim that astrophysical phenomena trace to the ledger via the forcing chain and phi-ladder without auxiliary assumptions. No downstream uses are recorded yet, but the declaration closes the structural implication inside the cosmic magnetic fields module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.