IndisputableMonolith.Measurement.RecognitionAngle.BlindCone

   1import Mathlib
   2import IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle
   3
   4/-!
   5# Recognition Blind Cone: Definitions and Basic Properties
   6
   7Defines the blind-cone set at a point `x` for a given action budget `Amax` and
   8proves existence of a positive threshold angle under `Amax>0`.
   9-/
  10
  11noncomputable section
  12
  13open scoped Real
  14
  15namespace IndisputableMonolith
  16namespace Measurement
  17namespace RecognitionAngle
  18
  19abbrev R3 := EuclideanSpace ℝ (Fin 3)
  20
  21/-- Budget-dependent minimal angle threshold. -/
  22@[simp] def θmin (Amax : ℝ) : ℝ := thetaMin Amax
  23
  24/-- The blind cone at `x` with budget `Amax`: pairs `(y,z)` whose separation angle at `x`
  25falls below `θmin(Amax)`. -/
  26def blindCone (x : R3) (Amax : ℝ) : Set (R3 × R3) :=
  27  { p | angleAt x p.1 p.2 < θmin Amax }
  28
  29/-- Existence of a strictly positive threshold angle for any `Amax>0`. -/
  30theorem blind_cone_exists {Amax : ℝ} (hA : 0 < Amax) : 0 < θmin Amax := by
  31  have h := theta_min_range (Amax := Amax) hA
  32  exact h.left
  33
  34/-- Upper bound: `θmin(Amax) ≤ π/2` for any `Amax>0`. Useful for cap-measure bounds. -/
  35theorem theta_min_le_pi_half {Amax : ℝ} (hA : 0 < Amax) : θmin Amax ≤ π/2 := by
  36  have h := theta_min_range (Amax := Amax) hA
  37  exact h.right
  38
  39end RecognitionAngle
  40end Measurement
  41end IndisputableMonolith
  42