pith. sign in
module module moderate

IndisputableMonolith.Physics.GammaRayBursts

show as:
view Lean formalization →

The GammaRayBursts module derives the Amati exponent of 1/2 for gamma-ray bursts from the combination of Lorentz factor scaling with isotropic energy in the Recognition Science framework. Astrophysicists working on high-energy transients would cite it when testing J-cost predictions against observed E_peak-E_iso correlations. The module supplies definitions for energies, efficiencies, and Lorentz factors together with supporting positivity and range theorems, all built directly on the JcostCore import.

claim$E_ {peak} ∝ E_{iso}^{1/2}$ follows from the scaling $Γ ∝ E_{iso}^{1/4} √E_{iso}$ under the J-cost composition law in RS-native units.

background

The module imports JcostCore, which supplies the J-cost function J(x) = (x + x^{-1})/2 - 1 and the Recognition Composition Law. It introduces GRB-specific quantities expressed on the phi-ladder: solar mass energy, accretion efficiency, GRB energy, Lorentz factor, and related positivity statements. The local setting is the T5-T8 forcing chain with c = 1 and ħ = φ^{-5}.

proof idea

This is a definition module, no proofs. It assembles direct definitions for the listed GRB parameters and records elementary positivity and range facts by reduction to JcostCore primitives.

why it matters in Recognition Science

The module supplies the gamma-ray burst sector of Recognition Science physics and records the Amati exponent 1/2 derivation stated in its documentation. It applies the J-uniqueness and phi-ladder mass formulas to an astrophysical observable but currently shows no downstream uses in the dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)