grb_energy_range
plain-language theorem explainer
The theorem asserts existence of a real E satisfying 10^51 < E < 10^54 in erg, where E stands for the isotropic energy of a typical gamma-ray burst. Astrophysicists using Recognition Science to bound GRB energetics would cite the result when fixing the canonical scale. The proof is a direct term construction that supplies the typical energy value and the two sides of its range theorem.
Claim. There exists a real number $E$ such that $10^{51} < E < 10^{54}$, where $E$ denotes the isotropic energy of a typical gamma-ray burst in erg.
background
The GammaRayBursts module develops GRB phenomenology inside Recognition Science following the outline of RS_Gamma_Ray_Bursts.tex. It imports the J-cost core and spectral emergence primitives. The typical_grb_energy definition fixes the efficiency parameter at 0.1 inside the grb_energy function, which itself unfolds to solar_mass_energy scaled by accretion_efficiency. The companion theorem typical_grb_in_range establishes the numerical bounds by simp and norm_num after these unfoldings. The E definition from SpectralEmergence counts edges of the D-cube but is not invoked in the range statement itself.
proof idea
The proof is a term-mode construction that directly packages the typical_grb_energy definition with the left and right conjuncts of typical_grb_in_range. No further tactics or lemmas are applied.
why it matters
The result supplies the canonical isotropic energy window for GRBs inside the Recognition Science framework as stated in the accompanying paper. It anchors later module calculations of luminosities and Lorentz factors. No downstream uses are recorded, leaving open its integration with the phi-ladder or J-cost derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.