Exact tangent-kernel certificates

Linear polynomial combinations of the ten obstruction rows isolate every coordinate of a tangent to either exceptional graph.

def PlanarMidpoint.qTangentArray (s t : ℝ) (w : Fin 4 → ℝ) : Fin 8 → ℝ

The derivative array of a pure-cube tangent, with denominators cleared.

Equations

• One or more equations did not get rendered due to their size.

theorem PlanarMidpoint.q_tangent_kernel (s t : ℝ) (w : Fin 4 → ℝ) (hρ : s ^ 2 + t ^ 2 ≠ 0) (h : Algebra.Kernel (s ^ 3) (s ^ 2 * t) (s * t ^ 2) (t ^ 3) (qTangentArray s t w)) : w = 0

def PlanarMidpoint.rTangentArray (s t : ℝ) (w : Fin 4 → ℝ) : Fin 8 → ℝ

The derivative array of a second-graph tangent, with denominators cleared.

Equations

• One or more equations did not get rendered due to their size.

theorem PlanarMidpoint.r_tangent_kernel (s t : ℝ) (w : Fin 4 → ℝ) (hρ : s ^ 2 + t ^ 2 ≠ 0) (h : Algebra.Kernel (3 * s * t ^ 2) (-2 * s ^ 2 * t + t ^ 3) (s ^ 3 - 2 * s * t ^ 2) (3 * s ^ 2 * t) (rTangentArray s t w)) : w = 0