c_grav_eq_c_RS
plain-language theorem explainer
In RS-native units both gravitational and electromagnetic signals propagate at speed 1 on the shared ledger substrate. A physicist working on gravitational-wave propagation or multi-messenger constraints would cite the equality to enforce a single speed limit. The proof is a one-line reflexivity that follows directly from the two constants being defined identically.
Claim. In RS-native units the gravitational propagation speed equals the speed of light: $c_{grav,RS}=c_{RS}=1$.
background
The module addresses G-007: whether gravity propagates at exactly c. In RS-native units the speed of light is defined as c_RS := 1 (one ledger cell per tick). The gravitational signal speed c_grav_RS is defined identically as 1 because both signals use the same ledger substrate with the same tick rate. Upstream results supply alternative expressions for c_RS (the cosmological 8-tick washout prefactor (1 - phi^{-8})^2 and the black-hole leading-log coefficient -log phi / 2), yet the propagation module adopts the structural value 1 for both quantities.
proof idea
The proof is a one-line term that applies reflexivity to the two definitions.
why it matters
This theorem supplies the structural equality required by G-007. It confirms that gravity and light share the ledger substrate and therefore the same speed limit in native units, consistent with the eight-tick octave (T7) and the single-substrate premise. The result matches the GW170817 observational bound to 10^{-15} while predicting exact rather than approximate equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.