amati_increases
plain-language theorem explainer
The theorem establishes strict monotonicity of the Amati peak with respect to isotropic energy under positive prefactor C. Astrophysicists fitting gamma-ray burst spectra within Recognition Science would cite this ordering to maintain consistent energy hierarchies. The term proof unfolds the peak definition then applies the positive-multiplier inequality together with the real-power monotonicity lemma.
Claim. Let real numbers $E_1$, $E_2$, $C$ satisfy $E_1 > 0$, $C > 0$, and $E_1 < E_2$. Then $C E_1^{1/2} < C E_2^{1/2}$.
background
The Gamma-Ray Bursts module derives burst observables from Recognition Science axioms as described in the paper RS_Gamma_Ray_Bursts.tex. The function amati_peak is defined by the product of a positive constant C and the isotropic energy raised to the power one-half, encoding the exponent that arises from the Lorentz-factor scaling combined with the square-root energy term. The upstream theorem from PrimitiveDistinction converts seven independent axioms into four structural conditions plus three definitional facts that underwrite the present ordering statement.
proof idea
The term proof first unfolds the definition of amati_peak to obtain the product form. It then applies the lemma mul_lt_mul_of_pos_left instantiated with the positivity hypothesis on C, which reduces the goal to the strict increase of the real-power map. The final step invokes Real.rpow_lt_rpow on the given inequalities together with a norm_num tactic that confirms the exponent 1/2.
why it matters
This monotonicity closes a basic consistency requirement for the Amati relation inside the Recognition Science treatment of gamma-ray bursts. It guarantees that larger isotropic energies produce strictly larger peak values under the derived exponent 1/2, supporting spectral modeling steps in the associated paper. No downstream theorems are recorded, yet the result supplies an elementary ordering fact needed before more elaborate burst-classification lemmas can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.