coupling_bound_from_GW170817_hypothesis
plain-language theorem explainer
This definition encodes the implication that a GW170817-level limit on tensor speed deviation forces the product of the coupling parameter and lag constant below a derived threshold. Researchers checking modified gravity models against multi-messenger data would cite it when testing Recognition Science consistency. The content follows from direct substitution into the explicit tensor speed formula and algebraic rearrangement of the resulting inequality.
Claim. If $|c_T^2 - 1| < 10^{-15}$, then $|α C_{lag}| < 10^{-13}$, where $c_T^2 = 1 + 0.01 α C_{lag}$.
background
The tensor speed squared is defined as 1 plus a correction term 0.01 times the product of the coupling α and the lag constant C_lag. The lag itself is fixed at phi to the minus five from the eight-tick resonance construction, while the numerical bound 10 to the minus 15 is taken directly from the GW170817 multi-messenger limit on propagation speed deviation. This definition appears in the gravitational wave constraints module, which imports the propagation speed expression and the resonance lag.
proof idea
The definition is a one-line wrapper obtained by substituting the explicit c_T squared formula into the deviation inequality and dividing through by the coefficient 0.01 to isolate the product α C_lag.
why it matters
It supplies the concrete coupling bound required by the sibling hypothesis that Recognition Science satisfies the GW170817 constraint. The step links the phi-ladder and eight-tick parameters to observational limits in the relativity sector of the forcing chain. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.