Recombination Does Not Help: a Kernel-Gated Measurement of Crossover in Program Synthesis, and the Verifier Artifact That Made It Affordable

Crossover is the operator that distinguishes a genetic algorithm from a hill-climber, and in evolutionary program synthesis its contribution is usually asserted rather than measured. Three preceding papers in this programme asked whether recombination is detectable in evolved programs and refuted the question's instrument each time. None asked the prior question: does recombination help? The measurement was unaffordable for a reason that turned out to be ours. A verified answer needs a formal gate over hundreds of candidates, and our gate cost one Lean 4 invocation per candidate. A Lean compile containing a false obligation exits nonzero and still prints a per-declaration axiom line for every candidate, the failing ones carrying sorryAx. Our wrapper discarded those lines the instant the exit code was nonzero, which made a batch appear atomic and motivated three successive rounds of isolation machinery — a bisection, a flat fall-back measured as better than the bisection, and a break-even law (1-p)^b > 1/b derived from the cost of isolating a failure. All three were solving a problem the wrapper had invented. Reading the kernel's own report gives every verdict in one invocation at any failure rate: measured at 1 invocation for 0, 1, 2, 4 and 8 failures of 8, every culprit named, no false candidate accepted. Dropping the exit code is sound because acceptance never rested on it — the forgery scan, a per-declaration axioms line, and a whitelist free of sorryAx are unchanged. Crossover significantly reduces the solve rate. Fitness is exact rational agreement with a specification at sample points, computed outside the proof assistant; acceptance is the Lean kernel, so a wrong fitness can misguide the search but cannot manufacture an acceptance. Over 200 paired seeds on a calibrated target, mutation-only solved 94/200 (47.0%) against crossover's 58/200 (29.0%), Fisher exact p = 2.98×10-4. Conditional on solving, the evaluation count is unchanged (median ratio 0.959 over 35 pairs, sign test p = 1.000). Crossover does not make successful searches faster; it makes success less likely. The mechanism is exact. An expression is affine in any one subtree's value, out = A + B·v, and B is computable in exact rationals by one forward and one backward pass (verified against the defining two evaluations over 500+ address-point pairs). A donor contributing B_donor·v in its own parent contributes B_site·v after transplant, so its contribution is rescaled or sign-inverted whenever the coefficients differ — subtree crossover transmits structure and not function. The repair the mechanism recommends fails, refuted by its own control. Biology recombines at homologous sites, so we restricted recombination to sites whose coefficient sign pattern matches the donor's, with an anti-homologous arm as the negative control and the falsifier fixed in advance. Homologous crossover reached 70/200 (35.0%): not significantly above random crossover (p = 0.238), and significantly below mutation-only (p = 0.019). The anti-homologous control, predicted to be worse, scored higher at 79/200 (39.5%) and is statistically indistinguishable from the treatment (p = 0.408) — exactly the outcome registered in advance as meaning the signature carries nothing. A fallback-to-mutation confound is excluded by counts: effective mutation fractions of 0.5117 and 0.5196 against 0.5000 cannot produce a 10.5 point spread. The ordering of the three crossover arms is left unexplained rather than given a story, since no adjacent pair is significant. What survives is the negative result from five independent directions, the last of them against an idea of our own. In this representation the only operator that reliably works is mutation. What it does not license is also recorded: matching sign(B) failing does not show that no contribution-preserving recombination can work, and a scheme that rescales the donor to preserve B·v is untested and is the obvious next candidate. The failure is reported now rather than after hunting for a variant that wins, because the prediction and its falsifier were fixed before the run. Transferable method: a measured limit reported by code you own is a property of that code until you check it one layer below. Three rounds of optimisation here were spent against a barrier of our own making, and the defect survived an existing guard because the wrapper's output looked like physics rather than like a choice. Scope. One grammar, one calibrated target rung, one budget, one population scheme, one crossover rate. Evidence about crossover in this setting, not a general theorem about recombination. The full specification target was solved by neither arm at this budget, so nothing is established at the size the gate itself cares about. Not peer reviewed.