theorem
proved
propagation_implies_equal_speed
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.PropagationSpeed on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
38theorem c_grav_eq_c_RS : c_grav_RS = c_RS := rfl
39
40/-- Propagation-speed structural marker implies gravity/light equality in RS units. -/
41theorem propagation_implies_equal_speed (h : c_grav_RS = c_RS) :
42 c_grav_RS = c_RS :=
43 h
44
45/-- When both speeds are defined from the same tick rate, their ratio is 1. -/
46theorem speed_ratio_unity : c_grav_RS / c_RS = 1 := by
47 simp only [c_grav_RS, c_RS, div_one]
48
49/-- No separate gravitational "medium" with different propagation:
50 when c_grav = c_light and c_light ≠ 0, the ratio c_grav / c_light = 1. -/
51theorem propagation_equality_forced (c_light c_grav : ℝ) (heq : c_light = c_grav)
52 (hneq : c_light ≠ 0) : c_grav / c_light = 1 := by
53 rw [heq]; exact div_self (ne_of_eq_of_ne heq.symm hneq)
54
55end PropagationSpeed
56end Gravity
57end IndisputableMonolith