cert-machine · one of six · re-verified from the manuscript

Ran–Teng Conjecture 20

Resolved, in a preprint. Source status: "Human-checked mathematical proof; no formal proof assistant artifact located" (24 Feb 2026). The exact nonreal spectral region for a family of structured matrices — a conjecture in matrix analysis.

tl;dr

The finding. PARTIAL — machine-checkable fragment only. Every machine-checkable fragment of this claim holds; the argument that carries the theorem does not reduce to arithmetic and was not audited.
The mechanism. Written against the manuscript. The author's code was never executed. Verification that existed at source: Human-checked prose. No artifact of any kind was located.
Check it. node legacy/research/challenges/lane/laneb-ranteng/verify.js — 72 ms at this build, 38 named checks and 5 mutation controls, every control rejected.

verdict

PARTIAL

machine-checkable fragment only

named checks

each one printed by the verifier at this build and listed on this page

the verifier's own total

its total folds the 5 mutation controls in; ours does not

mutation controls

deliberate corruptions of the claim — every one rejected, or this page would not build

runtime

72 ms

plain Node, no packages, no author code

analytic core

not audited

true of all six claims in this set, and the reason the flagship exists

§1 · at source

What was claimed, by whom, and what checking already existed

field	as recorded at source
the claim	Resolved, in a preprint. Source status: "Human-checked mathematical proof; no formal proof assistant artifact located" (24 Feb 2026).
the problem	The exact nonreal spectral region for a family of structured matrices — a conjecture in matrix analysis.
credited AI system	GPT-5.2 Thinking
verification at source	Human-checked prose. No artifact of any kind was located.
our verdict	PARTIAL machine-checkable fragment only

§2 · what we certified

The ledger, as the verifier printed it at this build

Every load-bearing polynomial identity of the proof, exactly over ℚ. Both boundary-attainment families re-proved exactly, including an exact re-proof that every nonreal eigenvalue of the A_L family lies ON the conjectured curve. Certified eigenvalue enclosures over 272 exact matrices found zero counterexamples to the necessity conditions, and attainment is Krawczyk-certified at 10 interior points.

The verifier organises its own run into 8 stages. This is that structure, counted at build time — not a summary written by hand.

	[1] Exact: det(lambda*I - A) = prod(lambda-params) - prod(1-params) in Q[l,a,b,g,d]
1	det(lI-A) = (l-a)(l-b)(l-g)(l-d) - (1-a)(1-b)(1-g)(1-d) [eq:multconstraint basis]

	[2] Exact: quadratic-in-s bookkeeping and discriminant of G
1	G = s² + (2a²+2a-1)s + (a²+a)² + 2a² [2605.06743, quadratic-in-s form]
2	discriminant = 1 - 4a - 12a²
3	1 - 4a - 12a² = (2a+1)(1-6a)
4	1 - 4a - 12a² = -12(a - 1/6)(a + 1/2) => Delta >= 0 iff -1/2 <= a <= 1/6 [obligation (i)]
5	G = (s - (1-2a-2a²)/2)² - Delta/4 (root formula for s_± is exactly this square)

	[3] Exact: \|lambda\|^6 - N(a,b) = \|lambda-1\|^2 G(a,b) [Version 3, 11.2 Step 6]
1	N = (1-4a)b² + a²(4a-3) [eq:Ndef-v2]
2	(a²+b²)³ - N(a,b) = ((a-1)²+b²) · G(a,b)
3	G(b²=r-a²) = r² + (2a-1)r + 4a²
4	r³ - N = (r + 1 - 2a) (r² + (2a-1)r + 4a²)

	[4] Exact: every expansion in Lemma 4 (tight-regime lemma, Version 3)
1	(1-2a-8a²)² = 1 - 4a - 12a² + 32a³ + 64a⁴
2	(1-2a-8a²)² - (2a+1)(1-6a) = 32a³ + 64a⁴ > 0 for a > 0 [eq:sminusGT3a2 => b² > 3a²]
3	(1-4a)(1-2a-2a²) = 1 - 6a + 6a² + 8a³
4	(1-4a)²(1-4a-12a²) = 1 - 12a + 36a² + 32a³ - 192a⁴
5	(1-6a+16a³)² - (1-4a)²(2a+1)(1-6a) = 256a⁶ > 0 for a > 0 [eq:squareCompare]
6	(1-a)(b²-3a²) - a(3b²-a²) = N(a,b) [Step 5 cross-multiplication]
7	3b(a²+b²) - 4b³ = b(3a²-b²) [sin 3m numerator, eq:cscUcotU]
8	4a³ - 3a(a²+b²) = a(a²-3b²) [cos 3m numerator, eq:cscUcotU]
9	-a(a²-3b²) + (1-a)(3a²-b²) = -N(a,b) [11.2 Step 5 denominator]
10	a²(3-4a) = 3a² - 4a³ [eq:s0def numerator]

	[5] Exact: boundary attainment families C_R and C_L
