Falsifiers
plain-language theorem explainer
The Falsifiers structure collects three real numbers that mark the admissible bands for testing ILG predictions against PPN data, lensing observations, and gravitational-wave signals. Recognition Science workers cite it when building concrete falsification protocols inside the relativity sector. The declaration is a bare structure definition carrying no lemmas or computational steps.
Claim. A structure $F$ whose fields are three real numbers $ppn_{tight}, lensing_{band}, gw_{band} : ℝ$ that enumerate the admissible falsifier bands for the ILG theory in the parametrized post-Newtonian formalism, gravitational lensing, and gravitational-wave channels.
background
The Relativity.ILG.Falsifiers module supplies data containers for falsification tests of the ILG sector. The upstream admissible predicate from Information.Thermodynamics is the trivial proposition True on any LedgerState, supplying a uniform admissibility check. The phi-ladder lattice hypothesis from NumberTheory.PhiLadderLattice provides a structure that downstream theorems may assume when Poisson-summation arguments on the phi-ladder become available.
proof idea
This is a plain structure definition with three real fields and an automatic Repr derivation. No lemmas or tactics are invoked; the declaration simply packages the three band values for later use.
why it matters
Falsifiers is referenced by displays_invariant_under_equivalence, PhaseLockFalsifier, lab_schedule_well_separated, FlightReport, VacuumPersistence, and Protocol. It supplies the concrete band data required by the ILG falsification layer and thereby supports the Recognition framework’s emphasis on testable predictions in the relativity sector. The structure closes one of the scaffolding interfaces that later theorems discharge when numerical band values are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.