IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle

   1import Mathlib
   2import IndisputableMonolith.Cost.ClassicalResults
   3
   4/-!
   5# Recognition Angle: Core Definitions
   6
   7This module defines the core objects used across the recognition-angle program:
   8
   9- `R3`: a convenient alias for 3D Euclidean space
  10- `angleAt x y z`: the geometric angle at `x` between the directions to `y` and `z`
  11- `A_of_theta θ := -log (sin θ)`: the kernel action as a function of the sensor angle
  12- `thetaMin Amax := arcsin (exp (-Amax))`: the budget-dependent minimal recognizable angle
  13
  14These are formulation-level definitions with conservative totality: `angleAt` is set to `0`
  15on degeneracies (`y = x` or `z = x`). Theorems and properties are developed in sibling
  16modules.
  17-/
  18
  19noncomputable section
  20
  21open scoped Real
  22
  23namespace IndisputableMonolith
  24namespace Measurement
  25namespace RecognitionAngle
  26
  27/-! ## Space and basic vectors -/
  28
  29abbrev R3 := EuclideanSpace ℝ (Fin 3)
  30
  31/-- Unit direction from `x` to `y` in `R3`; returns `0` on degeneracy. -/
  32def dir (x y : R3) : R3 :=
  33  let v := (y - x)
  34  if h : ‖v‖ = 0 then 0 else v / ‖v‖
  35
  36/-- Angle at `x` between rays to `y` and `z`, defined via `arccos` of the inner product
  37of unit directions. Returns `0` if either ray is degenerate. Range is in `[0, π]`. -/
  38def angleAt (x y z : R3) : ℝ :=
  39  let u := dir x y
  40  let v := dir x z
  41  if (u = 0) ∨ (v = 0) then 0 else Real.arccos ((⟪u, v⟫_ℝ) / (‖u‖ * ‖v‖))
  42
  43/-! ## Kernel action and budget threshold -/
  44
  45/-- Kernel action as a function of the sensor angle `θ`. Domain of interest is `(0, π/2]`. -/
  46def A_of_theta (θ : ℝ) : ℝ := -Real.log (Real.sin θ)
  47
  48/-- For budget `Amax > 0`, the minimal admissible angle. -/
  49def thetaMin (Amax : ℝ) : ℝ := Real.arcsin (Real.exp (-Amax))
  50
  51/-! ## Core limit and threshold lemmas (via classical results) -/
  52
  53open Filter
  54
  55/-- As θ → 0⁺, the kernel action `A_of_theta θ = -log(sin θ)` diverges to `+∞`. -/
  56theorem action_small_angle_diverges :
  57  Tendsto (fun θ => A_of_theta θ) (nhdsWithin 0 (Set.Ioi 0)) atTop := by
  58  simpa [A_of_theta] using
  59    IndisputableMonolith.Cost.ClassicalResults.neg_log_sin_tendsto_atTop_at_zero_right
  60
  61/-- Budget inequality implies the minimal angle threshold. -/
  62theorem theta_min_spec {Amax θ : ℝ}
  63    (hA : 0 < Amax) (hθ0 : 0 < θ) (hθh : θ ≤ π/2)
  64    (hAineq : A_of_theta θ ≤ Amax) :
  65    θ ≥ thetaMin Amax := by
  66  simpa [A_of_theta, thetaMin] using
  67    IndisputableMonolith.Cost.ClassicalResults.theta_min_spec_inequality Amax θ hA hθ0 hθh hAineq
  68
  69/-- Threshold is strictly positive and ≤ π/2 for any `Amax>0`. -/
  70theorem theta_min_range {Amax : ℝ} (hA : 0 < Amax) :
  71    0 < thetaMin Amax ∧ thetaMin Amax ≤ π/2 := by
  72  simpa [thetaMin] using
  73    IndisputableMonolith.Cost.ClassicalResults.theta_min_range Amax hA
  74
  75/-- If the angle is below the budget threshold, the action exceeds the budget. -/
  76theorem infeasible_below_thetaMin {Amax θ : ℝ}
  77    (hA : 0 < Amax) (hθ0 : 0 < θ) (hθh : θ ≤ π/2)
  78    (hθlt : θ < thetaMin Amax) :
  79    A_of_theta θ > Amax := by
  80  -- Using the contrapositive of `theta_min_spec` packaged as a classical result
  81  -- `theta_min_spec_inequality` gives the forward direction; we obtain strictness here.
  82  -- This is encoded in `theta_min_spec_inequality` by strict monotonicity in the classical block.
  83  -- Rearranged here as a direct statement on `A_of_theta`.
  84  have h := IndisputableMonolith.Cost.ClassicalResults.theta_min_spec_inequality Amax θ hA hθ0 hθh
  85  -- By contradiction on ≤
  86  by_contra hle
  87  have : θ ≥ thetaMin Amax := by simpa [A_of_theta, thetaMin] using h hle
  88  exact (lt_of_lt_of_le hθlt this).false.elim
  89
  90end RecognitionAngle
  91end Measurement
  92end IndisputableMonolith
  93