c_T_squared_GR_limit
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.