check_note.py: exact checks for OWR-17469-002
A. Lemma 2.3(a): unisolvence of the principal lattice U = (Z + 1)/(k + 1) for P_{k-1}
  d = 1: k = 1..10: collocation matrix of size N_k = binom(k-1+d, d) (up to 10) has full rank
  d = 2: k = 1..10: collocation matrix of size N_k = binom(k-1+d, d) (up to 55) has full rank
  d = 3: k = 1..7: collocation matrix of size N_k = binom(k-1+d, d) (up to 84) has full rank
  d = 4: k = 1..6: collocation matrix of size N_k = binom(k-1+d, d) (up to 126) has full rank
  d = 5: k = 1..5: collocation matrix of size N_k = binom(k-1+d, d) (up to 126) has full rank
  d = 6: k = 1..4: collocation matrix of size N_k = binom(k-1+d, d) (up to 84) has full rank
  42 cases checked; 8 negative controls (collinear sets, repeated points) detected as not unisolvent
  (0.6 s)
B. Lemma 2.2: sum_{|c|=m} (m!/c!) y^c = (y_1+...+y_d)^m
  d <= 4, m <= 6: identity holds at all 5628 points of the grids {0..m}^d (a polynomial of degree <= m in each variable vanishing there is 0)
  (0.1 s)
C. Lemma 3.2: the cells of the firewall
  #B = M^d - (M-4L)^d by direct count: 198 triples (d <= 3, M <= 24)
  #B <= 4dLM^(d-1) and 1-(1-4L/M)^d <= 4dL/M: 2610 triples (d <= 6, 4 <= M <= 60, L <= M/4)
  union of the B-cells = {some x_i outside (2δ, 1-2δ)}: 67964 rational points (d = 2, M <= 16)
  transition intervals of eta inside [δ, 2δ] and [1-2δ, 1-δ], disjoint: δ = 1/q, 4 <= q < 200
  (0.5 s)
D. Proposition 3.1(e): M = ceil((2n)^(1/d)) satisfies 2n <= M^d <= 2^(d+1) n
  120000 pairs (d <= 6, n <= 20000)
  (0.1 s)
E. Lemma 5.2: a^2 (1-c^2) - c^2 (D^2 (1-c^2) - (a-D)^2) = (a - D c^2)^2
  identity holds at 770 rational points (degrees 2, 2, 4 in a, D, c; the grid is large enough to prove it)
  (0.0 s)
F. Proposition 6.2: comb tail bound and sum_j 2 w_j <= 1
  j^(-1-δ) >= (j^(-δ) - (j+1)^(-δ))/δ (and the upper companion): 20000 cases (δ = 1, 2, 3 exactly; δ = 1/2 with rational enclosures); 2 c0 (1 + 1/δ) = 1 for c0 = δ/(2(1+δ))
  (0.1 s)
G. Remark 7.1 (not used in any proof): k = d = 1, nodes (2i-1)/(2n): n * int_0^1 dist(x, P) dx
  n * int_0^1 dist(x, P) dx = 1/4 exactly for n = 1..50, hence c_{1,1} <= 1/4 by Proposition 3.1(d)
  (0.1 s)
TOTAL failures: 0   (total time 1.5 s)
