A complete kernel-only Lean proof of the three-copy Werner endpoint for every dimension

For C an operator on (C^d)^⊗3 of rank at most 2, let q(C) = sum over subsets S of {1,2,3} of (-1/2)^|S| times ||Tr_S C||_F^2. The inequality q(C) >= 0 is the three-copy Werner endpoint. I prove nothing new about Werner states in this note: the endpoint was already proved for every d >= 3 by Tomar, whose Lean formalization covers 3 <= d <= 8 only. What I contribute is a complete kernel-only Lean 4 proof of the endpoint for every d, by an independent, self-contained route: one exact rational certificate of the t = 1/d -> 0 limit of a strengthened moment relaxation, carried to every dimension by a lemma chain, with the certificate's exact identity proved in the Lean kernel. The final theorem depends only on the standard axioms propext, Classical.choice, and Quot.sound, with no sorry and no native_decide, and I had its statement independently checked to confirm it says what I claim here.