falsifiers_default
plain-language theorem explainer
This definition supplies concrete default values for the three tolerance bands in the Falsifiers structure used by ILG consistency checks. Researchers testing Recognition Science predictions against PPN, lensing, and gravitational-wave data would reference these defaults to initialize admissibility verification. The definition is a direct record constructor that assigns three explicit real constants.
Claim. The default falsifier bands are given by $ppn_{tight} = 10^{-5}$, $lensing_{band} = 1$, $gw_{band} = 10^{-6}$.
background
The Falsifiers structure enumerates three real-valued bands for testing ILG against observations: ppn_tight for post-Newtonian parameter constraints, lensing_band for gravitational lensing, and gw_band for gravitational waves. The module sets the local context as enumerating falsifier bands for ILG. The upstream Falsifiers definition provides the structure type that this default populates.
proof idea
The definition directly constructs the Falsifiers record by assigning the three specified real values to the respective fields.
why it matters
This default populates the Falsifiers type and is used by the theorem falsifiers_default_ok to verify admissibility via simplification and norm_num. It supports the ILG falsification framework in Relativity by providing concrete starting values for band checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.