structure definition def or abbrev

`Falsifiers`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

   8structure Falsifiers where
   9  ppn_tight    : ℝ
  10  lensing_band : ℝ
  11  gw_band      : ℝ
  12  deriving Repr
  13
  14/-- Predicate that falsifier bands are nonnegative (admissible). -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

displays_invariant_under_equivalence in IndisputableMonolith.Constants.KDisplay decl_use
PhaseLockFalsifier in IndisputableMonolith.Flight.Falsifiers decl_use
lab_schedule_well_separated in IndisputableMonolith.Flight.GravityBridge decl_use
FlightReport in IndisputableMonolith.Flight.Report decl_use
VacuumPersistence in IndisputableMonolith.Gravity.Candidates.Podkletnov decl_use
Protocol in IndisputableMonolith.Measurement.RSNative.Core decl_use
falsifiers_default in IndisputableMonolith.Relativity.ILG.Falsifiers decl_use
falsifiers_ok in IndisputableMonolith.Relativity.ILG.Falsifiers decl_use

depends on (2)

Lean names referenced from this declaration's body.

admissible in IndisputableMonolith.Information.Thermodynamics decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use