`propagation_equality_forced`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.PropagationSpeed
domain: Gravity
line: 51 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.PropagationSpeed on GitHub at line 51.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

Derivations using this theorem

Gravity Propagates at the Speed of Light · foundational / THEOREM
Both ride the same recognition substrate; the ratio is exactly 1

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.