grb_energy
plain-language theorem explainer
grb_energy defines gamma-ray burst energy as the product of accretion efficiency 0.1, an input mass fraction, and the rest energy of one solar mass. Astrophysicists modeling GRB populations cite this expression when computing reference energies or positivity. The definition is a direct multiplication of the three fixed or supplied quantities.
Claim. $E(M_frac) := 0.1 · M_frac · 1.8 × 10^{54}$
background
The module develops gamma-ray burst models inside Recognition Science following the paper RS_Gamma_Ray_Bursts.tex. accretion_efficiency is the constant 0.1 representing the fraction of accreted mass converted to energy. solar_mass_energy is the rest-mass energy of one solar mass set to 1.8e54 in the working units. The present definition multiplies these with a variable mass fraction to obtain total burst energy.
proof idea
The definition body is the direct product accretion_efficiency * M_frac * solar_mass_energy.
why it matters
This definition supplies the energy expression referenced by grb_energy_positive (positivity for positive mass fraction), typical_grb_energy (reference value at 0.1), and typical_grb_in_range (bounds 1e51 to 1e54). It implements the core scaling relation for the gamma-ray burst analysis in the Recognition Science paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.