pith. sign in
module module high

IndisputableMonolith.Physics.GammaRayBursts

show as:
view Lean formalization →

GammaRayBursts module derives the Amati exponent of exactly 1/2 for the E_peak-E_iso correlation by multiplying the imported Lorentz factor scaling Γ ∝ E_iso^{1/4} by an extra √E_iso factor. Astrophysicists testing high-energy transient models cite the result for its parameter-free match to observations. The module assembles the relation through direct algebraic substitution of scalings supplied by the JcostCore import.

claim$E_{peak} ∝ E_{iso}^{1/2}$ obtained from the product Γ ∝ E_iso^{1/4} × √E_iso.

background

The module imports Mathlib and JcostCore, the latter supplying the J-cost function J(x) = (x + x^{-1})/2 - 1 together with its associated scaling laws for energy and Lorentz factors. It defines concrete GRB quantities including solar_mass_energy, accretion_efficiency, grb_energy, and lorentz_factor, then states positivity, range, and disjointness lemmas for long and short classes. The theoretical setting is the Recognition Science application of the single functional equation to astrophysical transients, with all constants fixed in RS-native units where c = 1.

proof idea

This is a definition module containing supporting lemmas. The central Amati exponent follows from one-line algebraic combination of the Γ scaling imported from JcostCore with the additional square-root energy factor stated in the module doc-comment.

why it matters in Recognition Science

The module supplies the gamma-ray burst sector of Recognition Science predictions and directly encodes the Amati exponent 1/2 stated in its doc-comment. It converts the abstract J-cost and phi-ladder machinery into concrete observables (energies, Lorentz factors, peak relations) that can be compared with telescope data. No downstream theorems are listed yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)