cosmic_magnetic_fields_from_ledger
plain-language theorem explainer
This definition sets the proposition that cosmic magnetic fields derive from the ledger equal to the fast radio burst proposition from the ledger. Astrophysicists working in the Recognition Science ledger framework would cite it to chain magnetic field models to ultra-high-energy cosmic ray inputs. The construction is a direct one-line alias to the upstream FRB definition.
Claim. Define the proposition $C$ that cosmic magnetic fields arise from the ledger by the equality $C := F$, where $F$ is the proposition that fast radio bursts arise from the ledger.
background
The Astrophysics module models cosmic magnetic fields through structural propositions that trace back to ledger inputs. The upstream declaration frb_from_ledger is itself defined as equivalent to uhecr_from_ledger, linking fast radio bursts to ultra-high-energy cosmic ray propositions. This establishes a chain from particle acceleration mechanisms to magnetic field generation within the Recognition Science ledger foundation.
proof idea
One-line definition that directly aliases the upstream frb_from_ledger declaration.
why it matters
The definition supplies the hypothesis for cosmic_magnetic_fields_structure, which proves the ledger origin via frb_structure, and for cosmic_magnetic_fields_implies_frb, which uses the hypothesis to recover the FRB proposition. It places cosmic magnetic fields inside the ledger chain that runs from T0 forcing through T8 dimensional constraints, without introducing new open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.