VacuumTestFalsifier

formal source

  39(This is a *one-way* falsifier: failure does not disprove the model unless
  40we control for other conditions.)
  41-/
  42def VacuumTestFalsifier (p_max : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
  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-/
  50def BandingFalsifier (εp : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
  51  ∃ t1 t2 t3,
  52    t1 < t2 ∧ t2 < t3 ∧
  53    |tr.ambientPressure t1 - tr.ambientPressure t2| ≤ εp ∧
  54    |tr.ambientPressure t2 - tr.ambientPressure t3| ≤ εp ∧
  55    (tr.thrust t1).2.2 < Tmin ∧
  56    (tr.thrust t2).2.2 ≥ Tmin ∧
  57    (tr.thrust t3).2.2 < Tmin
  58
  59/-- Sign-flip falsifier:
  60
  61Under a schedule “handedness flip” (modeled externally), thrust should flip sign.
  62
  63At the trace level, we encode this as the existence of two segments with
  64opposite-signed vertical thrust.
  65-/
  66def SignFlipFalsifier (Tmin : ℝ) (tr : Trace) : Prop :=
  67  ∃ tpos tneg,
  68    (tr.thrust tpos).2.2 ≥ Tmin ∧
  69    (tr.thrust tneg).2.2 ≤ -Tmin
  70
  71/-- Phase-lock falsifier (display-level):
  72