Research note — not peer-reviewed. Pilot #2 of the independent-verification lane, re-verified with checks proven able to fail. No contact with the claim's author or the database maintainer has been made — that, like every send, is an owner action.

Lane B pilot #2 · AI-claimed results · challenges · 2026-08-03

The identities under the Mathieu–Zhao classification hold exactly. The theorem above them is still unchecked.

An AI-assisted manuscript claims that for a compact connected Lie group G, the kernel of Haar integration is a Mathieu–Zhao space exactly when G is a torus. Its public record is author-side only: an author-checked manuscript plus an author-run SymPy identity verifier. We re-verified the manuscript’s computational supporting identities independently — our own BigInt-rational multivariate Laurent-polynomial arithmetic (including ℚ[i] for the square-root-free substitution), written without executing the author’s script. All 126 checks hold exactly; 3/3 planted mutations are rejected.

Verdict · node verify.js · exit 0 · 0.04 s · no dependencies

Verdict

CONFIRMED (supporting identities only)

Exact checks

126 / 126

Abelian pair

U·V + T² − 1 ≡ 0, exact

Pascal-row moments

m ≤ 5, all rows; Hopf coefficient to m = 8

Mutation controls

3 / 3 rejected

Source pinned

commit 7573e57

The load-bearing distinction, stated up front: what is confirmed is the manuscript’s computational layer — the finite identity checks its own verifier covers. The classification theorem (general-m extensions, the representation-theoretic transfer, orbit averaging on S³, the Duistermaat–van der Kallen torus direction) is mathematics we did not audit, and this page never says otherwise.

What was verified

With the manuscript’s conventions (Laurent constant term CT_w; Haar moment 2∫₀¹CT_w(·)·x dx; c_m = ∫₀¹(1−t²)^mdt): the weighted xz(1,1) witness moments m = 1…6; the abelian pair U, V, T, P with its printed expansion, w-spectrum {−1,0,1,2} and the relations U·V + T² − 1 = 0 and U·P; torus-scaling invariance of all six matrix-entry representatives and the square-root-free B(x,w) reparametrization; the Pascal-row moment identity 2∫CT_w(Q^sP^m)x dx = c_m·C(m−1,s−1) for m ≤ 5, all admissible s; the reduced Hopf coefficient identity through m = 8; and the closed form c_m = 4^m(m!)²/(2m+1)!. Mutations — a perturbed coefficient, a sign flip in T, a wrong Pascal row — are all caught.

What was not verified, stated so it cannot be assumed

The theorem. The verifier — the author’s and ours alike — checks finite supporting identities, not the classification. The general-m extension of every spot check, the representation-theoretic transfer (orbit averaging, highest-weight construction, central-quotient descent, adjoint pullback), the reduction of Haar integration to a constant term, and positivity outside the checked ranges are all unaudited mathematics. The formulation. Our implementation and the author’s share the manuscript’s definitions; an error identical in both would pass — the same transcription-gate caveat as pilot #1.

Where this sits in the lane

Pilot #1 (the rank-two Poisson counterexample) and pilot #2 are the two “bankers”: fast, fully exact, decisive on their computational layer. The flagship — re-deriving the Korenblum-constant Arb certificate in our own outward-rounded interval arithmetic — is the remaining piece of the pilot triad.

research/challenges/laneb-mathieu · verify.js — own implementation, BigInt-rational Laurent polynomials · VERDICT.md — full checked/not-checked split, sources at commit 7573e57 · claim source: aimath.robertj1.com; artifacts: github.com/octonion/mathematics/mc · battery green 2026-08-03