typical_grb_in_range
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values of efficiency or solar mass energy from the phi-ladder.
- Does not incorporate beaming or cosmological corrections to the isotropic energy.
- Does not address the two-class distinction between long and short GRBs.
- Does not provide a distribution over the GRB population.
Lean usage
example : 1e51 < typical_grb_energy ∧ typical_grb_energy < 1e54 := typical_grb_in_rangeformal statement (Lean)
28theorem typical_grb_in_range :
29 1e51 < typical_grb_energy ∧ typical_grb_energy < 1e54 := by
proof body
Term-mode proof.
30 simp only [typical_grb_energy, grb_energy, accretion_efficiency, solar_mass_energy]
31 norm_num
32
33/-! ## Two-Class Distinction -/
34