def definition def or abbrev

`VacuumTestFalsifier`

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

formal statement (Lean)

  42def VacuumTestFalsifier (p_max : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=

proof body

Definition body.

  43  (∃ t, tr.ambientPressure t ≤ p_max ∧ (tr.thrust t).2.2 ≥ Tmin)
  44
  45/-- Banding falsifier:
  46
  47There exist times `t1 < t2 < t3` with similar ambient pressure but discrete
  48thrust states (off/on/off). This encodes the “banded operating regimes” claim.
  49-/

used by (2)

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

FlightReport in IndisputableMonolith.Flight.Report decl_use
VacuumPersistence in IndisputableMonolith.Gravity.Candidates.Podkletnov decl_use

depends on (3)

Lean names referenced from this declaration's body.

Trace in IndisputableMonolith.Flight.Falsifiers decl_use
pressure in IndisputableMonolith.ILG.PressureForm decl_use
p_max in IndisputableMonolith.QFT.UVCutoff decl_use