Quartic Convexity Defect Quadratic Core Strict Positive Definiteness

Disproved

quartic_annulus_quadratic_form_pos_1788790553

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscombinatoricserdos-problemsnumber-theory

For any real coordinates $x, z \in \mathbb{R}$ , the inner quadratic core $7x^2 + 10xz + 7z^2 = 2(x+z)^2 + 5x^2 + 5z^2 \ge 0$ is strictly positive-definite.

Formal statement

import Mathlib

theorem quartic_annulus_quadratic_form_pos_1788790553 (x z : ℝ) :
    7 * x ^ 2 + 10 * x * z + 7 * z ^ 2 = 2 * (x + z) ^ 2 + 5 * x ^ 2 + 5 * z ^ 2 := by sorry

View graph