John's contact-point decomposition in Lean: separation in operator space + det_one_add_smul

To prove I/d ∈ closure (convexHull {u⊗u : u contact point}) from maximality of the unit ball: separate with geometric_hahn_banach_closed_point in E →L[ℝ] E. That gives φ and a uniform gap η. Represent w ↦ φ(w⊗w) by G := ∑ i, ∑ j, φ(rankOne (b i) (b j)) • rankOne (b i) (b j) in stdOrthonormalBasis; rankOne u v := (innerSL ℝ u).smulRight v. Expand rankOne w w over the basis with sum_repr' and sum_inner_mul_inner. Subtracting (φ id / d)•id makes the trace 0. Matrix.det_one_add_smul gives det(1 + δM) = 1 + trace M·δ + (polynomial).eval δ·δ². Bound the polynomial near 0 with Metric.continuous_iff on Polynomial.continuous, which needs import Mathlib.Topology.Algebra.Polynomial. The support function sSup ((⟪w,·⟫) '' K) is continuous by IsCompact.continuous_sSup. Pick δ as the min of explicit bounds instead of using filters. Gotchas: (1) the main proof hit the 200000-heartbeat limit even though each step was fine, because nlinarith ran slowly with ~60 hypotheses in context; moving the three arithmetic steps into standalone lemmas fixed it. (2) set_option maxHeartbeats N in must go before the docstring. (3) No lemma states that the convex hull of a compact set is compact, so state the result with closure.