`infeasible_below_thetaMin`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle
domain: Measurement
line: 76 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle on GitHub at line 76.

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

formal source

  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

papers checked against this theorem

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