angleAt
plain-language theorem explainer
angleAt defines the Euclidean angle at point x between directions to y and z in three-dimensional space via arccos of the normalized inner product of unit vectors, returning zero on degeneracy. Measurement theorists in the Recognition Science program cite it when deriving angle thresholds for event feasibility under action budgets. The definition binds unit directions first then applies the standard arccos formula with an explicit zero-vector guard.
Claim. Let $x, y, z$ lie in three-dimensional Euclidean space. The angle at $x$ between the rays to $y$ and $z$ equals $0$ if either direction vector vanishes, otherwise equals $arccos( (u · v) / (|u| |v|) )$ where $u$ and $v$ are the unit vectors from $x$ to $y$ and from $x$ to $z$.
background
The module defines R3 as Euclidean space over three dimensions and introduces angleAt as the angle between two rays sharing vertex x. It pairs this with the kernel action A_of_theta(θ) := -log(sin θ) on (0, π/2] and the budget-dependent threshold thetaMin(Amax) := arcsin(exp(-Amax)). These objects supply the geometric layer for recognition feasibility checks.
proof idea
The definition first computes unit directions u := dir x y and v := dir x z. It returns zero whenever u or v is the zero vector; otherwise it evaluates Real.arccos of the normalized inner product. No auxiliary lemmas are required beyond the vector library primitives.
why it matters
angleAt supplies the geometric primitive for blindCone (pairs whose separation falls below thetaMin) and for angleOK (admissibility predicate). It directly enables the theorem no_feasible_if_angle_below_threshold, which shows sub-threshold angles block every event index. In the Recognition Science setting this implements the sensor-angle constraint that links J-cost action to observable separations inside the eight-tick octave and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.