Differential rigidity of planar symmetric cubic fields

On every open preconnected planar domain, an everywhere differentiable cubic field satisfying the quartic obstruction equation is constant. The proof includes the exceptional cones, transitions between loci, and zero values; no continuity of the derivative is assumed.

def PlanarMidpoint.regularLocus : Set Coeff

Values outside the two exceptional graphs.

Equations

• PlanarMidpoint.regularLocus = {c : PlanarMidpoint.Coeff | c ≠ PlanarMidpoint.Q (PlanarMidpoint.trace c) ∧ c ≠ PlanarMidpoint.R (PlanarMidpoint.trace c)}

theorem PlanarMidpoint.isOpen_regularLocus : IsOpen regularLocus

theorem PlanarMidpoint.regular_obstruction_injective {c : Coeff} (hc : c ∈ regularLocus) (J : E →L[ℝ] Coeff) (hJ : ∀ (v : E), obstruction c J v = 0) : J = 0

theorem PlanarMidpoint.planar_obstruction_rigidity (Ω : Set E) (C : E → Coeff) (openΩ : IsOpen Ω) (connectedΩ : IsPreconnected Ω) (diffC : DifferentiableOn ℝ C Ω) (PDE : ∀ p ∈ Ω, ∀ (h : E), obstruction (C p) (fderiv ℝ C p) h = 0) : ∃ (c : Coeff), ∀ p ∈ Ω, C p = c

The quartic obstruction forces a differentiable planar cubic field to be constant on every open preconnected domain.