lorentz_factor
plain-language theorem explainer
The definition sets the Lorentz factor for a gamma-ray burst jet to the ratio of jet energy to baryon mass. Researchers modeling GRB jet dynamics in the Recognition Science framework cite it when establishing positivity of the boost. It is introduced as a direct noncomputable definition using real division.
Claim. The Lorentz factor is defined by the equation $E_{jet}/M_b$ for jet energy $E_{jet}$ and baryon mass $M_b$.
background
The module develops gamma-ray burst models from Recognition Science following the paper RS_Gamma_Ray_Bursts.tex. This definition supplies the basic kinematic ratio for jets without any imported lemmas. It precedes statements on positivity and energy ranges for long and short GRB classes.
proof idea
The definition is introduced directly as the quotient of the two real arguments. No lemmas or tactics are required.
why it matters
It supplies the expression used by the theorem lorentz_positive to prove positivity under positive energy and mass. The definition supports the GRB analysis in the Recognition Science paper and aligns with the framework's handling of physical quantities derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.