Pith. sign in
module module moderate

IndisputableMonolith.Physics.GammaRayBursts

show as:
view Lean formalization →

The GammaRayBursts module supplies definitions and lemmas for gamma-ray burst energies and the Amati relation in Recognition Science. Researchers in high-energy astrophysics cite it for the derived exponent of 1/2 in the Amati correlation. The structure relies on J-cost from the imported core module to express energies and Lorentz factors. Sibling declarations cover energy scales, efficiencies, and range constraints.

claim$E_{\rm peak} \propto E_{\rm iso}^{1/2}$ arising from $\Gamma \propto E_{\rm iso}^{1/4} \times \sqrt{E_{\rm iso}}$ in the Recognition Science J-cost framework.

background

The module resides in the Physics domain and imports JcostCore, which supplies the J-cost function satisfying the Recognition Composition Law. It introduces GRB-specific objects including solar_mass_energy as the reference energy scale, accretion_efficiency, grb_energy as the isotropic release, and lorentz_factor with its positivity and range lemmas. The theoretical setting extends the forcing chain T0-T8 to high-energy transients via J-cost expressions for energies and efficiencies.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module contributes the GRB energy and Amati relation results to the Recognition Science framework. It realizes the Amati exponent 1/2 as described in the module documentation. It stands ready for use in larger models of cosmic transients but has no downstream dependencies recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)