falsifiers_ok
plain-language theorem explainer
falsifiers_ok encodes the admissibility predicate for ILG falsifier bands by requiring each of the three real parameters to be nonnegative. Researchers checking consistency of ILG deviations with PPN, lensing, and GW data would invoke this predicate. The definition is a direct conjunction of three inequalities on the fields of the Falsifiers record.
Claim. Let $f$ be a record with real components $f_ {ppn}, f_{lens}, f_{gw}$. Then falsifiers_ok$(f)$ holds precisely when $f_{ppn} ≥ 0$, $f_{lens} ≥ 0$, and $f_{gw} ≥ 0$.
background
The Falsifiers structure enumerates three real-valued bands that bound possible ILG deviations: the tight PPN parameter, the lensing band, and the GW band. The module supplies these bands so that downstream checks can test whether ILG remains compatible with existing observations. The upstream admissible predicate from Information.Thermodynamics is the trivial proposition True, so the only nontrivial constraint introduced here is nonnegativity of the bands themselves.
proof idea
The definition is a direct conjunction of the three inequalities on the record fields. No lemmas or tactics are required; the body is the primitive statement of the predicate.
why it matters
This predicate is the admissibility condition consumed by the theorem falsifiers_default_ok, which verifies the default illustrative bands. It supplies the concrete nonnegativity gate needed for any ILG falsification argument inside the relativity module. The definition therefore closes the interface between the enumerated bands and the consistency checks that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.