check_note.py -- EP-963 -- Python 3.13.5
(i) Theorem 1.2, first proof (Section 3.2): the closed tree for N = 7, K = 4
    order-feasible patterns per K-subset for K = 3..7: [1, 6, 26, 98, 344]
  ok    order-feasible pattern counts 1, 6, 26, 98, 344 for K = 3..7 (Lemma 3.2)
    K = 4, a < b < c < d: d=a+b+c, d=a+b, c=a+b, d=a+c, d=b+c, a+d=b+c
  ok    the six order-feasible patterns for K = 4 are c=a+b, d=a+b, d=a+c, d=b+c, d=a+b+c, a+d=b+c
    tree_K4_N7.jsonl: 30 nodes, 29 branches, 151 certificates (explicit multipliers), max depth 4, largest denominator in y: 13  [0.01 s]
  ok    N = 7 tree CLOSED: 30 nodes, 151 certificates -> every 7 positive reals contain a dissociated 4-subset
    example (node 3, case p7=p1+p2+p4): y = (4/7, 2/7, 0, 0, 1/7, 0, 0), v = (2/7, 2/7, 0, -1/7, 1/7, 0, 0), multipliers (-1/7, -2/7, -1/7, 1/7)
  ok    the example certificate of Section 3.2: v = -(1/7)r1 - (2/7)r2 - (1/7)r3 + (1/7)e
  ok    tree_K4_N7_v2nogoods.jsonl CLOSED (56 nodes, 281 certificates)
  ok    tree_K4_N8.jsonl CLOSED (79 nodes, 396 certificates)
  ok    tree_K4_N8_v2nogoods.jsonl CLOSED (65 nodes, 326 certificates)
    tree_K4_N6.jsonl: verdict EXISTENCE; 10 verified solution points, of which (scaled to p_1 = 1) integral: (1,2,3,4,5,6)
  ok    N = 6 tree is not closed; its solution points are exact 6-sets without a dissociated 4-subset, among them {1,...,6} (control)
    corruption 'negative entry in a certificate': REJECTED
    corruption 'certificate entry changed': REJECTED
    corruption 'zero certificate': REJECTED
    corruption 'one case of a split deleted': REJECTED
    corruption 'one case listed twice, another missing': REJECTED
    corruption 'a branch replaced by a false certificate': REJECTED
    corruption 'sign flipped in a node relation': REJECTED
    corruption 'a case that is not order-feasible (a+b = c+d)': REJECTED
    corruption 'Q of a node changed': REJECTED
    corruption 'cases of one node removed (open leaf)': REJECTED
    corruption 'a second, empty list of cases for the root': REJECTED
  ok    all 11 corrupted trees rejected
(ii) Proposition 3.1: the lower bound g+(4) >= 6 and sets without a dissociated 4-subset
    (1, 2, 3, 4): 3 = 1+2; (1, 2, 3, 5): 3 = 1+2; (1, 2, 3, 6): 6 = 1+2+3; (1, 2, 4, 5): 5 = 1+4; (1, 2, 4, 6): 6 = 2+4; (1, 2, 5, 6): 6 = 1+5; (1, 3, 4, 5): 4 = 1+3; (1, 3, 4, 6): 4 = 1+3; (1, 3, 5, 6): 6 = 1+5; (1, 4, 5, 6): 5 = 1+4; (2, 3, 4, 5): 5 = 2+3; (2, 3, 4, 6): 6 = 2+4; (2, 3, 5, 6): 5 = 2+3; (2, 4, 5, 6): 6 = 2+4; (3, 4, 5, 6): 3+6 = 4+5
  ok    {1,...,6}: each of the 15 four-subsets carries a relation
  ok    {1,...,7} contains a dissociated 4-subset, e.g. (3, 5, 6, 7)
    identities: 3 = 1+2; 3 = 1+2; 3 = 1+2; a+1 = 1+a; a+3 = 1+2+a; a+3 = 2+a+1; a+1 = 1+a; a+3 = 3+a; 1+a+3 = 3+a+1; a+1 = 1+a; 2+a+1 = 3+a; a+3 = 3+a; a+3 = 2+a+1; a+3 = 2+a+1; a+3 = 3+a
  ok    {1,2,3,a,a+1,a+3}: every 4-subset carries a relation that holds identically in a (so for every real a > 3 a 6-set without a dissociated 4-subset)
  ok    direct check of {1,2,3,a,a+1,a+3} for a = 4..60
  ok    {0,+-1,...,+-6}: 13 reals without a dissociated 4-subset (so g(4) >= 13, f(13) <= 3)
  ok    {1,2,4} and {3,5,6,7} are maximal dissociated subsets of {1,...,7} (no matroid; Section 4)
