SignFlipFalsifier

formal source

  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
  73There exist two times `t1 < t2` under sustained pulsing such that the thrust
  74proxy decays significantly.
  75
  76This encodes the *failure mode* claim (“continuous forcing degrades performance”).
  77It does **not** yet encode the “pulsing restores it” part; that will require
  78either richer trace fields (power/temperature) or explicit segment labels.
  79-/
  80def PhaseLockFalsifier (window : ℕ) (drop : ℝ) (tr : Trace) : Prop :=
  81  ∃ t1 t2,
  82    t1 < t2 ∧
  83    (∀ t, t1 ≤ t ∧ t < t1 + window → (tr.schedule t).pulse = true) ∧
  84    (∀ t, t2 ≤ t ∧ t < t2 + window → (tr.schedule t).pulse = true) ∧
  85    (tr.thrust t1).2.2 - (tr.thrust t2).2.2 ≥ drop
  86
  87end Falsifiers
  88end Flight
  89end IndisputableMonolith
  90