dir
plain-language theorem explainer
The dir function returns the unit vector in the direction from x to y in three-dimensional Euclidean space, defaulting to the zero vector on degeneracy. Researchers constructing ribbon models or angular recognition kernels cite this normalization when building winding numbers and cancellation predicates. The definition subtracts the position vectors and scales by the reciprocal norm unless the displacement vanishes.
Claim. For points $x, y$ in Euclidean space $R^3$, let $v = y - x$. Then dir$(x,y) = v/|v|$ if $|v| > 0$, and $0$ otherwise.
background
R3 is the abbreviation for EuclideanSpace ℝ (Fin 3), i.e., ordinary three-dimensional real vectors equipped with the standard inner product and norm. The module supplies the geometric primitives for the recognition-angle program: the angle at a vertex between two rays, the action kernel A_of_theta(θ) = -log(sin θ), and the minimal recognizable angle thetaMin derived from an action budget. These objects remain purely kinematic at this layer; recognition costs and phi-ladders enter only in downstream modules.
proof idea
The definition is a direct case distinction: compute the displacement vector v = y - x, then return the normalized vector v/‖v‖ when the norm is positive and the zero vector otherwise. No external lemmas are applied; the construction is a one-line wrapper around vector subtraction and norm scaling.
why it matters
dir supplies the direction component of Ribbon syllables in the Masses.Ribbons module, enabling the cancels predicate, winding count on the eight-tick clock, and normal-form length ell. It therefore anchors the geometric substrate required for the recognition-angle action kernel and for the three-dimensional spatial structure forced at T8 of the unified forcing chain. The definition closes a basic interface that downstream angleAt and ribbon constructions rely upon without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.