pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.GW.PropagationSpeed

show as:
view Lean formalization →

The PropagationSpeed module defines the squared propagation speed of gravitational waves in the Recognition Science framework. It supplies algebraic expressions for c_T² in the GR limit and the RS-specific case, plus checks against GW170817 bounds. Researchers in modified gravity and gravitational wave phenomenology cite these when constraining scalar couplings. The module consists of direct definitions and one-line derivations from the quadratic action.

claimThe module defines the squared propagation speed $c_T^2 = 1 + O(α_C)$ in the RS framework, with the GR limit $c_T^2 = 1$ and an RS-specific value near unity that satisfies the GW170817 bound.

background

The module sits inside the gravitational wave sector of Recognition Science. It imports the fundamental RS time quantum τ₀ = 1 tick from Constants and the quadratic action for tensor modes from ActionExpansion. The setting is tensor perturbation theory in TT gauge, where the propagation speed receives a modification linear in the scalar coupling α_C.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the c_T² definitions that feed the parent Relativity.GW module for tensor perturbation theory and the Constraints module for GW170817 bounds on scalar coupling. It completes the PropagationSpeed component of the gravitational wave analysis chain.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)