Coefficient uniqueness in the planar quarter-turn basis

Proved

PlanarRot90CoefficientUniqueness

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

crossing-consequencesgeometrypolygonal

For a nonzero planar direction $d$ , if a vector $v$ is represented as $a d+b\,\operatorname{PlanarRot90}(d)$ , then the coefficients are recovered by the two normalized inner products with $d$ and its quarter-turn.

Preamble

import Definitions.Def_PlanarRot90

open Classical
noncomputable section

Formal statement

lemma PlanarRot90CoefficientUniqueness {d v : EuclideanSpace ℝ (Fin 2)}
    (hd : d ≠ 0) {a b : ℝ}
    (h : v = a • d + b • PlanarRot90 d) :
    a = inner ℝ v d / (‖d‖ ^ 2) ∧
      b = inner ℝ v (PlanarRot90 d) / (‖d‖ ^ 2) := by sorry

Source

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

View graph