theorem proved term proof

`speed_ratio_unity`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  46theorem speed_ratio_unity : c_grav_RS / c_RS = 1 := by

proof body

Term-mode proof.

  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. -/

depends on (5)

Lean names referenced from this declaration's body.

c_RS in IndisputableMonolith.Cosmology.EtaBPrefactorDerivation decl_use
c_RS in IndisputableMonolith.Gravity.BlackHoleEntropyFromLedger decl_use
c_grav_RS in IndisputableMonolith.Gravity.PropagationSpeed decl_use
c_RS in IndisputableMonolith.Gravity.PropagationSpeed decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use