falsifiers_default_ok
The theorem confirms that the default illustrative falsifier bands for ILG satisfy the nonnegativity predicate. Researchers testing ILG against PPN, lensing, and GW data would cite it to establish that the chosen defaults are admissible starting points. The proof reduces directly via simplification of the two definitions, followed by repeated constructor applications and numerical normalization to discharge the three inequalities.
claimLet $F$ denote the default falsifier structure with components $ppn_tight = 10^{-5}$, $lensing_band = 1$, and $gw_band = 10^{-6}$. Then all three components of $F$ are nonnegative.
background
The module enumerates falsifier bands for ILG, covering parametrized post-Newtonian (PPN) constraints, gravitational lensing, and gravitational-wave (GW) observations. The structure Falsifiers packages three real numbers that represent admissible deviation bands in each channel. The predicate falsifiers_ok asserts that each of these three numbers is nonnegative, ensuring the bands remain physically meaningful (nonnegative widths).
proof idea
The term proof first simplifies using the definitions of falsifiers_ok and falsifiers_default. It then applies repeat' constructor to split the conjunction into three separate goals, after which norm_num discharges each numerical inequality.
why it matters in Recognition Science
This result certifies that the illustrative default bands supplied in the same module are admissible under the nonnegativity requirement. It supplies a concrete, ready-to-use instance for the enumeration of ILG falsifiers described in the module documentation. No downstream theorems yet depend on it, so its role in larger relativity falsification chains remains open.
scope and limits
- Does not derive the numerical values from observational data.
- Does not claim these bands are optimal or exhaustive.
- Does not address possible correlations among the three channels.
formal statement (Lean)
24@[simp] theorem falsifiers_default_ok : falsifiers_ok falsifiers_default := by
proof body
Term-mode proof.
25 simp [falsifiers_ok, falsifiers_default]
26 repeat' constructor <;> norm_num
27
28end ILG
29end Relativity
30end IndisputableMonolith