grb_energy_positive
plain-language theorem explainer
The theorem shows that gamma-ray burst energy remains strictly positive for any positive accreted mass fraction. Modelers working with Recognition Science GRB energetics cite it to confirm that the energy formula stays physically admissible. The proof is a one-line wrapper that unfolds the three defining expressions and invokes the positivity tactic on the resulting product of positive terms.
Claim. If $M > 0$, then $0 < E(M)$, where $E(M) = 0.1 · M · 1.8×10^{54}$ is the gamma-ray burst energy expressed in native units.
background
The module develops gamma-ray burst properties from Recognition Science as described in RS_Gamma_Ray_Bursts.tex. Three noncomputable definitions supply the content: solar_mass_energy equals 1.8e54, accretion_efficiency equals 0.1, and grb_energy(M) is their product with the mass fraction M. These sit inside the J-cost framework imported from Cost.JcostCore and inherit the positivity properties already established for the Recognition Composition Law.
proof idea
The proof unfolds grb_energy, accretion_efficiency, and solar_mass_energy to obtain the explicit product 0.1 · M_frac · 1.8e54. It then applies the positivity tactic, which succeeds directly because the hypothesis 0 < M_frac and the two constant definitions are all positive.
why it matters
The result secures the elementary positivity requirement for GRB energies inside the Recognition Science model. It supplies a basic consistency check that later module declarations such as typical_grb_energy and lorentz_factor rely upon when they compute observable quantities. The declaration therefore fills an early step in the RS_Gamma_Ray_Bursts.tex development by confirming that the energy expression never produces unphysical negative values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.