EightTickParams

formal source

  23  coprime : Nat.Coprime modA modB := by decide
  24
  25/-- Parameters for eight‑tick gating: a chosen phase and a nonempty set of admissible windows. -/
  26structure EightTickParams where
  27  phase  : Fin 8
  28  window : Set (Fin 8)
  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