Soundness sampling for Theorem 4 (seed 11; 60 lpv, 13 ncA, 60 ms5, 60 cells)
  Lemma 12: p3 <= p* for the sampled remainder        459 ok, 0 violations
  Lemma 14: E P(Z) < T^-                             3042 ok, 0 violations   smallest margin 4.135e-05
  Lemma 14: E P(Z) <= Theta - h(rho)                 3042 ok, 0 violations   smallest margin 3.269e-08
  Lemma 23 end to end: E F_p(xi)(Z) < T(u)           2890 ok, 0 violations   smallest margin 1.677e-03
  W1 consequence: P(y) > F_V(y)                     36504 ok, 0 violations   smallest margin 3.597e-04
  cells end to end: E|L| < T(u)                        91 ok, 0 violations   smallest margin 5.636e-02
  cells: E P(M1) <= Theta1 - h(rho)                   321 ok, 0 violations   smallest margin 1.474e-05
  cells: R_a(b1 y) < P(y)                            3600 ok, 0 violations   smallest margin 5.258e-05
  cells: Theta1 <= tau (sqrt3 (1-q)^2 - a)            321 ok, 0 violations
  cone: p(xi) = sum nu V, nu >= 0                    2028 ok, 0 violations
  cone: sum nu = lambda <= 1                         2028 ok, 0 violations   smallest margin 1.846e-07
  envelope: F_V(y) <= Phi_V(y)                      36504 ok, 0 violations   smallest margin 6.944e-06
  ncA end to end: E|L| < T(u)                         237 ok, 0 violations   smallest margin 4.023e-02
  ncA: min(1, a2/b) <= mbar(B)                        237 ok, 0 violations
  pieces end to end: E|L| <= T(u)                     448 ok, 0 violations   smallest margin 2.265e-05
  pieces: a_i in its enclosure                       1640 ok, 0 violations
  pieces: eta_j <= |y_j|                             5952 ok, 0 violations
  pieces: p_j <= p_j^+                               5952 ok, 0 violations
  pieces: r' <= r'^+                                  448 ok, 0 violations
  pieces: remainder norm^2 <= (b^2)^+                 448 ok, 0 violations
  pieces: |p_j y_j| <= bound                         5952 ok, 0 violations
  TOTAL violations: 0
