timeOK

formal source

  29  hNonempty : window.Nonempty
  30
  31/-- Temporal admissibility for a tick index `n`. -/
  32def timeOK (n : ℤ) (p : EightTickParams) : Prop :=
  33  let cls : Fin 8 := (Int.toNat (Int.emod n 8)).toFin
  34  cls ∈ p.window
  35
  36/-- Geometric admissibility (angle threshold). -/
  37def angleOK (x y z : R3) (Amax : ℝ) : Prop :=
  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