typical_grb_in_range
plain-language theorem explainer
Recognition Science assigns a typical GRB isotropic energy of 3.24e52 erg by accreting 0.1 solar masses at 10 percent efficiency. Astrophysicists checking consistency with observed GRB catalogs would cite the resulting bounds. The proof reduces the claim to numerical evaluation after unfolding the defining expressions.
Claim. $10^{51} < E_{typ} < 10^{54}$ erg, with $E_{typ} := 0.1$ times $0.1$ times $1.8$ times $10^{54}$.
background
The module defines solar_mass_energy as 1.8e54 erg, accretion_efficiency as 0.1, grb_energy(M_frac) as accretion_efficiency times M_frac times solar_mass_energy, and typical_grb_energy as grb_energy applied to 0.1. These sit inside the Recognition Science treatment of gamma-ray bursts, which employs the Distinction predicate to classify burst types. The upstream Distinction supplies the binary predicate detecting distinguishability on any carrier type.
proof idea
A term proof that first applies simp to unfold typical_grb_energy, grb_energy, accretion_efficiency and solar_mass_energy, then uses norm_num to confirm the inequality holds for the resulting real number.
why it matters
The bound is invoked by the downstream theorem grb_energy_range to witness an energy inside the observed GRB range. It fills a step in RS_Gamma_Ray_Bursts.tex showing that Recognition Science reproduces the 10^{51}--10^{54} erg interval for typical burst energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.