A sufficiently narrow quarter-turn cone avoids a non-collinear ray

Proved

PlanarRot90ConeAvoidsRay

by xuanji · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometryplanar-rotation

Let $d$ be a nonzero planar direction and let $v$ fail to be a positive scalar multiple of $d$ . Then there is a constant $\kappa>0$ such that every point of the nonnegative ray generated by $v$ is distinct from every point of the form

td+s\,R_{90}(d),

whenever $t>0$ , $s e0$ , and $|s|<\kappa t$ . Thus a sufficiently narrow signed quarter-turn cone around the positive $d$ -ray avoids the nonnegative $v$ -ray. The lemma supplies the quantitative cone aperture used in polygonal collar constructions.

Preamble

import Definitions.Def_PlanarRot90

open Classical
noncomputable section

Formal statement

theorem PlanarRot90ConeAvoidsRay {d v : EuclideanSpace ℝ (Fin 2)}
    (hd : d ≠ 0) (_hnot : ¬ ∃ a : ℝ, 0 < a ∧ v = a • d) :
    ∃ κ : ℝ, 0 < κ ∧
      ∀ c t s : ℝ, 0 ≤ c → 0 < t → s ≠ 0 → |s| < κ * t →
        c • v ≠ t • d + s • PlanarRot90 d := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PlanarRot90ConeAvoidsRay.lean#L1-L82

View graph