Encyclopedia Gravity Gravity Propagation Speed C Rs
ARTICLE 4 claims 2 theorems 2 models
Gravity Propagation Speed C Rs
In the Recognition Science framework, gravity and light travel at the same speed because both move on the same underlying ledger of events.
The speed declaration
In physics, the speed of light in a vacuum, c, is a fixed number: about 299,792,458 meters per second. General relativity predicts that gravitational waves also travel at this speed, and the 2017 detection GW170817 confirmed the agreement to within about one part in 1015. The Recognition Science (RS) framework makes the same claim for a structural reason.
The framework models reality as a ledger, a discrete record of recognition events, where each event advances by one tick. In these natural units, the speed of light is defined as one ledger cell per tick, written c_RS = 1. The declaration c_grav_RS = 1 sets the gravitational signal speed to the same value. The machine-checked theorem c_grav_eq_c_RS proves the equality by definition: both speeds are literally the same real number 1, so their ratio is 1.
The reason is that RS posits no separate gravitational medium with its own tick rate. Light and gravity both propagate on the same ledger substrate, so they share the same speed limit. This is a structural identity, not an empirical fit. The framework's library of formal theorems contains this result as a proved statement, audited to the standard axioms of its type theory.
What the declaration does not do is derive the numerical value of c in SI units, nor does it prove that physical gravitational waves in our universe travel at exactly c. The equality c_grav = c is a definitional consequence within the framework's model, not a measurement. The GW170817 observation is cited as empirical confirmation, not as part of the proof. The framework also does not claim that gravity propagates faster or slower than light in any regime; it asserts exact equality in its native units.
MODEL c_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- In RS-native units: speed of light c = 1 (ledger cells per tick). -/
def c_RS : ℝ := 1
MODEL c_grav_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- Gravitational "signal" speed in RS-native units.
Same as c: both use the ledger as substrate. -/
def c_grav_RS : ℝ := 1
THEOREM c_grav_eq_c_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- **G-007 Structural**: In RS-native units, gravity and light have the same
propagation speed (both = 1). The ledger is the single substrate;
there is no separate "gravitational medium" with different tick rate.
GW170817 confirmed c_grav = c to 10⁻¹⁵. RS predicts exact equality. -/
theorem c_grav_eq_c_RS : c_grav_RS = c_RS := rfl
THEOREM speed_ratio_unity · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- When both speeds are defined from the same tick rate, their ratio is 1. -/
theorem speed_ratio_unity : c_grav_RS / c_RS = 1 := by
simp only [c_grav_RS, c_RS, div_one]
What this page does not claim
The framework does not derive the numerical value of c in SI units from first principles. The framework does not prove that physical gravitational waves travel at exactly c; it asserts equality within its model. The declaration does not claim any regime where gravity propagates faster or slower than light.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/PropagationSpeed.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the framework derive the tick rate that sets the value of c in physical units?
- What empirical evidence beyond GW170817 constrains the equality of gravitational and electromagnetic propagation speeds?
- Does the framework's ledger substrate imply a discrete structure for spacetime itself?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
MODEL c_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- In RS-native units: speed of light c = 1 (ledger cells per tick). -/ def c_RS : ℝ := 1In RS-native units, the speed of light is defined as one ledger cell per tick, written c_RS = 1. c_RS · IndisputableMonolith/Gravity/PropagationSpeed.leanMODEL c_grav_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- Gravitational "signal" speed in RS-native units. Same as c: both use the ledger as substrate. -/ def c_grav_RS : ℝ := 1The gravitational signal speed is set to the same value, c_grav_RS = 1. c_grav_RS · IndisputableMonolith/Gravity/PropagationSpeed.leanTHEOREM c_grav_eq_c_RS · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- **G-007 Structural**: In RS-native units, gravity and light have the same propagation speed (both = 1). The ledger is the single substrate; there is no separate "gravitational medium" with different tick rate. GW170817 confirmed c_grav = c to 10⁻¹⁵. RS predicts exact equality. -/ theorem c_grav_eq_c_RS : c_grav_RS = c_RS := rflThe theorem c_grav_eq_c_RS proves the equality by definition: both speeds are literally the same real number 1. c_grav_eq_c_RS · IndisputableMonolith/Gravity/PropagationSpeed.leanTHEOREM speed_ratio_unity · IndisputableMonolith/Gravity/PropagationSpeed.lean
/-- When both speeds are defined from the same tick rate, their ratio is 1. -/ theorem speed_ratio_unity : c_grav_RS / c_RS = 1 := by simp only [c_grav_RS, c_RS, div_one]When both speeds are defined from the same tick rate, their ratio is 1. speed_ratio_unity · IndisputableMonolith/Gravity/PropagationSpeed.lean