angleOK
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not incorporate temporal window membership.
- Does not depend on phase or coprime-moduli parameters.
- Does not guarantee existence of any event index.
- Does not extend beyond Euclidean three-space.
Lean usage
example {x y z : R3} {Amax : ℝ} (hθ : angleOK x y z Amax) : ∃ n : ℤ, feasible x y z Amax trivialParams n := by refine exists_feasible_if_angleOK_and_time_slot hθ (by simp [trivialParams])formal statement (Lean)
37def angleOK (x y z : R3) (Amax : ℝ) : Prop :=
proof body
Definition body.
38 angleAt x y z ≥ thetaMin Amax
39
40/-- Combined feasibility for event index `n`. -/