Five exact direction tests determine the quartic obstruction at each point.
theorem
PlanarMidpoint.planar_five_direction_rigidity
(Ω : Set E)
(C : E → Coeff)
(openΩ : IsOpen Ω)
(connectedΩ : IsPreconnected Ω)
(diffC : DifferentiableOn ℝ C Ω)
(tests : ∀ p ∈ Ω, ∀ (j : Fin 5), obstruction (C p) (fderiv ℝ C p) (vec (↑↑j) 1) = 0)
:
Exact tests in the five directions (j,1), at every point of the domain,
force a differentiable planar cubic field to be constant.