R3
plain-language theorem explainer
R3 supplies the three-dimensional Euclidean space for position vectors in angular and feasibility calculations. It is invoked by angleAt, dir, blindCone and the temporal gating predicates to combine spatial directions with eight-tick admissibility checks. The declaration is a direct abbreviation of the Mathlib EuclideanSpace constructor and carries no proof obligations.
Claim. Let $R^3$ denote the three-dimensional Euclidean space over the reals, i.e., the vector space equipped with the standard inner product and norm.
background
The Temporal Gating module abstracts eight-tick discrete sampling windows and pairs them with an angular threshold to form a feasibility predicate. R3 supplies the spatial domain in which directions and angles are computed for that predicate. The abbreviation re-exports the EuclideanSpace ℝ (Fin 3) type already used in the sibling modules ActionSmallAngle and BlindCone, ensuring consistent three-dimensional geometry across the measurement layer.
proof idea
Direct type abbreviation; no lemmas or tactics are applied.
why it matters
R3 anchors the geometric operations that feed angleOK and feasible, which in turn are used by exists_feasible_if_angleOK_and_time_slot. It thereby realizes the T8 step that fixes three spatial dimensions inside the unified forcing chain and supplies the arena for small-angle action and blind-cone constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.