amati_peak
plain-language theorem explainer
amati_peak encodes the Amati scaling for gamma-ray burst peak energy as proportional to the square root of isotropic energy. Astrophysicists working on GRB correlations cite this when deriving how observed peak energy grows with total burst output. The declaration is a direct algebraic definition with no lemmas or tactics required.
Claim. The Amati peak energy satisfies $E_0 = C E^{1/2}$ for isotropic energy $E$ and positive scaling factor $C$.
background
The module develops gamma-ray burst phenomenology inside Recognition Science, following the paper RS_Gamma_Ray_Bursts.tex. It imports JcostCore to connect burst energetics to the underlying J-cost and forcing-chain machinery, although this particular definition does not invoke any sibling or upstream declarations. All quantities are real numbers; no physical units or phi-ladder rungs are inserted at this stage.
proof idea
The declaration is a noncomputable definition that directly transcribes the algebraic expression $C * E_iso ^ (0.5 : ℝ)$ with no proof body, no tactics, and no referenced lemmas.
why it matters
The definition supplies the exact functional form required by the downstream theorem amati_increases, which proves strict monotonicity under positive inputs. It therefore anchors the Recognition Science account of GRB scaling relations that ultimately trace back to the J-uniqueness and phi-ladder steps of the unified forcing chain. No open scaffolding or hypothesis interface is closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.