c_T_squared_GR_limit
The result establishes that the squared propagation speed of tensor gravitational waves equals one when both the coupling parameter and the lag parameter are set to zero. Gravitational wave modelers comparing modified gravity predictions against the general relativity baseline would cite this boundary value. The argument is a direct simplification of the explicit linear expression for the speed.
claim$c_T^2(0,0)=1$, where the function is given by $c_T^2(alpha,C_{lag})=1+0.01 alpha C_{lag}$.
background
In the gravitational wave propagation module the squared tensor speed is introduced via an explicit linear correction to the vacuum value. The correction term is proportional to the product of a dimensionless coupling strength and a lag parameter that encodes possible departures from standard propagation. This construction supplies the interpolation between the unmodified general relativity case and modified theories while remaining inside the Recognition Science framework of forced constants and the eight-tick octave.
proof idea
The proof is a one-line wrapper that applies the simplifier tactic directly to the definition of the propagation speed function.
why it matters in Recognition Science
The limit anchors the downstream derived statement that recovers both the general relativity value and the general linear correction form. It therefore supplies the required GR boundary condition for any later comparison with observational constraints on wave speed. The placement is consistent with the T8 requirement of three spatial dimensions and the overall forcing chain that fixes the vacuum speed to unity in the absence of modifications.
scope and limits
- Does not constrain the speed for nonzero values of the coupling or lag parameters.
- Does not incorporate higher-order terms beyond the supplied linear correction.
- Does not derive observational bounds or compare with specific events such as GW170817.
Lean usage
exact c_T_squared_GR_limitformal statement (Lean)
14theorem c_T_squared_GR_limit :
15 c_T_squared 0 0 = 1 := by
proof body
One-line wrapper that applies simp.
16 simp [c_T_squared]
17