c_T_squared
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the coupling α from the Recognition Composition Law.
- Does not include nonlinear terms in the speed expansion.
- Does not compute C_lag from the forcing chain steps.
- Does not address propagation speeds of scalar or vector modes.
formal statement (Lean)
11noncomputable def c_T_squared (α C_lag : ℝ) : ℝ :=
proof body
Definition body.
12 1 + 0.01 * (α * C_lag)
13