r2_exact.py (verification run on the final text, 2026-10-20)
python 3.13.5
1. Lemma 2.3(a): unisolvence of U = (Z+1)/(k+1) for P_{k-1}, 1 <= k, d <= 5
   d=1 k=1: N_k=   1, exact rank 1
   d=1 k=2: N_k=   2, exact rank 2
   d=1 k=3: N_k=   3, exact rank 3
   d=1 k=4: N_k=   4, exact rank 4
   d=1 k=5: N_k=   5, exact rank 5
   d=2 k=1: N_k=   1, exact rank 1
   d=2 k=2: N_k=   3, exact rank 3
   d=2 k=3: N_k=   6, exact rank 6
   d=2 k=4: N_k=  10, exact rank 10
   d=2 k=5: N_k=  15, exact rank 15
   d=3 k=1: N_k=   1, exact rank 1
   d=3 k=2: N_k=   4, exact rank 4
   d=3 k=3: N_k=  10, exact rank 10
   d=3 k=4: N_k=  20, exact rank 20
   d=3 k=5: N_k=  35, exact rank 35
   d=4 k=1: N_k=   1, exact rank 1
   d=4 k=2: N_k=   5, exact rank 5
   d=4 k=3: N_k=  15, exact rank 15
   d=4 k=4: N_k=  35, exact rank 35
   d=4 k=5: N_k=  70, exact rank 70
   d=5 k=1: N_k=   1, exact rank 1
   d=5 k=2: N_k=   6, exact rank 6
   d=5 k=3: N_k=  21, exact rank 21
   d=5 k=4: N_k=  56, exact rank 56
   d=5 k=5: N_k= 126, exact rank 126
   control repeated  d=2 k=2: rank 2 < N_k = 3
   control collinear d=2 k=2: rank 2 < N_k = 3
   control repeated  d=2 k=3: rank 5 < N_k = 6
   control collinear d=2 k=3: rank 3 < N_k = 6
   control repeated  d=3 k=3: rank 9 < N_k = 10
   control collinear d=3 k=3: rank 3 < N_k = 10
   control repeated  d=4 k=2: rank 4 < N_k = 5
   control collinear d=4 k=2: rank 2 < N_k = 5
   control repeated  d=5 k=3: rank 20 < N_k = 21
   control collinear d=5 k=3: rank 3 < N_k = 21
   25 cases full rank; 10 negative controls detected; induction step sets checked for d, k <= 5
   (0.1 s)
2. Lemma 3.2: #B, its bound, and the measure bound
   dynamic-programme count, formula and both bounds: 2610 triples (d <= 6, 4 <= M <= 60, 1 <= L <= M/4)
   direct enumeration agrees: 1365 triples (all with M^d <= 300000)
   (7.8 s)
3. Lemma 2.2: multinomial identity sum_{|c|=m} m!/c! |y|^c = |y|_1^m (symbolic, sympy)
   28 identities (d <= 4, 0 <= m <= 6) hold as polynomial identities
   (0.2 s)
4. Lemma 5.2: cone identity (symbolic) and random tests of B_x in C(x), q_x in B_x
   identity verified symbolically: True
   40000 random points of balls B_x: all in C(x); 4000 random cubes q_x: all in B_x with |x-a|_inf <= Rt
   (0.2 s)
5. Proposition 6.2: comb tail sum_{j>n} j^(-1-delta) >= (n+1)^(-delta)/delta, n <= 1000
   10 values of delta in [1/20, 3], n = 0..1000: all hold (min tail/bound = 1.00002497939)
   2 c0 zeta(1+delta) <= 1 for all these delta (gaps and teeth fit into (0,1))
   (3.5 s)
6. Proposition 3.1(d): sandwich inequality V_N <= ((m+1)/m)^k V_{n0}, exact integer form
   574944 cases (d, k <= 4, n0 <= 12, n0 <= N <= 3000)
   (2.7 s)
TOTAL FAILURES: 0   (14.5 s)
