pith. sign in
module module high

IndisputableMonolith.Relativity.GW.PropagationSpeed

show as:
view Lean formalization →

The module defines the squared propagation speed c_T² of gravitational waves in the Recognition Science setting. It supplies the general expression, the GR limit, and the RS form with scalar-coupling correction. Gravitational-wave phenomenologists checking modified-gravity predictions against GW170817 would cite these definitions. The module consists of a collection of definitions built directly on the quadratic action supplied by its import.

claim$c_T^2 = 1 + O(\alpha_C)$ (RS modification); $c_T^2 = 1$ (GR limit)

background

The module belongs to the gravitational-wave section of Relativity. It imports the quadratic action for tensor modes from ActionExpansion and the RS time quantum τ₀ = 1 tick from Constants. The local setting is tensor perturbation theory in TT gauge, where the action expansion yields a propagation speed that deviates from unity by a term 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 PropagationSpeed component required by the parent Relativity.GW module, which assembles the full tensor-perturbation framework including the c_T² = 1 + O(α_C) modification. It also supports the Constraints module that applies GW170817 bounds on scalar coupling. It therefore closes the step that translates the RS action into an observable propagation-speed shift.

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)