Exact polynomial certificates for the planar obstruction kernel.

def PlanarMidpoint.Algebra.Kernel (a b c d : ℝ) (z : Fin 8 → ℝ) : Prop

The ten quartic coefficient equations, in immutable derivative order (aₓ,bₓ,cₓ,dₓ,aᵧ,bᵧ,cᵧ,dᵧ).

Equations

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

theorem PlanarMidpoint.Algebra.tracefree_0 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 0 = 0

theorem PlanarMidpoint.Algebra.tracefree_1 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 1 = 0

theorem PlanarMidpoint.Algebra.tracefree_2 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 2 = 0

theorem PlanarMidpoint.Algebra.tracefree_3 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 3 = 0

theorem PlanarMidpoint.Algebra.tracefree_4 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 4 = 0

theorem PlanarMidpoint.Algebra.tracefree_5 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 5 = 0

theorem PlanarMidpoint.Algebra.tracefree_6 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 6 = 0

theorem PlanarMidpoint.Algebra.tracefree_7 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) : (a ^ 2 + b ^ 2) ^ 2 * z 7 = 0

theorem PlanarMidpoint.Algebra.normalized_0 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 0 = 0

theorem PlanarMidpoint.Algebra.normalized_1 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 1 = 0

theorem PlanarMidpoint.Algebra.normalized_2 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 2 = 0

theorem PlanarMidpoint.Algebra.normalized_3 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 3 = 0

theorem PlanarMidpoint.Algebra.normalized_4 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 4 = 0

theorem PlanarMidpoint.Algebra.normalized_5 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 5 = 0

theorem PlanarMidpoint.Algebra.normalized_6 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 6 = 0

theorem PlanarMidpoint.Algebra.normalized_7 (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) : b * z 7 = 0

theorem PlanarMidpoint.Algebra.even_0 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 1 * z 0 = 0

theorem PlanarMidpoint.Algebra.even_1 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 3 * z 1 = 0

theorem PlanarMidpoint.Algebra.even_2 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 1 * z 2 = 0

theorem PlanarMidpoint.Algebra.even_3 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 3 * z 3 = 0

theorem PlanarMidpoint.Algebra.even_4 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 3 * z 4 = 0

theorem PlanarMidpoint.Algebra.even_5 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 1 * z 5 = 0

theorem PlanarMidpoint.Algebra.even_6 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 3 * z 6 = 0

theorem PlanarMidpoint.Algebra.even_7 (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) : a * c ^ 1 * z 7 = 0

theorem PlanarMidpoint.Algebra.tracefree_injective (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (-a) (-b) z) (hab : a ≠ 0 ∨ b ≠ 0) : z = 0

Every nonzero tracefree cubic has injective obstruction matrix.

theorem PlanarMidpoint.Algebra.even_injective (a c : ℝ) (z : Fin 8 → ℝ) (h : Kernel a 0 c 0 z) (ha : a ≠ 0) (hc : c ≠ 0) : z = 0

The even slice has injective obstruction matrix away from its two axes.

theorem PlanarMidpoint.Algebra.normalized_classification (a b : ℝ) (z : Fin 8 → ℝ) (h : Kernel a b (1 - a) (-b) z) (hz : z ≠ 0) : b = 0 ∧ (a = 0 ∨ a = 1)

The trace-normalized slice has exactly the two possible rank exceptions.

theorem PlanarMidpoint.Algebra.pure_kernel (z : Fin 8 → ℝ) (h : Kernel 1 0 0 0 z) (i : Fin 8) : i ≠ 7 → z i = 0

At the pure-cube representative, the kernel has only its final coordinate.

theorem PlanarMidpoint.Algebra.mixed_kernel (z : Fin 8 → ℝ) (h : Kernel 0 0 1 0 z) : z 1 = 0 ∧ z 3 = 0 ∧ z 4 = 0 ∧ z 6 = 0 ∧ z 0 = 2 * z 5 ∧ z 2 = 4 * z 5 ∧ z 7 = -8 * z 5

At the mixed representative, every kernel vector has the stated ratios.

theorem PlanarMidpoint.Algebra.pure_tangent_injective (z : Fin 8 → ℝ) (h : Kernel 1 0 0 0 z) (ht : z 7 = 0) : z = 0

Tangency to the pure-cube graph removes its remaining kernel direction.

theorem PlanarMidpoint.Algebra.mixed_tangent_injective (z : Fin 8 → ℝ) (h : Kernel 0 0 1 0 z) (ht : z 0 = 0) : z = 0

Tangency to the mixed-cube graph removes its remaining kernel direction.