check_note.py: exact checks for the note on OWR-723-005 (Python 3.13.5)
== Part A: phi_alpha(S)
PASS  Lemma 2.2(d): phi_alpha(S) = alpha/(alpha+|S|) for |S| <= 2 (12 sets x alpha = 1..6, from the definition)
PASS  Proposition 4.1(a): phi_alpha({0,1,2}) = (alpha^2 + 1 - 2^-alpha)/((alpha+1)(alpha+2)), alpha = 1..8
PASS  Proposition 4.1(a): alpha/(alpha+3) - phi_alpha({0,1,2}) is 0 for alpha = 1 and > 0 for alpha = 2..12
PASS  Proposition 4.1: phi_1({0,1,2}) = 1/4
PASS  Proposition 4.1: phi_2({0,1,2}) = 19/48
PASS  Proposition 4.1: phi_1({0,1,3}) = 1/4
PASS  Proposition 4.1: phi_2({0,1,3}) = 517/1296
PASS  Proposition 4.1: phi_1({0,1,2,3}) = 11/54
PASS  Proposition 4.1: phi_1({0,1,2,4}) = 85/432
PASS  Lemma 2.3 (gap formula) = definition, and Lemma 2.2(c) invariances, on 40 random (S, alpha)
PASS  Remark 4.2(a): phi_1(S) = 1/4 for all 105 triples {0 < a < b <= 15}
== Part B: direct integration, expansion, binomial formula
PASS  Lemma 2.1 = grid-cell integration on 30 random rational point sets (d <= 3, n <= 4, p in {2,4,6})
      (direct integrations done in 0.6 s)
PASS  direct integration (no Lemma 2.1-2.3) = expansion with phi from the definition, 17 cases (d = 1, 2)
PASS  E_iid: binomial formula = expansion with alpha/(alpha+k) (n <= 5, d <= 3, p in {2,4,6})
== Part C: Theorems 1.1 and 1.2
PASS  Theorem 1.1(i): E_lat(n,d,2) = E_iid(n,d,2) = (2^-d - 3^-d)/n (n <= 5, d in {1,2,3,5})
PASS  Theorem 1.1(ii): E_lat = E_iid for n in {1,2} (d <= 3, p in {4,6,8})
PASS  Theorem 1.1 by direct integration (n = 2; and n = 3, d = 2, p = 2)
PASS  counterexample n=3, d=1, p=4: E_lat = 19/1620 = 19/1620, E_iid = 4/405 = 16/1620, E_lat > E_iid
PASS  Theorem 1.2: E_lat(3,d,4) - E_iid(3,d,4) = (8/9) 2^-d [(2/5)^d - (19/48)^d] > 0, d = 1..12
PASS  Theorem 1.2: n = 4 closed form, > 0, d = 1..12
PASS  Theorem 1.2: E_iid(n,d,4) = n^-3 [(2^-d - 3^-d) + 3(n-2)(3^-d - 2 4^-d + 5^-d)] (n <= 10, d <= 8)
PASS  Theorem 1.2 by direct integration: d = 2 (n = 3, 4) and the values 6829/777600, 391/48600, 139/17280, 99/17280
PASS  values of Table 2 (d = 1: p = 4, n = 5..8; n = 3, p = 6, 8, 10; d = 2: n = 4), direct integration
== Part D: Theorem 1.3
PASS  T_p = {2: 1, 4: 4, 6: 41, 8: 715, 10: 17722} (recursion), = brute force for p <= 8, T_p <= (p/2)^p
PASS  Theorem 5.1: E_lat >= 4/((p+1)^d (p+2)(p+3)(n-1)) on all directly computed cases with n >= 3
PASS  Proposition 5.2: E_iid <= T_p (2^-d - 3^-d) n^(-p/2) (p <= 8, d <= 4, n <= 15)
      N(d,4) for d = 1, 2, 3, 5, 10: [35, 146, 462, 3562, 393598]
      N(d,6) for d = 1, 2, 3, 5, 10: [30, 71, 150, 581, 14144]
      N(d,8) for d = 1, 2, 3, 5, 10: [31, 61, 109, 316, 4037]
      N(d,10) for d = 1, 2, 3, 5, 10: [34, 59, 95, 235, 2037]
