def definition def or abbrev

`PhaseLockFalsifier`

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

formal statement (Lean)

  80def PhaseLockFalsifier (window : ℕ) (drop : ℝ) (tr : Trace) : Prop :=

proof body

Definition body.

  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

used by (1)

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

FlightReport in IndisputableMonolith.Flight.Report decl_use

depends on (2)

Lean names referenced from this declaration's body.

Trace in IndisputableMonolith.Flight.Falsifiers decl_use
Falsifiers in IndisputableMonolith.Relativity.ILG.Falsifiers decl_use