theta_min_spec
plain-language theorem explainer
For positive budget Amax and angle θ in (0, π/2], the condition that kernel action A(θ) stays at most Amax forces θ to meet or exceed arcsin(exp(-Amax)). Measurement models cite this when bounding feasible sensor angles under action budgets. The proof is a one-line wrapper that applies the classical inequality theorem after unfolding the local definitions.
Claim. Assume $A>0$, $0<θ≤π/2$, and $-log(sin θ)≤A$. Then $θ≥arcsin(exp(-A))$.
background
The module defines the kernel action as $A(θ)=-log(sin θ)$ on the interval (0, π/2] and the threshold as $θ_min(A)=arcsin(exp(-A))$. These objects link geometric sensor angles to action costs in the recognition-angle program. The result rests on the upstream classical inequality theorem that encodes the identical implication before the local definitions are introduced.
proof idea
One-line wrapper that applies the classical theorem theta_min_spec_inequality from Cost.ClassicalResults and uses simpa to unfold A_of_theta and thetaMin.
why it matters
Supplies the forward implication used by the downstream theorem infeasible_below_thetaMin, which shows that angles below the threshold make action exceed the budget. It closes the budget-to-angle step inside the measurement module and aligns with the action kernel definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.