lorentz_positive
The theorem establishes positivity of the Lorentz factor, defined as the ratio of jet energy to baryonic mass, whenever both quantities are positive reals. Modelers of gamma-ray burst outflows in Recognition Science cite it to guarantee the factor stays physically admissible in energy calculations. The proof is a direct one-line application of the division-positivity lemma from Mathlib.
claimLet $E>0$ and $M>0$ be real numbers. Then the Lorentz factor defined by $E/M$ satisfies $E/M>0$.
background
The module develops gamma-ray burst energetics inside Recognition Science, following the paper RS_Gamma_Ray_Bursts.tex. The upstream definition supplies the Lorentz factor as the ratio of jet energy to baryonic mass for real inputs. This ratio appears in the module's treatment of relativistic outflows and energy positivity statements.
proof idea
The proof is a one-line term that applies the Mathlib lemma div_pos directly to the two positivity hypotheses.
why it matters in Recognition Science
The result secures positivity of the Lorentz factor inside the Recognition Science treatment of gamma-ray bursts. It supports downstream claims on GRB energy ranges and classes within the same module. No open scaffolding is closed here; the step simply enforces a basic physical sign condition required by the framework's relativistic modeling.
scope and limits
- Does not compute a numerical value for the Lorentz factor.
- Does not incorporate frame transformations or relativistic beaming.
- Does not treat cases in which jet energy or baryonic mass is zero or negative.
formal statement (Lean)
46theorem lorentz_positive (E_jet M_b : ℝ) (hE : 0 < E_jet) (hM : 0 < M_b) :
47 0 < lorentz_factor E_jet M_b := div_pos hE hM
proof body
Term-mode proof.
48
49/-! ## Amati Relation -/
50