infeasible_below_thetaMin
plain-language theorem explainer
The theorem states that any angle θ strictly below the budget-dependent minimum thetaMin(Amax) forces the kernel action A_of_theta(θ) to exceed the budget Amax. Analysts of recognition thresholds in physical measurements cite it to bound feasible sensor angles under fixed action cost. The proof is a short contradiction that invokes the classical inequality theta_min_spec_inequality and uses strict monotonicity of the action function to reach a falsehood.
Claim. Let $A>0$ and $0<θ≤π/2$. If $θ<θ_min(A)$ then $A(θ)>A$, where $A(θ):=-log(sin θ)$ and $θ_min(A):=arcsin(exp(-A)).
background
The module defines the kernel action $A(θ):=-log(sin θ)$ on $(0,π/2]$ and the minimal admissible angle $θ_min(A):=arcsin(exp(-A))$ for positive budget $A$. These objects formalize the cost of recognizing a direction in three-dimensional space under a fixed action budget. The result depends on the classical inequality theta_min_spec_inequality, which encodes the forward direction from action bound to angle lower bound via monotonicity of log and sine.
proof idea
The proof applies theta_min_spec_inequality to obtain the forward implication from action ≤ Amax to θ ≥ thetaMin Amax. It assumes for contradiction that A_of_theta θ ≤ Amax, derives θ ≥ thetaMin Amax via the inequality, and obtains a direct falsehood with the hypothesis θ < thetaMin Amax.
why it matters
This theorem supplies the sharp infeasibility boundary for the recognition-angle program. It supports the claim that recognition is limited by the action budget and feeds the broader measurement framework that links to the phi-ladder and discrete tiers in Recognition Science. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.