Proof-Carrying Detection of Reticulate Evolution: a Tree-Level Null, the Measured Cost of the Alignment Step, and the Gromov Hinge of Buneman's Converse

Not peer reviewed. This repository once described work as “5-round Opus peer reviewed” on the basis of a function that made no model call; that description was withdrawn and no equivalent claim is made here. Tests for recombination are normally calibrated against a permutation ensemble. This paper develops one calibrated against a theorem, reports the two ways its own first version was wrong, and gives the measurement we believe is new. The null is a theorem. A strict molecular clock on a clonal genealogy makes expected p-distances ultrametric, and an ultrametric admits no unfilled Vietoris–Rips cycle at any scale, so three sequences violating the strong triangle inequality are a certificate rather than a surprise relative to shuffles. The inference rule is formalised in Lean 4, and emitted certificates embed the aligned rows so the kernel recomputes every count itself. That statistic is nonetheless the wrong one. On a clonal tree with a relaxed clock and no reticulation whatever, divergence-matched so only the clock differs, the ultrametric margin exceeds every single-recombinant margin; at 32 leaves min(no reticulation) = 99/4000 > 79/4000 = max(one recombinant) at every seed. The four-point condition encodes tree without clock; we prove in Lean that every symmetric ultrametric satisfies it, and the quartet margin on the same data does not move. The main empirical contribution is about the alignment step. Running the test on real data required writing an aligner, which puts a step on the trust surface that no downstream proof covers. Measured on simulated populations with no reticulation and a known true alignment, reference-anchored alignment manufactures 0 of 9100 four-point violations at a 0.4% gap load and 1600 of 9100 at 8.2%. We found no published benchmark that varies alignment quality as an independent variable, so we believe this is the first direct measurement of a mechanism the field already asserts — confirmatory but novel. Read as an admissibility threshold it refuses 7 of 10 real viral populations; the 3 that pass agree with a literature prior fixed in advance, and the two certificates clearing their matched floor are kernel-accepted with both corrupted twins rejected. Two corrections to our own apparatus are reported as results. The band-edge test by which the aligner had been certified is not a soundness certificate and had really failed — a pair scoring 16555 against an unbanded optimum of 17275 with the band edge never touched. Certifying every alignment against the unbanded optimum dropped the figure above from 4876 to 1600: two thirds of the headline was an uncertified step inside the measuring apparatus, inflating the result in the favourable direction. Separately, the reported statistic is a maximum over subsets where the established treelikeness tests are averages; run seed-paired against the hard null, the maximum separates 16.57x against 5.07x for mean delta_q and 1.22x for the proportion of violating quadruples. New in edition 2. The head-to-head edition 1 listed as its chief limitation has been run, against the one incumbent whose null also assumes no clock. On the five populations where both tests can be measured they agree exactly: both specific on the strict-clock and the relaxed-clock null, both detecting all three reticulate populations at every seed. The incumbent is not beaten on power, so the paper's claims are revised — the case rests on an exhibitable witness and on the absence of a permutation null, not on power. Two asymmetries are reported, one each way: the incumbent needs no recalibration when divergence changes, and it returns no measurement at all on gap-blocked data. A new theorem. The hinge of Buneman's converse, which this programme had only cited, is proved: a symmetric dissimilarity satisfies the four-point condition if and only if its Gromov product satisfies the max inequality at every root. We found no formalisation of tree metrics, splits or Buneman's theorem in Lean, Isabelle or Coq. All Lean declarations compile with zero sorry and no axioms beyond {propext, Classical.choice, Quot.sound}. Bundle. The PDF and LaTeX source, the Lean 4 modules, and the raw JSON output and data provenance behind every number, so the claims can be checked or disputed without trusting this description. Repository: SocrateAI-Scientific-Genetic.