==============================================================================================================
1. Exhaustive checks: Thm 1.1, Prop 1.3 (every one-parity S), Thm 1.2 (every B); minima; extremal pairs
==============================================================================================================
[PASS] bitmask r(d) equals a direct pair count, all 2^n patterns, n <= 10
[PASS] r(A) = r(-A) for all 2^n patterns, n <= 16 (justifies the reduced enumeration for n > NFULL)
  n   patterns  max#miss  dist (#missing: #sets up to A->-A)         Prop1.3 Thm1.2  equality set  floor(2n/3)+1  2t+2   time
  1          2         1  {1: 1}                                     True    True            1..1              1     -    0.0s
  2          4         2  {1: 1, 2: 1}                               True    True            1..2              2     2    0.0s
  3          8         2  {1: 3, 2: 1}                               True    True            1..3              3     2    0.0s
  4         16         2  {0: 2, 1: 3, 2: 3}                         True    True            1..3              3     2    0.0s
  5         32         2  {0: 6, 1: 7, 2: 3}                         True    True            1..4              4     4    0.0s
  6         64         2  {0: 16, 1: 11, 2: 5}                       True    True            1..5              5     4    0.0s
  7        128         2  {0: 40, 1: 19, 2: 5}                       True    True            1..5              5     4    0.0s
  8        256         2  {0: 92, 1: 27, 2: 9}                       True    True            1..6              6     6    0.0s
  9        512         2  {0: 204, 1: 43, 2: 9}                      True    True            1..7              7     6    0.0s
 10       1024         2  {0: 432, 1: 67, 2: 13}                     True    True            1..7              7     6    0.0s
 11       2048         2  {0: 912, 1: 99, 2: 13}                     True    True            1..8              8     8    0.0s
 12       4096         2  {0: 1876, 1: 155, 2: 17}                   True    True            1..9              9     8    0.0s
 13       8192         2  {0: 3860, 1: 219, 2: 17}                   True    True            1..9              9     8    0.0s
 14      16384         2  {0: 7834, 1: 335, 2: 23}                   True    True           1..10             10    10    0.0s
 15      32768         2  {0: 15898, 1: 463, 2: 23}                  True    True           1..11             11    10    0.0s
 16      65536         2  {0: 32034, 1: 703, 2: 31}                  True    True           1..11             11    10    0.0s
 17     131072         2  {0: 64546, 1: 959, 2: 31}                  True    True           1..12             12    12    0.0s
 18     262144         2  {0: 129576, 1: 1459, 2: 37}                True    True           1..13             13    12    0.1s
 19     524288         2  {0: 260136, 1: 1971, 2: 37}                True    True           1..13             13    12    0.2s
 20    1048576         2  {0: 521264, 1: 2979, 2: 45}                True    True           1..14             14    14    0.4s
 21    1048576         2  {0: 1044528, 1: 4003, 2: 45}               True    True           1..15             15    14    0.5s
 22    2097152         2  {0: 2091066, 1: 6031, 2: 55}               True    True           1..15             15    14    1.2s
 23    4194304         2  {0: 4186170, 1: 8079, 2: 55}               True    True           1..16             16    16    2.5s
 24    8388608         2  {0: 8376386, 1: 12159, 2: 63}              True    True           1..17             17    16    5.6s
 25   16777216         2  {0: 16760898, 1: 16255, 2: 63}             True    True           1..17             17    16   11.7s
 26   33554432         2  {0: 33529934, 1: 24423, 2: 75}             True    True           1..18             18    18   23.6s
min_A S_m for m = 1..n (exhaustive), for selected n:
   n=10: [0, 0, 1, 2, 4, 6, 9, 13, 19, 27]
        floor((m-1)^2/4): [0, 0, 1, 2, 4, 6, 9, 12, 16, 20]
   n=16: [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 31, 39, 49, 61, 75]
        floor((m-1)^2/4): [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 30, 36, 42, 49, 56]
   n=20: [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 30, 36, 42, 50, 60, 72, 86, 102, 120]
        floor((m-1)^2/4): [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 30, 36, 42, 49, 56, 64, 72, 81, 90]
   n=26: [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 30, 36, 42, 49, 56, 64, 72, 82, 94, 108, 124, 142, 162, 184, 208]
        floor((m-1)^2/4): [0, 0, 1, 2, 4, 6, 9, 12, 16, 20, 25, 30, 36, 42, 49, 56, 64, 72, 81, 90, 100, 110, 121, 132, 144, 156]
