def
definition
def or abbrev
BandingFalsifier
show as:
view Lean formalization →
formal statement (Lean)
50def BandingFalsifier (εp : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
proof body
Definition body.
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-/