thetaMin
plain-language theorem explainer
The definition supplies the budget-dependent minimal admissible angle via thetaMin(Amax) = arcsin(exp(-Amax)). Measurement theorists enforcing recognition constraints on sensor geometries cite this when bounding angles by kernel action budgets. It is a direct functional definition that inverts the relation A_of_theta(θ) = Amax without additional lemmas.
Claim. For a budget $A>0$, the minimal admissible angle is given by $θ_min(A) = arcsin(e^{-A})$.
background
The module defines the kernel action as A_of_theta(θ) := -log(sin θ) on (0, π/2] and introduces thetaMin as its inverse for a given budget. Local conventions treat angleAt as the geometric angle at a point in R3 (set to zero on degeneracies) and rely on classical inequalities for the action. Upstream results include the BIT kernel (constant, inverse-linear, or exponential forms) and ILG kernel (power-law form with cutoff), both feeding into action bounds via the referenced classical results on monotonicity.
proof idea
Direct definition that composes Real.exp and Real.arcsin to solve A_of_theta(θ) = Amax for θ. No lemmas or tactics are invoked; the expression is the closed-form inverse of the sibling A_of_theta definition.
why it matters
This definition anchors feasibility checks throughout the recognition-angle program. It is invoked by theta_min_spec and infeasible_below_thetaMin to convert action budgets into angle thresholds, and appears in BlindCone.R3 and TemporalGating.angleOK for event admissibility. In the Recognition framework it realizes the small-angle limit of the kernel action, consistent with the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.