gw170817_bound
plain-language theorem explainer
The declaration fixes the real number 10^{-15} as the GW170817 bound on deviations of gravitational-wave propagation speed from light speed. Researchers checking modified-gravity or Recognition Science models against LIGO-Virgo multi-messenger data cite this constant to enforce consistency. The definition is a direct constant assignment with no lemmas or computation.
Claim. The GW170817 bound equals the real number $10^{-15}$.
background
The Relativity.GW.Constraints module encodes observational limits on tensor-mode speed. It imports PropagationSpeed, which introduces the class GWObservationalFacts containing the bound as a hypothesis. Upstream, the Hypothesis structure from CPM2D bundles constants and functionals for GalerkinState models together with projection_defect and energy-control inequalities. The from theorem in PrimitiveDistinction reduces seven axioms to four structural conditions plus three definitional facts.
proof idea
The definition is a direct constant assignment of 1e-15. No lemmas are invoked and no tactics are executed.
why it matters
The constant is referenced by GW_constraint_framework, which proves the bound is strictly less than 0.001, by RS_satisfies_GW_bound_hypothesis, and by GW170817_bound_satisfied in the PropagationSpeed module. It supplies the observational anchor that lets Recognition Science models satisfy the T7 eight-tick octave and T8 spatial-dimension constraints on propagation speed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.