A Proved Lift That Does Not Transfer: Split-Level Certificates of Non-Tree-Likeness, and Three Mechanisms of Failure

A quartet certificate refutes the four-point condition on four sequences with an exact integer comparison a proof kernel can recheck. It names four sequences; what a biologist reads is a split, one group of sequences against another. This paper promotes the certificate to that level and reports both halves of the result. The formal half succeeds. Because complete deletion gives every quadruple its own denominator, the Bandelt–Dress isolation index — a minimum over straddling quadruples — is unavailable without an incommensurable comparison, so the split certificate is defined as a logical conjunction of per-quadruple integer comparisons. We then prove that two certified incompatible splits force a four-point violation, with the witness quadruple constructed from the four side-intersections rather than searched for. Four theorems; the Lean module is 27/27 declarations with no sorry and no axioms beyond {propext, Classical.choice, Quot.sound}. One of them proves a claim earlier editions asserted in prose. The empirical half fails, and the failures are the contribution. Reaching a working simulated demonstration (20/20 specificity, 15/15 sensitivity over seven populations at five seeds) required three negative controls to fail first: the criterion had no noise floor and fired on a two-count margin in two thousand where an exact tree forces equality; no constant floor can separate, because saturation retains exactly n−3 splits at a floor 64× the one that erases every other dataset; and the matched null was never matched, because the relaxed-clock simulator's divergence at fixed mutation rate has a coefficient of variation near 50% spanning 10–28×, so matching it in expectation is ill-posed however carefully implemented. Rejection sampling on each replicate's realised divergence repairs it. The demonstration then does not transfer. At sixteen taxa on real viral populations the strict conjunction certifies 0, 2 and 4 splits where a tree has 13: every population reads as a tree, so its single agreement with a tree-like prior is vacuous. The mechanism is measured, not inferred — conjuncts for a balanced split number C(n/2,2)^2, which is 36 at n=8 but 784 at n=16, and the closest-missing splits failed by one conjunct out of 91. An exception budget calibrated against the matched null recovers power and does not separate: all three populations, including the only tree-like control, stop reading as trees at a smaller budget than a genuine tree does (−21, −15, −11). Any threshold between 13 and 24 would classify all three correctly, which on three populations with one negative control is fitting a cutoff to the answer, so none is chosen. The binding constraint is not the statistic but the alignment admissibility gate, which leaves three of ten populations usable with a single negative control — and one negative control cannot separate “this method false-positives” from “that population’s prior is wrong”. The next step for this line is more admissible negative controls, not another statistic. A methodological finding has scope beyond this paper: a matched null calibrated on the mean of a nuisance parameter is not matched when the nuisance has a heavy-tailed realised distribution, and averaging more replicates does not repair it — averaging shrinks the standard error of the tuning, not the spread of the replicates the statistic is computed on. The diagnostic is cheap: measure the across-realisation coefficient of variation of the quantity being matched. All figures are produced by committed code and stored artifacts; none is hand-entered. Not peer reviewed.