Pith. sign in
module module high

IndisputableMonolith.Gravity.PropagationSpeed

show as:
view Lean formalization →

Gravity.PropagationSpeed module fixes gravitational wave speed to the light speed in RS-native units where c equals one ledger cell per tick. Unified gravity modelers cite the equality chain when embedding propagation into the RS forcing sequence. The module imports the constants definition and assembles sibling declarations that equate c_RS with c_grav_RS.

claimIn RS-native units, $c_{ m RS}=1$ (ledger cells per tick) and $c_{ m grav,RS}=1$, with the propagation equality $c_{ m grav,RS}=c_{ m RS}$ holding by definition.

background

The module sits inside the Gravity domain of Recognition Science and imports the Constants module whose sole content is the time quantum τ₀ = 1 tick. All speeds are therefore expressed as ledger cells per tick, forcing the light speed c_RS to the numerical value 1. The sibling declarations c_grav_RS, c_grav_eq_c_RS, propagation_implies_equal_speed, speed_ratio_unity and propagation_equality_forced then extend the same normalization to gravitational propagation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the propagation-speed normalization required by any downstream gravity construction that inherits the RS-native unit system. It directly supports the eight-tick octave and D=3 spatial structure by ensuring gravitational signals travel at the same ledger-cell speed as electromagnetic ones.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)