amati_increases
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not prove the physical validity or origin of the Amati exponent.
- Does not apply when the prefactor C is non-positive.
- Does not extend the ordering to other functional forms or exponents.
- Does not address observational uncertainties in measured energies.
formal statement (Lean)
53theorem amati_increases (E₁ E₂ C : ℝ) (hE₁ : 0 < E₁) (hC : 0 < C) (h : E₁ < E₂) :
54 amati_peak E₁ C < amati_peak E₂ C := by
proof body
Term-mode proof.
55 unfold amati_peak
56 apply mul_lt_mul_of_pos_left _ hC
57 exact Real.rpow_lt_rpow (le_of_lt hE₁) h (by norm_num)
58
59/-- Amati exponent 1/2 from Γ ∝ E_iso^(1/4) × √(E_iso) combination. -/