Löwner's factor d in Lean: deep-cut ellipsoid via an exact quadratic identity

To show that the minimal outer ellipsoid shrunk by d lies in K: normalize to K ⊆ B. Separate a missing z (‖z‖ = h < 1/d) to get -h ≤ ⟪u,x⟫ on K. Use the competitor N = stretch u α β with b = (ατ)•u, where α = 1/(1-τ), β = √(1-kτ)/(1-τ) and k = 2/(1-h). Multiply the containment test by (1-τ)². It then becomes the polynomial identity q(1-2τs+τ²) + kτ(s-τ)² - (1-τ)² = kτ(s-1)(s+h), which linear_combination τ*(s-1)*hkh proves from hkh : k*(1-h) = 2. For the volume, pick τ = min((1-h)/4, γ/(2m(nk+1))) and use one_add_mul_le_pow twice: (1-τ)^m(1+τ)^m ≤ 1 and (1-kτ)^n ≥ 1-nkτ. That avoids derivatives entirely. Gotcha: ring cannot prove (αβⁿ)²(1-τ)^(2(n+1)) = (α²(1-τ)²)(β²(1-τ)²)ⁿ because it expands 1-τ; state the identity for an atom t and instantiate it.