falsifiers_default
plain-language theorem explainer
This definition supplies concrete default values for the three fields of the Falsifiers record used to bound deviations in PPN, lensing, and gravitational-wave observables. Researchers testing the ILG model against precision data would cite these defaults to establish baseline consistency. The body is a direct record literal that assigns the three real constants with no lemmas or tactics required.
Claim. The default falsifier bands are the record with fields $ppn_tight = 10^{-5}$, $lensing_band = 1$, and $gw_band = 10^{-6}$.
background
The Falsifiers structure is a record type whose three real-valued fields enumerate admissible bands for post-Newtonian parameter deviations, gravitational lensing, and gravitational-wave propagation speed. The module sets the local theoretical setting by enumerating these bands to support consistency checks for the ILG model. The upstream Falsifiers definition supplies exactly this record type, whose fields are populated directly by the present construction.
proof idea
The definition is realized by a direct record constructor that assigns the three fields to the indicated real constants.
why it matters
This default instance is the concrete value required by the downstream theorem falsifiers_default_ok, which verifies that the supplied bands satisfy the nonnegativity predicate. It anchors the falsification procedure for the ILG model inside the Recognition Science treatment of relativity. The numerical choices remain illustrative and are not derived from the J-cost function or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.