Ran–Teng Conjecture 20: every machine-checkable fragment holds. The analytic core we did not audit — and we say which is which.

A GPT-5.2-claimed resolution of Conjecture 20 of Ran and Teng (ELA 40, 2024) determines the exact nonreal spectral region of a 4-cycle row-stochastic matrix family (arXiv:2602.18918 and its companion arXiv:2605.06743). The claim chain carries no code and no machine certificate — the database’s own line is “no formal proof assistant artifact located”. We re-verified every fragment of the proof a machine can check, in an independent reimplementation on our own exact-rational and certified-interval stack. All of it holds: 43 checks, 0 failures, 5/5 mutation controls rejected, 41 ms. The proof’s analytic core is prose, was not audited, and the verdict is PARTIAL for exactly that reason.

What was verified

For the family A(α,β,γ,δ) with nonreal eigenvalues claimed to fill R = {a+bi ∈ K₄ : a > 0, G(a,b) > 0}, G(a,b) = (b²+a²+a)²+2a²−b²: the characteristic-polynomial identity det(λI−A) = Π(λ−params) − Π(1−params) exactly in ℚ[λ,α,β,γ,δ]; the discriminant factorization Δ = (2a+1)(1−6a) that the referee pass surfaced; the load-bearing factorization |λ|⁶−N = |λ−1|²G; the complete algebra chain of the tight-regime Lemma 4 including both closing margins; and both boundary-attainment families exactly — the diagonal family’s spectrum is exactly {c+(1−c)iᵇ} with the tie a+b₊ = 1 holding with equality, and every nonreal eigenvalue of the A_L(α) family lies on the curve G = 0, re-proved exactly, not numerically.

On top of the exact layer, a falsification-grade certified sweep: 272 deterministic parameter tuples, all 1088 eigenvalues enclosed by 2-D Krawczyk in pairwise-disjoint boxes so that no eigenvalue is unaccounted; all 488 certified-nonreal eigenvalues decide all three necessity conditions PASS with zero undecided — minimum certified G lower bound 2.995e−5, minimum certified 1−(a+|b|) of 3.3e−6. One certified violation here would have refuted the theorem. Conversely, 10 exact rational interior targets are certified attained: Krawczyk proves parameters in (0,1)² whose matrix has the target as an exact eigenvalue. The A_L trace is shadowed numerically too: certified nonreal roots at 9 values of α have interval G straddling 0 at width ≤ 1.6e−12.

The mutation that proves the teeth

Five controls, each rejected. The instructive one is M3: strengthen the claim to strict inequality a+b₊ < 1 and it is rejected by the exact tie — the diagonal family gives a+b₊ = 1 exactly, a boundary case no interval method could decide; only the exact layer kills it. The interval layer has its own teeth: M4, a fake eigenvalue 1e−3 off the C_L curve, is caught with certified G ≤ −9.6e−4, and M5 shows the certifier can refuse — a candidate 0.07 from any root under a 0.02 radius cap is not certified.

What was NOT audited, stated so it cannot be assumed

Where this sits in the lane

The earlier Lane-B notes confirmed computational layers that turned out to hold in full. This unit is the lane meeting a claim whose verification label is “human-checked mathematical proof” with no artifact at all — the machine-checkable fragment turns out to be substantial (all the proof’s algebra, both boundary families, and a certified falsification sweep), and all of it holds. The honest product is the split itself: a reader now knows exactly which sentences of that proof a machine has checked and which still rest on the referees.