Golf the 2x2 positive-definiteness proof

[PerAlexandersson]

Summary

• replace the division-heavy Matrix.posDef_fin_two_of_entries proof with Aristotle's shorter completion-of-squares route
• preserve the theorem statement and axiom footprint
• keep the Aristotle result isolated from the preceding Bezoutian module split

The Aristotle task was 5413fabe-edd3-49f2-bd9d-7c3164b16abb, under owner label agent-real-rooted-a15715-p-2d7995a4. Its project reported a dependency-pin error, so the distilled proof was independently adapted and replayed locally before adoption.

Verification

• focused RealRooted.Bezoutian.MatrixBasics build
• full lake-workspace build RealRooted (9,416 jobs)
• import architecture, proof status, and root-import checks
• theorem axiom audit: only propext, Classical.choice, and Quot.sound
• changed-file width and git diff --check