propagation_equality_forced
plain-language theorem explainer
Equal non-zero speeds for light and gravity imply their ratio equals one. This result supports the Recognition Science claim that both forces share the same propagation substrate defined by the tick rate. Physicists modeling gravitational waves alongside electromagnetic signals would invoke it to enforce a common speed limit. The argument reduces to algebraic substitution and the division identity for nonzero reals.
Claim. If $c_ {light} = c_ {grav}$ and $c_ {light} ≠ 0$, then $c_ {grav}/c_ {light} = 1$.
background
The module addresses G-007 on whether gravity propagates at exactly c. It formalizes the RS framework asserting that light and gravity propagate on the same ledger substrate with identical tick rates, yielding the same speed limit. In RS-native units the speed of light is normalized to one cell per tick, so the gravitational speed must match structurally.
proof idea
The proof is a one-line term-mode reduction. It rewrites the target equality using the supplied hypothesis that the two speeds coincide, then invokes the lemma establishing that any nonzero real divided by itself equals one.
why it matters
This theorem closes the basic equality case for propagation speeds in the Gravity module. It directly supports the RS derivation status for G-007 by confirming that equal tick rates force equal speeds without invoking a separate gravitational medium. The result aligns with the framework's normalization where c = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.