GW170817_bound_satisfied
plain-language theorem explainer
The theorem confirms that the Recognition Science squared tensor gravitational wave speed satisfies the GW170817 multi-messenger bound to within 10^{-15}. Researchers comparing modified gravity models to neutron-star merger data would cite this when checking consistency with observed propagation speeds. The proof is a one-line wrapper that directly applies the bound field from the instantiated observational facts class.
Claim. Assuming the gravitational wave observational facts class holds, the absolute difference between the Recognition Science squared tensor speed and unity satisfies $|c_{T,RS}^2 - 1| < 10^{-15}$.
background
In the gravitational wave propagation speed module the squared tensor speed is defined noncomputably as c_T_squared_RS by feeding the argument (1 - 1/phi)/2 together with phi to the power -5 into the function c_T_squared. The class GWObservationalFacts packages the hypothesis that this quantity lies within 10^{-15} of unity. The upstream definition gw170817_bound supplies the concrete numerical threshold 1e-15 together with the comment that it is the coupling bound derived from GW170817 multi-messenger constraints.
proof idea
The proof is a one-line wrapper that applies the gw170817_bound field of the supplied GWObservationalFacts instance.
why it matters
The declaration verifies that the Recognition Science tensor-mode prediction remains compatible with the tight observational limit extracted from the GW170817 event. It sits downstream of the c_T_squared_RS definition and the gw170817_bound hypothesis, thereby closing one consistency check between the phi-ladder structure (with hbar scaling as phi^{-5}) and general-relativity limits on gravitational-wave speed. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.