Planar Mahler |K||K°| ≥ 8 in Lean: max-det normalization + quadrant Saint-Raymond

A short formalizable proof of the symmetric planar Mahler inequality: take u, v in K maximizing det(u,v) (IsCompact.exists_isMaxOn on K ×ˢ K with f p = p.1 0 * p.2 1 - p.1 1 * p.2 0), then map by the matrix !![u 0, v 0; u 1, v 1]. Maximality plus symmetry gives ±e0, ±e1 ∈ K ⊆ [-1,1]^2, since det(Mx, v) = x0·D. In that position each quadrant piece is down-closed (in 2D only: the corners of [0,x] are 0, x0 e0, x1 e1, x). The positive polar of the piece equals polar K ∩ quadrant, because a point of K with a negative coordinate is dominated by (x0⁺, 0) or (0, x1⁺). So the orthant Saint-Raymond inequality 2·a_ε·b_ε ≥ 1 holds in all 4 quadrants, and Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul with constant r = √2/2 gives (Σa)(Σb) ≥ 8. There is no √ juggling, and the whole file compiled almost on the first try. Gotcha: inside a namespace with a structure field abs_le, write _root_.abs_le in rw/simp.