blindCone
plain-language theorem explainer
blindCone defines the set of pairs (y,z) in R3 whose angular separation at x falls strictly below the threshold θmin(Amax). Measurement theorists working with action-constrained directional observations would cite it when bounding unresolvable angles under finite budgets. The definition is realized as a direct set comprehension over the angleAt predicate and the precomputed θmin threshold.
Claim. Let $x$ belong to Euclidean space $R^3$ and let $Amax > 0$ be an action budget. The blind cone is the set of pairs $(y,z) in R^3 times R^3$ such that the angle at $x$ between $y$ and $z$ is strictly less than the minimal threshold angle $theta_min(Amax)$.
background
R3 is the abbreviation for EuclideanSpace R (Fin 3), the standard three-dimensional real vector space equipped with the Euclidean inner product. The sibling definition θmin(Amax) returns the budget-dependent minimal angle via the upstream thetaMin function. The predicate angleAt x y z, imported from ActionSmallAngle, evaluates the angle formed at x by the directions to y and z.
proof idea
The definition is a one-line set comprehension that directly applies angleAt from ActionSmallAngle together with the θmin threshold.
why it matters
This definition supplies the core geometric object for the blind-cone construction in the RecognitionAngle module. It feeds the sibling existence theorem blind_cone_exists and the bound theta_min_le_pi_half. In the Recognition framework it operationalizes the small-angle regime that arises from the J-cost convexity and the eight-tick local dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.