PASS  Theorem 1.3: the values of N(d,p) quoted in Remark 5.3
PASS  Remark 5.3: E_lat(3,1,p) / bound of Theorem 5.1 = 1.2315, 1.0895, 1.0371, 1.0160 (p = 4..10), 1.000005 (p = 30)
PASS  Remark 5.3: n E_lat(n,1,4) = 0.02875 (n = 10), 0.02813 (n = 20), direct integration; quoted 0.02875, 0.02813; E_lat(10,1,4) = 1825939/635040000
== Part E: Theorem 1.4 (threshold certificates)
PASS  (p,d) = (4,1): deg n^p E_iid = 2 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 4 (Table 1: 4); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 65) reach n_0 - 1
PASS  (p,d) = (4,2): deg n^p E_iid = 2 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 20 (Table 1: 20); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 65) reach n_0 - 1
PASS  (p,d) = (4,3): deg n^p E_iid = 2 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 54 (Table 1: 54); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 65) reach n_0 - 1
PASS  (p,d) = (4,4): deg n^p E_iid = 2 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 121 (Table 1: 121); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 120) reach n_0 - 1
PASS  (p,d) = (6,1): deg n^p E_iid = 3 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 3 (Table 1: 3); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 25) reach n_0 - 1
PASS  (p,d) = (6,2): deg n^p E_iid = 3 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 8 (Table 1: 8); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 25) reach n_0 - 1
PASS  (p,d) = (6,3): deg n^p E_iid = 3 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 16 (Table 1: 16); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 25) reach n_0 - 1
PASS  (p,d) = (6,4): deg n^p E_iid = 3 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 26 (Table 1: 26); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 25) reach n_0 - 1
PASS  (p,d) = (8,1): deg n^p E_iid = 4 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 3 (Table 1: 3); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 10) reach n_0 - 1
PASS  (p,d) = (8,2): deg n^p E_iid = 4 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 6 (Table 1: 6); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 10) reach n_0 - 1
PASS  (p,d) = (8,3): deg n^p E_iid = 4 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 11 (Table 1: 11); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 10) reach n_0 - 1
PASS  (p,d) = (10,1): deg n^p E_iid = 5 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 3 (Table 1: 3); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 6) reach n_0 - 1
PASS  (p,d) = (10,2): deg n^p E_iid = 5 <= p/2; P(n_0 + t) has nonnegative coefficients for n_0 = 5 (Table 1: 5); P(n_0 - 1) <= 0 or n_0 = 3; the recorded exact computations (n <= 6) reach n_0 - 1
PASS  (p,d) = (4,5): the certificate gives n_0 = 245 (Section 6: 245); P(n_0 - 1) <= 0
PASS  (p,d) = (4,6): the certificate gives n_0 = 469 (Section 6: 469); P(n_0 - 1) <= 0
PASS  Section 6, (p,d) = (4,1): E_iid(n,1,4) = (3n-1)/(30 n^3); L(n) - E_iid(n) = f(n)/(210 n^3 (n-1)), f = 4n^3 - 21n^2 + 28n - 7, f(3) = -4, f(4) = 25
PASS  Section 6, (p,d) = (6,1): E_iid(n,1,6) = (9n^2-8n+2)/(84 n^5); L(n) - E_iid(n) = g(n)/(252 n^5 (n-1)), g = 2n^5 - 27n^3 + 51n^2 - 30n + 6, g(3) = 132
== Part F: negative controls (each wrong input must be detected)
PASS  detected: phi_2({0,1,2}) := 2/5 makes E_lat(3,1,4) = E_iid(3,1,4) (no strict inequality)
PASS  detected: the expansion with +1/n instead of -1/n differs from the direct value at n = 3
PASS  detected: the direct integration with A/(n+1) instead of A/n differs at n = 3
PASS  detected: Theorem 1.2 with 20/48 instead of 19/48 does not match (d = 1)
PASS  detected: twice the bound of Theorem 5.1 exceeds E_lat(3,1,4)
PASS  detected: Proposition 5.2 with T_4/8 is violated (d = 1, some n <= 12)
PASS  detected: the threshold certificate fails at n_0 - 1 = 19 for (p,d) = (4,2)
running time 12.8 s
TOTAL failures: 0
