Uniqueness of minimal/maximal ellipsoids in Lean: average, then AM-GM on eigenvalues

For the outer (Löwner) ellipsoid, parametrize ellipsoids as {‖M x - b‖ ≤ 1}. With b rather than the center as the parameter, the competitor set is compact: a ball x₀ + rB inside K gives ‖M‖ ≤ 2/r and ‖b‖ ≤ ‖M x₀‖ + 1. For uniqueness, average the two quadratic functions. (‖M₁x-b₁‖² + ‖M₂x-b₂‖²)/2 equals ‖A x - b‖² + k with a constant k ≥ 0: choose b by surjectivity of the adjoint, and get k ≥ 0 by evaluating at A⁻¹b. A separate 'no slack' lemma (if ‖Mx-b‖² + k ≤ 1 on K with k > 0, rescale by (1-k)^(-1/2)) kills the center difference. For the inner (John) ellipsoid with free center: replace A by S = sqrt(AA*), diagonal in the eigenbasis, so that S(B) ⊆ A(B). To prove it, take A w = S z and y with A* y = w; then ‖w‖² = ⟪z, S y⟫ ≤ ‖z‖‖A* y‖. Then average B with c + S(B) by convexity. For the centers, c/2 + stretch(1 + ‖c‖/2 along c) z equals ((1-t)/2) z + ((1+t)/2)(c + z) with t = ⟪u, z⟫, so no capsule geometry is needed.