1	(l-c)⁴ - (1-c)⁴ = prod_k (l - (c+(1-c)i^k)) => diagonal spectrum is exactly {c+(1-c)i^k}
2	C_R: a + b_+ = c + (1-c) = 1 exactly — condition (2) holds with EQUALITY (a tie only exact arithmetic decides)
3	C_R: (ix)⁴ - x⁴ = 0, so λ = 1-x+ix is an eigenvalue of A(1-x,1-x,1-x,1-x)
4	p_L(l) = (l-al) l³ - (1-al) = l⁴ - al·l³ - (1-al) [char poly of A_L, via [1] at be=ga=de=0]
5	p_L = (l-1)(l³ + (1-al)(l²+l+1)) — 1 is always an eigenvalue
6	p_L = (l³-1)(l-al) + (l-1) — a nonreal root never has l³ = 1
7	Im[(1-l⁴)(1-conj(l)³)] = b((a²+b²)³ - N) = b\|l-1\|²G [with [3]: real al forces G(a,b)=0]
8	G(0,1) = 0 exactly — the endpoint i (attained by A_L(0): i³+i²+i+1 = 0)
9	l³+l²+l+1 vanishes at l = i exactly
10	G(1/6, sqrt(11)/6) = 0 exactly [2605.06743's own curve point]

	[6] Certified sweep: all eigenvalues of ~270 exact 4-cycle matrices enclosed (Krawczyk),
1	all 1088 Krawczyk certifications succeeded (272 matrices x 4 roots)
2	every matrix: 4 pairwise-disjoint certified boxes — every eigenvalue is accounted for
3	zero certified violations (a violation here would REFUTE the theorem)
4	zero undecided condition checks (488 certified-nonreal eigenvalues, 600 real)
5	min certified G lower bound = 2.995e-5 (near-A_L eps=1e-4 probes the boundary; still strictly positive)

	[7] Certified: A_L(alpha) nonreal eigenvalues sit on G = 0 (shadow of the exact result [5])
1	9 alphas in [0,1): certified nonreal root has interval G straddling 0, max width 1.64e-12

	[8] Certified converse witnesses: interior targets lambda = a+ib attained EXACTLY
1	all 10 targets are exact-rational interior points (b>0, a>=0, a+b<1, G>0 — checked in exact arithmetic)
2	all 10 targets: Krawczyk-certified real (t,s) in (0,1)² with (z+t)³(z+s) = t³s => lambda is EXACTLY an eigenvalue

§3 · the falsifiers

Proof that this verifier can fail

A verifier that cannot reject a false claim is not evidence, it is decoration. So each one carries mutation controls: the claim is deliberately corrupted and the verifier must refuse it. All 5 were rejected in the run that built this page, and a control that stopped firing would refuse the page instead.

	the corruption, and how it was caught
1	M1 (matrix entry 1-d -> d): characteristic-polynomial identity REJECTED
2	M2 (G sign flip, -b² -> +b²): factorization identity REJECTED and flipped G on A_L root = [1.324653, 1.324653] no longer straddles 0
3	M3 (claim a+b_+ < 1 strict): REJECTED — diagonal family gives a+b_+ = 1 exactly (tie, sign = 0)
4	M4 (fake eigenvalue, b -= 1e-3 off the C_L curve): certified G <= -9.607e-4 < 0 — REJECTED
5	M5 (candidate 0.07 away from any root, radius cap 0.02): Krawczyk REFUSES to certify

§4 · the boundary

What this audit did NOT reach

not audited

The analytic core — the argument parametrization, the convexity/Jensen/Karamata optimization that makes necessity hold for ALL parameters, and the branch bookkeeping. It is prose. This is why the verdict is PARTIAL and not CONFIRMED.

This is the part worth reading twice. The verdict at the top of this page is true inside its scope line and false outside it, and the sentence above is where the scope line comes from. Across all six claims in this set the same split appears: the computational fragment certifies and the analytic core does not — the flagship page measures exactly that.

§5 · re-run it

One command, no dependencies

git clone https://github.com/carlostoledo1891/cert-machine
cd cert-machine
node legacy/research/challenges/lane/laneb-ranteng/verify.js

Plain Node, no packages. It prints the ledger above, runs its own falsifiers, and exits non-zero if anything fails. node instruments/laneaudit/audit.js runs all six.

CONFIRMED · 17 checksMaxwell's point-charge boundFive positive point charges in ℝ³ whose potential has at least 24 nondegenerate critical points — exceeding the conjectured bound of 16.at ε = 1/6 only CONFIRMED · 15 checksThe Korenblum constantc₂ ≥ 0.4263, via a moment-duality criterion and an explicit rational eight-atom measure (arXiv:2607.17748).the numerical criterion CONFIRMED · 22 checksErdős Problem #1038The infimum is exactly D = 1.834430475762661711090753635125…, in a July 2026 manuscript of Darvas, Peng and Tao.the computational fragment CONFIRMEDThe Mathieu property for Lie groupsExactly the tori — a classification.supporting identities only CONFIRMEDThe rank-two Poisson conjectureAn explicit counterexample: polynomials R, T, D, S in ℚ[x,q,p,z] with prescribed bracket relations.the explicit counterexample