Vanishing of exceptional tangent derivatives

The derivative of either rational graph intersects the obstruction kernel only in zero. Denominators are cleared using the strictly positive squared trace length; the remaining identities are polynomial certificates.

theorem PlanarMidpoint.Q_tangent_obstruction_zero {τ : E} (hτ : τ ≠ 0) (A : E →L[ℝ] E) (h : ∀ (v : E), obstruction (Q τ) (QDeriv τ ∘SL A) v = 0) : QDeriv τ ∘SL A = 0

theorem PlanarMidpoint.R_tangent_obstruction_zero {τ : E} (hτ : τ ≠ 0) (A : E →L[ℝ] E) (h : ∀ (v : E), obstruction (R τ) (RDeriv τ ∘SL A) v = 0) : RDeriv τ ∘SL A = 0