/-- The Minkowski metric in one time and one space dimension, signature `(−, +)`:`η((t, x), (t, x)) = −t² + x²`. -/def eta : Matrix (Fin 2) (Fin 2) ℝ := !![-1, 0; 0, 1]
boost_preserves_etatheoremProved here from basic factspropext, Classical.choice, Quot.sound
boost_preserves_etaLean 4Proved here from basic factsFormally verified
/-- **Boosts are Lorentz transformations:** `Λᵀ η Λ = η`, i.e. every boost preserves the interval`−t² + x²`. Proof: multiply out; the entries reduce to `cosh² φ − sinh² φ = 1`. -/theorem boost_preserves_eta (φ : ℝ) : (boost φ).transpose * eta * boost φ = eta := by have h := Real.cosh_sq φ ext i j fin_cases i <;> fin_cases j <;> simp [boost, eta, Matrix.mul_apply, Fin.sum_univ_two] <;> nlinarith [h]
lorentz_factor_three_fifthstheoremProved here from basic factspropext, Classical.choice, Quot.sound
lorentz_factor_three_fifthsLean 4Proved here from basic factsFormally verified
/-- A traveller at `v = 3/5` of the speed of light has Lorentz factor`γ = 1/√(1 − 9/25) = 5/4`: every `5` years of Earth time are `4` years of proper time. -/theorem lorentz_factor_three_fifths : 1 / Real.sqrt (1 - (3 / 5 : ℝ) ^ 2) = 5 / 4 := by have h : (1 - (3 / 5 : ℝ) ^ 2) = (4 / 5) ^ 2 := by norm_num rw [h, Real.sqrt_sq (by norm_num)] norm_num
/-- The effective potential for timelike geodesics in the Schwarzschild metric of mass `M`, for aparticle with angular momentum per unit mass `L` (units `G = c = 1`):`V(r) = (1 − 2M/r)(1 + L²/r²)`. Radial motion obeys `ṙ² = E² − V(r)`. -/noncomputable def effectivePotential (M L r : ℝ) : ℝ := (1 - 2 * M / r) * (1 + L ^ 2 / r ^ 2)
effective_potential_derivtheoremProved here from basic factspropext, Classical.choice, Quot.sound
effective_potential_derivLean 4Proved here from basic factsFormally verified
/-- **Where circular orbits live.** For `r ≠ 0`,`V′(r) = 2 (M r² − L² r + 3 M L²) / r⁴`. Circular orbits sit at critical points of `V`, i.e. atthe roots of `M r² − L² r + 3 M L² = 0`. The term `3 M L²` has no Newtonian counterpart. -/theorem effective_potential_deriv (M L : ℝ) {r : ℝ} (hr : r ≠ 0) : HasDerivAt (effectivePotential M L) (2 * (M * r ^ 2 - L ^ 2 * r + 3 * M * L ^ 2) / r ^ 4) r := by have h1 : HasDerivAt (fun s => 1 - 2 * M / s) (2 * M / r ^ 2) r := by have := ((hasDerivAt_inv hr).const_mul (2 * M)).const_sub 1 convert this using 1 · funext s simp [div_eq_mul_inv] · field_simp have h2 : HasDerivAt (fun s => 1 + L ^ 2 / s ^ 2) (-2 * L ^ 2 / r ^ 3) r := by have hsq : HasDerivAt (fun s => s ^ 2) (2 * r) r := by simpa using hasDerivAt_pow 2 r have := ((hsq.inv (pow_ne_zero 2 hr)).const_mul (L ^ 2)).const_add 1 convert this using 1 · funext s simp [div_eq_mul_inv] · field_simp show HasDerivAt (fun s => (1 - 2 * M / s) * (1 + L ^ 2 / s ^ 2)) _ r convert h1.mul h2 using 1 field_simp ring
circular_orbit_boundtheoremProved here from basic factspropext, Classical.choice, Quot.sound
circular_orbit_boundLean 4Proved here from basic factsFormally verified
/-- **No circular orbits with too little angular momentum.** If `M > 0`, `r > 0` and`M r² − L² r + 3 M L² = 0` (a circular orbit of radius `r`), then `L² ≥ 12 M²`. Proof: completingthe square, `(2 M r − L²)² = L⁴ − 12 M² L²`, so `L² (L² − 12 M²) ≥ 0`, and `L ≠ 0` because`L = 0` would force `M r² = 0`. -/theorem circular_orbit_bound {M L r : ℝ} (hM : 0 < M) (hr : 0 < r) (hcirc : M * r ^ 2 - L ^ 2 * r + 3 * M * L ^ 2 = 0) : 12 * M ^ 2 ≤ L ^ 2 := by have hsq : (2 * M * r - L ^ 2) ^ 2 = L ^ 2 * (L ^ 2 - 12 * M ^ 2) := by have : (2 * M * r - L ^ 2) ^ 2 = 4 * M * (M * r ^ 2 - L ^ 2 * r) + L ^ 4 := by ring rw [this, show M * r ^ 2 - L ^ 2 * r = -(3 * M * L ^ 2) by linarith] ring have hL : 0 < L ^ 2 := by rcases (sq_nonneg L).lt_or_eq with h | h · exact h · exfalso rw [← h] at hcirc have : M * r ^ 2 = 0 := by linarith have : 0 < M * r ^ 2 := by positivity linarith have hprod : 0 ≤ L ^ 2 * (L ^ 2 - 12 * M ^ 2) := hsq ▸ sq_nonneg _ by_contra hlt have : L ^ 2 * (L ^ 2 - 12 * M ^ 2) < 0 := mul_neg_of_pos_of_neg hL (by linarith [not_le.mp hlt]) linarith
iscotheoremProved here from basic factspropext, Classical.choice, Quot.sound
iscoLean 4Proved here from basic factsFormally verified
/-- **The innermost stable circular orbit is at `r = 6M`.** At the critical angular momentum`L² = 12 M²` the two circular orbits (stable and unstable) merge, and the circular-orbitequation forces `r = 6M`, three times the Schwarzschild radius. Inside it there are no stablecircular orbits: matter in an accretion disc spirals in. -/theorem isco {M L r : ℝ} (hM : 0 < M) (hL : L ^ 2 = 12 * M ^ 2) (hcirc : M * r ^ 2 - L ^ 2 * r + 3 * M * L ^ 2 = 0) : r = 6 * M := by rw [hL] at hcirc have h : M * (r - 6 * M) ^ 2 = 0 := by nlinarith have h' : (r - 6 * M) ^ 2 = 0 := by rcases mul_eq_zero.mp h with h0 | h0 · linarith · exact h0 have := pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h' linarith
/-- **You cannot add your way past the speed of light.** Hint: from `abs_lt` get `-1 < u < 1`and `-1 < v < 1`; show `0 < 1 + u * v` by `nlinarith`, rewrite with `abs_div`, `abs_of_pos`,`div_lt_one` and `abs_lt`, and finish both inequalities with `nlinarith` (they are`(1 - u)(1 - v) > 0` and `(1 + u)(1 + v) > 0`). -/theorem velocity_addition {u v : ℝ} (hu : |u| < 1) (hv : |v| < 1) : |(u + v) / (1 + u * v)| < 1 := by sorry
Show the compiled solution
velocity_additionLean 4Proved here from basic factsFormally verified
/-- **Relativistic velocity addition stays below the speed of light.** If `|u| < 1` and `|v| < 1`then `|(u + v)/(1 + uv)| < 1`. (This is `tanh(φ + ψ)` for `u = tanh φ`, `v = tanh ψ`.) Proof:`1 + uv > 0`, and `(1 + uv) − (u + v) = (1 − u)(1 − v) > 0`,`(1 + uv) + (u + v) = (1 + u)(1 + v) > 0`. -/theorem velocity_addition {u v : ℝ} (hu : |u| < 1) (hv : |v| < 1) : |(u + v) / (1 + u * v)| < 1 := by obtain ⟨hu1, hu2⟩ := abs_lt.mp hu obtain ⟨hv1, hv2⟩ := abs_lt.mp hv have hpos : 0 < 1 + u * v := by nlinarith rw [abs_div, abs_of_pos hpos, div_lt_one hpos, abs_lt] constructor <;> nlinarith
/-- **The innermost stable circular orbit is at `6M`.** Hint: substitute `L² = 12 M²`; thecircular-orbit equation becomes `M (r − 6M)² = 0`. -/theorem isco {M L r : ℝ} (hM : 0 < M) (hL : L ^ 2 = 12 * M ^ 2) (hcirc : M * r ^ 2 - L ^ 2 * r + 3 * M * L ^ 2 = 0) : r = 6 * M := by sorry
Show the compiled solution
iscoLean 4Proved here from basic factsFormally verified
/-- **The innermost stable circular orbit is at `r = 6M`.** At the critical angular momentum`L² = 12 M²` the two circular orbits (stable and unstable) merge, and the circular-orbitequation forces `r = 6M`, three times the Schwarzschild radius. Inside it there are no stablecircular orbits: matter in an accretion disc spirals in. -/theorem isco {M L r : ℝ} (hM : 0 < M) (hL : L ^ 2 = 12 * M ^ 2) (hcirc : M * r ^ 2 - L ^ 2 * r + 3 * M * L ^ 2 = 0) : r = 6 * M := by rw [hL] at hcirc have h : M * (r - 6 * M) ^ 2 = 0 := by nlinarith have h' : (r - 6 * M) ^ 2 = 0 := by rcases mul_eq_zero.mp h with h0 | h0 · linarith · exact h0 have := pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h' linarith