GWObservationalFacts
plain-language theorem explainer
GWObservationalFacts defines a typeclass that asserts the RS tensor speed squared lies within 10^{-15} of unity. Researchers comparing gravitational wave propagation in modified gravity to multi-messenger data cite it to enforce empirical consistency. The definition is a direct packaging of the upstream numerical threshold onto the model expression c_T_squared_RS.
Claim. The class asserts that $|c_{T,RS}^2 - 1| < 10^{-15}$, where $c_{T,RS}^2$ denotes the squared tensor propagation speed evaluated in the Recognition Science model at the indicated phi-dependent parameters.
background
The module Relativity.GW.PropagationSpeed compares tensor mode speeds under the Recognition Science action expansion against general relativity limits. It draws on two upstream definitions: gw170817_bound, the real number 1e-15 described as the hypothesis from GW170817 multi-messenger constraints, and c_T_squared_RS, which applies the function c_T_squared to the arguments ((1 - 1/phi)/2) and phi^{-5}. These supply the observational threshold and the RS-specific speed that the class combines into a single Prop.
proof idea
The declaration is a class definition introducing a Prop with one field. It directly references the upstream gw170817_bound definition and applies the bound to the already-computed quantity c_T_squared_RS.
why it matters
This class supplies the hypothesis for the downstream theorem GW170817_bound_satisfied, which extracts the field to confirm the RS model respects the observational limit. It anchors the computed proximity of c_T_squared_RS to 1, arising from the phi-ladder structure, to the GW170817 constraint and thereby supports consistency with the GR limit inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.