`R3`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating
domain: Measurement
line: 17 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating on GitHub at line 17.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.