feasible

formal source

  38  angleAt x y z ≥ thetaMin Amax
  39
  40/-- Combined feasibility for event index `n`. -/
  41def feasible (x y z : R3) (Amax : ℝ) (p : EightTickParams) (n : ℤ) : Prop :=
  42  angleOK x y z Amax ∧ timeOK n p
  43
  44/-! ## Basic feasibility theorems (parameterized) -/
  45
  46/-- If the geometric threshold fails, no event index is feasible (for any gating params). -/
  47theorem no_feasible_if_angle_below_threshold
  48    {x y z : R3} {Amax : ℝ} (hθlt : angleAt x y z < thetaMin Amax)
  49    (p : EightTickParams) : ∀ n : ℤ, ¬ feasible x y z Amax p n := by
  50  intro n h
  51  have : angleAt x y z ≥ thetaMin Amax := h.left
  52  exact (not_le.mpr hθlt) this
  53
  54/-- If a geometric threshold holds and there exists a permitted time slot,
  55then a feasible event exists. -/
  56theorem exists_feasible_if_angleOK_and_time_slot
  57    {x y z : R3} {Amax : ℝ} {p : EightTickParams}
  58    (hθ : angleOK x y z Amax) (hslot : ∃ n : ℤ, timeOK n p) :
  59    ∃ n : ℤ, feasible x y z Amax p n := by
  60  rcases hslot with ⟨n, hn⟩
  61  exact ⟨n, And.intro hθ hn⟩
  62
  63/-- Example: with a trivial always-on window, any angle-OK configuration is feasible. -/
  64def trivialParams : EightTickParams :=
  65  { phase := 0, window := Set.univ, hNonempty := by classical exact Set.nonempty_univ }
  66
  67example {x y z : R3} {Amax : ℝ} (hθ : angleOK x y z Amax) :
  68    ∃ n : ℤ, feasible x y z Amax trivialParams n := by
  69  refine exists_feasible_if_angleOK_and_time_slot (x := x) (y := y) (z := z) (Amax := Amax)
  70    (p := trivialParams) hθ ?_
  71  exact ⟨(0 : ℤ), by simp [timeOK, trivialParams]⟩