falsifiers_default
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the band values from the J-cost or phi-ladder.
- Does not claim these bands are tight enough to rule out the ILG model.
- Does not enumerate bands for every observational channel.
Lean usage
example : falsifiers_ok falsifiers_default := by simp [falsifiers_ok, falsifiers_default]formal statement (Lean)
19def falsifiers_default : Falsifiers :=
proof body
Definition body.
20 { ppn_tight := (1/100000 : ℝ)
21 , lensing_band := 1
22 , gw_band := (1/1000000 : ℝ) }
23