angleOK
plain-language theorem explainer
The definition encodes geometric admissibility for three points in Euclidean three-space under a fixed action budget. It is invoked by combined feasibility predicates that merge angular and temporal constraints inside eight-tick sampling windows. The body reduces directly to a comparison between the angle formed by unit directions and the budget-derived threshold arcsin of the negative exponential.
Claim. For vectors $x,y,z$ in Euclidean three-space and budget parameter $A>0$, the condition holds precisely when the angle at $x$ between the rays to $y$ and $z$ satisfies angle at $x$ between rays to $y$ and $z$ is at least arcsin of exp of negative $A$.
background
The module abstracts discrete eight-tick gating windows and pairs them with a feasibility predicate. Points live in Euclidean three-space. The angle at a reference point is recovered from the arccos of the normalized inner product of unit directions, returning zero on degeneracy. The minimum admissible angle for budget $A$ is the arcsine of the exponential decay of that budget, enforcing the small-angle action limit.
proof idea
One-line wrapper that applies the angle computation between unit directions and compares the result to the budget threshold function.
why it matters
It supplies the angular half of the combined feasibility predicate. That predicate is used by the existence theorem for feasible events whenever both the angle condition and a permitted time slot are present. The definition therefore closes the geometric admissibility requirement inside the eight-tick gating abstraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.