(iii) Proposition 5.1: g+(5) >= 13 and g+(6) >= 24, proved by exhibition; intervals
  ok    A* = {1,...,10,12,13,15}: none of its 1287 five-subsets is dissociated (g+(5) >= 13)
  ok    {0} u A* u (-A*): 27 reals, none of the 80730 five-subsets dissociated (g(5) >= 27, f(27) <= 4)  [0.1 s]
  ok    S24 = {1,...,21,24,25,27}: none of the 134596 six-subsets dissociated (g+(6) >= 24)  [0.2 s]
  ok    {1,...,12}: no dissociated 5-subset
  ok    {1,...,13}: dissociated 5-subset (3, 6, 11, 12, 13)
  ok    {1,...,23}: no dissociated 6-subset  [0.1 s]
  ok    {1,...,24}: dissociated 6-subset (11, 17, 20, 22, 23, 24)
(iv) Corollary 1.3: the values of f(n) for n <= 31
  ok    g(1..4) = 1, 3, 7, 13 and g(5) >= 27
    f(n): 1:0 2:1 3:1 4:2 5:2 6:2 7:2 8:3 9:3 10:3 11:3 12:3 13:3 14:4 15:4 16:4 17:4 18:4 19:4 20:4 21:4 22:4 23:4 24:4 25:4 26:4 27:4 28:>=4 29:>=4 30:>=4 31:>=4
  ok    f(n) = 0,1,1,2,2,2,2, 3 (8 <= n <= 13), 4 (14 <= n <= 27); exact for n <= 27 only
  ok    f(n) >= floor(log2 n) for every n <= 31
  ok    first n not covered by the known bounds: 32; f(32) >= 5 iff g(5) <= 31 iff g+(5) <= 15
  ok    g(6) >= 1 + 2*24 = 49, so f(n) <= 5 for n <= 49 (Proposition 5.1(b))
    greedy bound (3^(K-1)-1)/2 for K = 1..5: [0, 1, 4, 13, 40]; needed 2^(K-1)-1: [0, 1, 3, 7, 15]
(v) Theorem 1.2, second proof (Section 3.3): linear forms over a dissociated triple
  ok    13 sign classes in {-1,0,1}^3, 10 of them non-unit; 40 normalized sign vectors on a 4-subset
  ok    N = 5: 45 choices of forms, 588 admissible configurations {'plane': 384, 'line': 180, 'zero': 24}  [0.0 s]; realized and checked directly: 588 of 588, 28 distinct primitive sets, e.g. [(1, 2, 3, 4, 5), (1, 2, 3, 4, 6), (1, 2, 3, 4, 7)]
  ok    N = 6: 120 choices of forms, 1692 admissible configurations {'line': 276, 'plane': 1400, 'zero': 16}  [0.3 s]; realized and checked directly: 1692 of 1692, 21 distinct primitive sets, e.g. [(1, 2, 3, 4, 5, 6), (1, 2, 3, 4, 5, 7), (1, 2, 3, 4, 6, 7)]
  ok    N = 7: 210 choices of forms, 0 admissible configurations {}  [0.8 s] -> no set of 7 positive reals without a dissociated 4-subset
  ok    N = 8: 252 choices of forms, 0 admissible configurations {}  [1.3 s] -> no set of 8 positive reals without a dissociated 4-subset
total time 3.2 s
ALL CHECKS PASSED
