c_T_squared_near_one
plain-language theorem explainer
The theorem shows that the squared tensor speed of gravitational waves stays within one percent of the speed of light when the coupling parameters satisfy |α| < 0.3 and |C_lag| < 0.2. Analysts of binary-merger waveforms would cite the bound to confirm that the Recognition Science correction remains compatible with observed luminal propagation. The argument expands the explicit linear definition of the speed expression and bounds the product term by repeated application of the multiplication inequality together with the supplied absolute-value假设
Claim. If $|α| < 0.3$ and $|C_{lag}| < 0.2$, then $|c_T^2(α, C_{lag}) - 1| < 0.01$, where $c_T^2(α, C_{lag}) = 1 + 0.01 α C_{lag}$.
background
The module defines the squared tensor speed by the linear correction $c_T^2(α, C_{lag}) = 1 + 0.01 α C_{lag}$. The lag parameter originates in the eight-tick resonance construction as $C_{lag} = φ^{-5} ≈ 0.09$. The present result supplies a uniform numerical check that this correction remains small inside the stated intervals on the couplings.
proof idea
The tactic proof first unfolds the definition of the speed expression. It then rewrites the absolute value of the product via abs_mul, factors into separate absolute values, and applies mul_lt_mul twice to replace |α| and |C_lag| by the supplied bounds 0.3 and 0.2. The resulting product 0.006 is compared to 0.01 by norm_num.
why it matters
The bound supplies a concrete consistency check between the Recognition Science correction to gravitational-wave speed and the tight observational limit from events such as GW170817. It rests on the eight-tick octave that fixes C_lag = φ^{-5} and on the linear action expansion that produces the 0.01 prefactor. The result supports compatibility with luminal propagation inside the model without further tuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.