The normalized dual direction used by the anchor search and its norm-attaining pairing.

theorem V7.normingDirection_eq_anchorNormingVector {d : ℕ} (q : ℝ) (g : Point d) : normingDirection q g = O3.anchorNormingVector q g

theorem V7.normingDirection_correct : NormingDirectionStatement