[PASS] Thm 1.1 lower bound: at most two d in [1,n] missing, two attained for n >= 2 (n <= 26)
[PASS] Prop 1.3: sum over S of r >= C(|S|,2) for every one-parity S, every signed set (n <= 26)
[PASS] Thm 1.2 lower bound: sum over B of r >= floor((|B|-1)^2/4) for every B, every signed set (n <= 26)
[PASS] equality set {m : min_A S_m = f(m)} is exactly {1, ..., floor(2n/3)+1} for every n <= 26
[PASS] Remark 3.2(2) exhaustively: extremal pairs = rule R, each missed by exactly one set up to sign (2 <= n <= 26)
[section 1 done, 45.8s]
==============================================================================================================
2. Lemma 2.1 (all clauses, incl. identity (1)), Lemma 2.2 (exactly one), charging map of Prop 1.3
==============================================================================================================
[PASS] Lemma 2.1 (every clause, incl. (1)), Lemma 2.2 (exactly one, ranges), charging map: all 2^n patterns, n <= 14  -- 105 (n,d) cases; failures: none
[PASS] the same clauses + Prop 1.3/Thm 1.1/Thm 1.2 on test sets, n in (30, 61, 120, 121)  -- 100 sets; failures: none
[section 2 done, 46.2s]
==============================================================================================================
3. Proposition 3.1 for all n <= 40 and all a with (n-1)/2 <= a <= n-1
==============================================================================================================
[PASS] Prop 3.1 formula = direct count (420 cases (n,a)); the three ranges partition [1,n]  -- formula failures [], partition failures []
[PASS] each of the three counts (a-d)_+, (n-a-d)_+, (d-a-1)_+ in the proof is right; no pair with x<0<y has x-y>0  -- failures []
[PASS] the inequality the proof actually needs, n-a-1 <= a (i.e. n <= 2a+1), holds for every admissible a
[PASS] for a = ceil((n-1)/2)-1 >= 0 the cross count (d-a-1)_+ is wrong for some d (so a >= (n-1)/2 is needed)
[FINDING] the inequality 'n-a <= a' cited at the end of the proof of Prop 3.1 FAILS for 20 admissible cases, exactly a = (n-1)/2 with n odd: [(1, 0), (3, 1), (5, 2), (7, 3), (9, 4), (11, 5)] ... (the formula itself still holds there)
[PASS] the failures of 'n-a <= a' are exactly the cases a = (n-1)/2, n odd
[section 3 done, 46.2s]
==============================================================================================================
4. Equality cases
==============================================================================================================
[PASS] Thm 1.1 equality: A_a misses exactly {a, a+1} for every n/2 <= a <= n-1, 2 <= n <= 40
[PASS] for odd n and a = (n-1)/2, A_a misses only (n+1)/2 (so the hypothesis a >= n/2 of Thm 1.1 is needed)
[PASS] t = floor((n-2)/3), a = n-1-t: (n-1)/2 <= a <= n-1, 2a-n >= t, n-a-1 = t, q = t (2 <= n <= 40)
[PASS] Thm 1.2 equality: for A_(n-1-t), the m smallest r sum to f(m) for every 1 <= m <= min{n, 2t+2} (2 <= n <= 40)
[PASS] min{n, 2t+2} = 2t+2 for every n >= 2 (the 'min' in Thm 1.2 is redundant)
[PASS] in fact a = n-1-t >= n/2 for all n >= 2 (the boundary case a = (n-1)/2 of Sec. 3 is never used)
[PASS] stronger: the same A_(n-1-t) gives equality for every m <= floor(2n/3)+1 (= 2t+3 when n != 2 mod 3)
   n  t  a=n-1-t  2t+2  floor(2n/3)+1  equality range of A_(n-1-t)
   2  0       1     2              2          2
   3  0       2     2              3          3
   4  0       3     2              3          3
   5  1       3     4              4          4
   6  1       4     4              5          5
   7  1       5     4              5          5
   8  2       5     6              6          6
   9  2       6     6              7          7
  10  2       7     6              7          7
  11  3       7     8              8          8
  12  3       8     8              9          9
  13  3       9     8              9          9
  14  4       9    10             10         10
  20  6      13    14             14         14
  21  6      14    14             15         15
  22  6      15    14             15         15
  26  8      17    18             18         18
  40 12      27    26             27         27
[PASS] q-claim for every admissible a with q >= 0 (400 cases): 0..q occur exactly twice (once on [n-a,a], once on [a+1,n]), other values > q, equality for m <= 2q+2
[PASS] family A_a (all admissible a): the set of m with equality is exactly {1, ..., floor(2n/3)+1}, n <= 40
[PASS] exhaustive equality set (Sec. 1) = equality set of the family A_a, for every n <= 26
[FINDING] Remark 3.2(1) says the exhaustive equality range is 'slightly beyond the range covered by the sets A_a'. In fact, for every n <= 26 the two ranges coincide ({1..floor(2n/3)+1}). The exhaustive range exceeds the range PROVED in Thm 1.2 (2t+2) by exactly one when n != 2 (mod 3), i.e. for n in [3, 4, 6, 7, 9, 10, 12, 13, 15, 16, 18, 19, 21, 22, 24, 25], and equals it otherwise.
   ratio (floor(2n/3)+1)/n for n = 20..26: [0.7, 0.714, 0.682, 0.696, 0.708, 0.68, 0.692] (tends to 2/3)
