IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating

   1import Mathlib
   2import IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle
   3
   4/-!
   5# Temporal Gating: Eight‑Tick Windows and Feasibility Predicate
   6
   7Abstracts the discrete sampling/gating windows (eight‑tick) and defines a feasibility
   8predicate combining the angular threshold with temporal admissibility.
   9-/
  10
  11noncomputable section
  12
  13namespace IndisputableMonolith
  14namespace Measurement
  15namespace RecognitionAngle
  16
  17abbrev R3 := EuclideanSpace ℝ (Fin 3)
  18
  19/-- Coprime moduli framing for double-period phasing (e.g., 8 and 45). -/
  20structure PhaseParams where
  21  modA : ℕ := 8
  22  modB : ℕ := 45
  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
  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]⟩
  72
  73end RecognitionAngle
  74end Measurement
  75end IndisputableMonolith
  76