(A) rigorous exclusion of d' via Lemma 1 at the tensor's own scale
   t_min >= 0.979796 ; 3*mu_1 <= 0.307799 ; mu_4 >= 2/5 ; contradiction (3 mu_1 < mu_4): True
(B) distance of target points to the Gram image of the unit ball (tensor multistart) vs to h(P_4)
   d' = (.09,.09,.09,.24) [claimed outside]           ThmA-inside=False  min|G(A)-d| over ball = 2.333e-02   dist to h(P_4) = 2.333e-02
   d* = (.06,.06,.06,.171) [claimed outside]          ThmA-inside=False  min|G(A)-d| over ball = 1.003e-02   dist to h(P_4) = 1.003e-02
   (.09,.09,.09,.21) [claimed boundary point]         ThmA-inside=True  min|G(A)-d| over ball = 7.841e-08   dist to h(P_4) = 1.897e-09
   (.1,.12,.15,.2) [random point, Thm A says inside]  ThmA-inside=True  min|G(A)-d| over ball = 4.421e-15   dist to h(P_4) = 4.198e-09
   (.25,.25,.25,.25) [GHZ-type, inside]               ThmA-inside=True  min|G(A)-d| over ball = 4.244e-09   dist to h(P_4) = 5.765e-09
(C) maximise f(d_4) - f(d_1) - f(d_2) - f(d_3) over the unit sphere (n=4), multistart
   max polygon violation found = 1.027e-14 (Theorem A predicts <= 0)
(D) Lemma 1 proof chain on random tensors, n = 3..6
   n=3: max(mu1 - u'G1u) = 4.4e-16, max(u'G1u - tail) = 4.5e-16, max(tail - sum mu_j) = 8.9e-16 (all should be <= ~1e-15)
   n=4: max(mu1 - u'G1u) = 1.1e-16, max(u'G1u - tail) = 4.4e-16, max(tail - sum mu_j) = 2.6e-16 (all should be <= ~1e-15)
   n=5: max(mu1 - u'G1u) = 0.0e+00, max(u'G1u - tail) = 0.0e+00, max(tail - sum mu_j) = -1.4e-16 (all should be <= ~1e-15)
   n=6: max(mu1 - u'G1u) = 0.0e+00, max(u'G1u - tail) = -2.0e-01, max(tail - sum mu_j) = -1.1e+00 (all should be <= ~1e-15)
