c_T_squared_derived
plain-language theorem explainer
The declaration establishes that the squared tensor gravitational-wave speed equals unity at vanishing couplings and admits a linear correction in the product of the parameters α and C_lag. Gravitational-wave analysts working in modified-gravity extensions would cite the identity when bounding deviations from general relativity. The argument is a direct term-mode construction that invokes the GR-limit case and supplies the explicit numerical prefactor 0.01.
Claim. $c_T^2(0,0)=1$ and for all real numbers α and C_lag there exists a real number coeff such that $c_T^2(α,C_lag)=1+coeff·(α·C_lag)$.
background
The module defines the squared tensor-wave speed as the linear function 1 + 0.01·(α·C_lag). C_lag is the lag coupling φ^{-5} taken from the eight-tick resonance construction. The auxiliary coefficient function from the pipelines module supplies the series expansion used elsewhere for gap corrections, though the present statement only requires existence of some real multiplier. The local setting is the propagation-speed analysis within the gravitational-wave sector of the Recognition Science framework.
proof idea
The proof applies the constructor tactic to split the conjunction. The first conjunct is discharged by direct appeal to the GR-limit theorem c_T_squared_GR_limit. The second conjunct is handled by introducing the universal quantifiers, refining the existential witness to the constant 0.01, and simplifying the definition of c_T_squared.
why it matters
This result anchors the parameterization of tensor-mode propagation speed in the RS-derived gravitational-wave sector. It supplies the exact GR limit together with the leading correction term that feeds into observational bounds such as those from GW170817. Within the framework it connects the eight-tick resonance lag C_lag to the propagation-speed deviation, consistent with the overall forcing chain that fixes D=3 and the value of α^{-1} near 137.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.