convex_hessian() uses wrong criterion for positive semidefiniteness

[mzargham]

Summary

convex_hessian() in symproof/library/convex.py (lines 81–137) claims to prove Hessian positive semidefiniteness (PSD) via Sylvester's criterion, but the implementation is mathematically incorrect.

Problem

The docstring (line 88) says "positive semi-definiteness" and line 92 says "Sylvester's criterion for PSD." The code then checks only leading principal minors with Q.nonnegative (line 130).

This is wrong on two levels:

1. Sylvester's criterion (all leading principal minors > 0) characterises positive definiteness (PD), not PSD.
2. Positive semidefiniteness requires checking that all principal minors (not just leading ones) are ≥ 0 — there are 2ⁿ − 1 of them for an n×n matrix.

The current check (leading principal minors ≥ 0) is neither PD nor PSD. A matrix can have all leading principal minors ≥ 0 yet have a negative non-leading principal minor, meaning it is not PSD. A sealed proof bundle claiming "f is convex" via this function may be mathematically unsound.

Suggested fix directions

• Option A (simplest): Check leading principal minors > 0 (strict). This correctly proves PD → strict convexity. Rename/redocument accordingly.
• Option B: Check all principal minors ≥ 0 (correct for PSD, but exponential in matrix dimension).
• Option C: Use an eigenvalue-based or LDL decomposition approach for PSD.

Files

• symproof/library/convex.py:81-137