pith. machine review for the scientific record. sign in
def definition def or abbrev

SignFlipFalsifier

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  66def SignFlipFalsifier (Tmin : ℝ) (tr : Trace) : Prop :=

proof body

Definition body.

  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-/

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.