gamma_ge_one
plain-language theorem explainer
The Lorentz factor γ = c / √(c² - v²) satisfies γ ≥ 1 for any real speed v below light speed c. Recognition Science researchers deriving special relativity from the J-cost function cite this to confirm non-negative time dilation. The proof reduces the claim to a non-negative square root via le_div_iff rewriting, the one_mul lemma, and Real.le_sqrt.mpr with nlinarith.
Claim. For real numbers $v$ and $c$ with $0 < c$ and $|v| < c$, the Lorentz factor satisfies $1 ≤ c / √(c² - v²)$.
background
The module derives special relativity from the recognition framework: c is the canonical propagation speed, Lorentz transformations are symmetries of the J-cost function, and the invariant interval is the recognition metric. The Lorentz factor is identified with γ = cosh(θ) where θ = atanh(v/c), so that J(γ) = γ - 1 ≥ 0. The cost function appears as Jcost of a RecognitionEvent in ObserverForcing and as derivedCost of a MultiplicativeRecognizer in MultiplicativeRecognizerL4.
proof idea
The term proof first rewrites the inequality with le_div_iff using positivity of the square root, then applies the one_mul lemma from ArithmeticFromLogic to reduce the left side to 1. It finishes by invoking Real.le_sqrt.mpr, positivity, and nlinarith on the squared form using abs_lt.mp hv and sq_abs v.
why it matters
This anchors the structural derivation of special relativity by confirming the basic non-negativity of γ that follows from J-cost ≥ 0. It supports later results in the module such as time_dilation_structural and mass_energy_phi_rung. In the forcing chain it aligns with T5 J-uniqueness, where J(x) = cosh(log x) - 1, and with the interpretation of γ as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.