falsifiers_default_ok
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.