Documentation

LeanPool.PlanarMidpoint.FiveDirections

Five exact direction tests determine the quartic obstruction at each point.

theorem PlanarMidpoint.obstruction_zero_of_five (c : Coeff) (J : E →L[ℝ] Coeff) (htest : ∀ (j : Fin 5), obstruction c J (vec (↑↑j) 1) = 0) (h : E) :
obstruction c J h = 0

Five fixed directions suffice because each obstruction component is quartic.

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) :
∃ (c : Coeff), ∀ p ∈ Ω, C p = c

Exact tests in the five directions (j,1), at every point of the domain, force a differentiable planar cubic field to be constant.