c_T_squared
plain-language theorem explainer
The definition supplies the squared tensor gravitational wave speed as one plus a linear correction 0.01 times the product of coupling strength α and lag constant C_lag. Gravitational wave phenomenologists and RS modelers cite it when testing consistency with the GW170817 multi-messenger bound. It is introduced as a direct algebraic assignment that expands around the GR value of unity.
Claim. The squared tensor speed is given by $c_T^2 (α, C_{lag}) = 1 + 0.01 α C_{lag}$.
background
The module on gravitational wave propagation speed parameterizes deviations from general relativity through a linear correction controlled by the coupling α and the lag C_lag. The lag constant originates in the eight-tick resonance module as C_lag = φ^{-5}, the RS-derived value fixed by the self-similar fixed point of the forcing chain. This choice places the correction at the scale set by the phi-ladder and the eight-tick octave.
proof idea
The declaration is a one-line definition that directly assigns the arithmetic expression 1 + 0.01 * (α * C_lag). No lemmas or tactics are applied.
why it matters
It supplies the central expression used by c_T_squared_GR_limit (recovers unity at vanishing parameters), c_T_squared_near_one (bounds the deviation for small α and C_lag), and c_T_squared_RS (instantiates the RS values). Downstream it supports the hypothesis coupling_bound_from_GW170817_hypothesis that checks the model against the observed propagation speed constraint. In the framework it encodes the effect of the lag coupling on tensor mode speed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.