GW_constraint_framework
plain-language theorem explainer
The theorem asserts the existence of a coupling bound from the GW170817 event that matches the predefined value of 10^{-15} and remains below 0.001. Gravitational wave physicists testing propagation speed deviations would reference this to anchor multi-messenger constraints. The proof works by exhibiting the bound explicitly and confirming the numerical inequality through simplification and numeric normalization.
Claim. There exists a real number $b$ such that $b = 10^{-15}$ and $b < 0.001$.
background
The GW170817 bound is defined as the real constant 1e-15, serving as a hypothesis for coupling strength derived from multi-messenger constraints on the GW170817 event. This sits in the Relativity.GW.Constraints module, which imports propagation speed results to enforce consistency with observed signals from binary neutron star mergers. The upstream definition supplies the concrete numerical value used throughout the constraint framework.
proof idea
The term proof constructs the existential witness directly as the predefined bound, applies reflexivity to the equality, and invokes simplification followed by numeric normalization to verify the strict inequality.
why it matters
This result supplies the core verified constraint in the GW module, confirming the GW170817 hypothesis meets the required tightness threshold. It supports the Recognition Science approach to relativity by linking observed bounds to the forcing chain's implications for constants and propagation. With no downstream uses recorded, it closes a basic verification step in the constraints layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.