no_feasible_if_angle_below_threshold
plain-language theorem explainer
If the angle at x between y and z lies strictly below thetaMin(Amax), then no integer tick index n makes the event feasible for any eight-tick gating parameters. Measurement modelers cite this to exclude geometrically disallowed events before temporal checks. The proof is a term-mode one-liner that extracts the angleOK conjunct from feasible and applies not_le.mpr to the strict inequality.
Claim. If the angle at point $x$ between points $y$ and $z$ satisfies $angleAt(x,y,z) < thetaMin(Amax)$, then for any eight-tick parameters $p$ and any integer $n$, the predicate feasible$(x,y,z,Amax,p,n)$ fails, where feasible is the conjunction of the angular threshold condition and the temporal window condition.
background
The module defines temporal gating via eight-tick discrete windows. R3 is Euclidean space over Fin 3. angleAt computes the angle at x via arccos of the normalized inner product of unit directions to y and z, returning zero on degeneracy. thetaMin(Amax) is arcsin(exp(-Amax)), the minimal admissible angle for given budget Amax. EightTickParams packages a phase in Fin 8 together with a nonempty set of admissible windows. The feasible predicate is defined as the conjunction angleOK x y z Amax and timeOK n p.
proof idea
The proof is a term-mode one-liner. It introduces n and assumes feasible, extracts the left conjunct angleOK to obtain angleAt x y z >= thetaMin Amax, then applies not_le.mpr directly to the hypothesis angleAt < thetaMin to reach a contradiction.
why it matters
This theorem supplies the negative direction for the angle condition in the basic feasibility pair. It immediately precedes and supports the companion result exists_feasible_if_angleOK_and_time_slot by showing that angle violation blocks every n independently of the window set. Within the Recognition framework it sharpens the blind-cone geometry by confirming that only events outside the cone are ruled out before any eight-tick sampling is considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.