[section 4 done, 46.2s]
==============================================================================================================
5. The remarks after Thm 1.2 and the footnote
==============================================================================================================
[PASS] f(m) >= m^2/8 for 4 <= m <= 10^5 (so |B| >= eps n >= 4 gives >= eps^2 n^2/8); f(m) >= m(m-2)/4 for all m >= 1
[FINDING] m = 3: 8 f(3) = 8 < 9, so the threshold eps n >= 4 is needed for the constant 1/8 as stated
[PASS] f(m) >= m^2/9 for 3 <= m <= 10^5 (so (Q2) holds with constant eps^2/9 for every n > 2/eps)
   eps=0.1  : ceil(eps n) <= 2t+2 for all n in [2, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24995
   eps=0.25 : ceil(eps n) <= 2t+2 for all n in [2, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24998
   eps=0.5  : ceil(eps n) <= 2t+2 for all n in [2, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24999
   eps=0.6  : ceil(eps n) <= 2t+2 for all n in [8, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24999
   eps=0.65 : ceil(eps n) <= 2t+2 for all n in [38, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24999
   eps=0.66 : ceil(eps n) <= 2t+2 for all n in [98, 10^5]; at n=10^5, f(m)/(eps n)^2 = 0.24999
[PASS] eps = 2/3: ceil(2n/3) > 2t+2 exactly when n = 1 (mod 3) (so 'eps < 2/3' is the right hypothesis for the proved range)
[PASS] with the stronger range floor(2n/3)+1 one has ceil(2n/3) <= floor(2n/3)+1 for all n (1/4 sharp also at eps = 2/3)
[PASS] footnote: for n >= 2 the set A_(n-1) misses n-1 and n; for n = 1, r(1) = 0 (so eps n <= 2 allows sum 0)
[section 5 done, 46.3s]
==============================================================================================================
6. Independent 2-colouring solver for Remark 3.2(2) (n <= 64), and cross-check of the recorded outputs
==============================================================================================================
[PASS] 2-colouring solver, 2 <= n <= 64: two differences can be missing together iff rule R; then exactly one set up to sign; agrees with the exhaustive pair lists
   number of extremal sets up to sign, n = 2..64: [1, 1, 3, 3, 5, 5, 9, 9, 13, 13, 17, 17, 23, 23, 31, 31, 37, 37, 45, 45, 55, 55, 63, 63, 75, 75, 87, 87, 95, 95, 111, 111, 127, 127, 139, 139, 157, 157, 173, 173, 185, 185, 205, 205, 227, 227, 243, 243, 263, 263, 287, 287, 305, 305, 329, 329, 357, 357, 373, 373, 403, 403, 435]
[PASS] every single d in [1,n] is missed by some signed set (n <= 40)
[PASS] finder's verify_output.txt (n = 1..20): max #missing and distribution agree with Sec. 1  -- 20 rows parsed
[PASS] first referee's output (n = 1..26): max #missing, distribution and the equality range agree with Sec. 1  -- 26 rows parsed; equality ranges [1, 2, 3, 3, 4, 5, 5, 6, 7, 7, 8, 9, 9, 10, 11, 11, 12, 13, 13, 14, 15, 15, 16, 17, 17, 18]
[PASS] first referee's count of extremal sets (n = 2..64) agrees with the 2-colouring solver here
[PASS] first referee's output: 'ALL CHECKS PASSED: True' is present
[PASS] author's lead_check_output.txt (n = 1..20): all True, and 'equality for m in 1..Y' agrees with Sec. 1  -- 20 rows parsed
[FINDING] lead_check.py has default NMAX = 18 (sys.argv[1] overrides it); the recorded output covers n = 1..20, so it was run with argument 20. Default found in source: True
[section 6 done, 48.2s]
==============================================================================================================
Summary
==============================================================================================================
  PASS  bitmask r(d) equals a direct pair count, all 2^n patterns, n <= 10
  PASS  r(A) = r(-A) for all 2^n patterns, n <= 16 (justifies the reduced enumeration for n > NFULL)
  PASS  Thm 1.1 lower bound: at most two d in [1,n] missing, two attained for n >= 2 (n <= 26)
  PASS  Prop 1.3: sum over S of r >= C(|S|,2) for every one-parity S, every signed set (n <= 26)
  PASS  Thm 1.2 lower bound: sum over B of r >= floor((|B|-1)^2/4) for every B, every signed set (n <= 26)
  PASS  equality set {m : min_A S_m = f(m)} is exactly {1, ..., floor(2n/3)+1} for every n <= 26
  PASS  Remark 3.2(2) exhaustively: extremal pairs = rule R, each missed by exactly one set up to sign (2 <= n <= 26)
  PASS  Lemma 2.1 (every clause, incl. (1)), Lemma 2.2 (exactly one, ranges), charging map: all 2^n patterns, n <= 14
  PASS  the same clauses + Prop 1.3/Thm 1.1/Thm 1.2 on test sets, n in (30, 61, 120, 121)
  PASS  Prop 3.1 formula = direct count (420 cases (n,a)); the three ranges partition [1,n]
  PASS  each of the three counts (a-d)_+, (n-a-d)_+, (d-a-1)_+ in the proof is right; no pair with x<0<y has x-y>0
  PASS  the inequality the proof actually needs, n-a-1 <= a (i.e. n <= 2a+1), holds for every admissible a
  PASS  for a = ceil((n-1)/2)-1 >= 0 the cross count (d-a-1)_+ is wrong for some d (so a >= (n-1)/2 is needed)
  PASS  the failures of 'n-a <= a' are exactly the cases a = (n-1)/2, n odd
  PASS  Thm 1.1 equality: A_a misses exactly {a, a+1} for every n/2 <= a <= n-1, 2 <= n <= 40
  PASS  for odd n and a = (n-1)/2, A_a misses only (n+1)/2 (so the hypothesis a >= n/2 of Thm 1.1 is needed)
  PASS  t = floor((n-2)/3), a = n-1-t: (n-1)/2 <= a <= n-1, 2a-n >= t, n-a-1 = t, q = t (2 <= n <= 40)
  PASS  Thm 1.2 equality: for A_(n-1-t), the m smallest r sum to f(m) for every 1 <= m <= min{n, 2t+2} (2 <= n <= 40)
  PASS  min{n, 2t+2} = 2t+2 for every n >= 2 (the 'min' in Thm 1.2 is redundant)
  PASS  in fact a = n-1-t >= n/2 for all n >= 2 (the boundary case a = (n-1)/2 of Sec. 3 is never used)
  PASS  stronger: the same A_(n-1-t) gives equality for every m <= floor(2n/3)+1 (= 2t+3 when n != 2 mod 3)
  PASS  q-claim for every admissible a with q >= 0 (400 cases): 0..q occur exactly twice (once on [n-a,a], once on [a+1,n]), other values > q, equality for m <= 2q+2
  PASS  family A_a (all admissible a): the set of m with equality is exactly {1, ..., floor(2n/3)+1}, n <= 40
  PASS  exhaustive equality set (Sec. 1) = equality set of the family A_a, for every n <= 26
  PASS  f(m) >= m^2/8 for 4 <= m <= 10^5 (so |B| >= eps n >= 4 gives >= eps^2 n^2/8); f(m) >= m(m-2)/4 for all m >= 1
  PASS  f(m) >= m^2/9 for 3 <= m <= 10^5 (so (Q2) holds with constant eps^2/9 for every n > 2/eps)
  PASS  eps = 2/3: ceil(2n/3) > 2t+2 exactly when n = 1 (mod 3) (so 'eps < 2/3' is the right hypothesis for the proved range)
  PASS  with the stronger range floor(2n/3)+1 one has ceil(2n/3) <= floor(2n/3)+1 for all n (1/4 sharp also at eps = 2/3)
  PASS  footnote: for n >= 2 the set A_(n-1) misses n-1 and n; for n = 1, r(1) = 0 (so eps n <= 2 allows sum 0)
  PASS  2-colouring solver, 2 <= n <= 64: two differences can be missing together iff rule R; then exactly one set up to sign; agrees with the exhaustive pair lists
  PASS  every single d in [1,n] is missed by some signed set (n <= 40)
  PASS  finder's verify_output.txt (n = 1..20): max #missing and distribution agree with Sec. 1
  PASS  first referee's output (n = 1..26): max #missing, distribution and the equality range agree with Sec. 1
  PASS  first referee's count of extremal sets (n = 2..64) agrees with the 2-colouring solver here
  PASS  first referee's output: 'ALL CHECKS PASSED: True' is present
  PASS  author's lead_check_output.txt (n = 1..20): all True, and 'equality for m in 1..Y' agrees with Sec. 1
ALL CHECKS PASSED: True    [total 48.2s]
