cert-machine · one of six · re-verified from the manuscript
The Mathieu property for Lie groups
Exactly the tori — a classification. For which compact connected Lie groups G is the kernel of Haar integration on R(G) a Mathieu–Zhao space?
tl;dr
The finding.CONFIRMED — supporting identities only. What a machine can decide about this claim, it decided, and it held. What it cannot decide is stated below rather than left to the reader to notice.
The mechanism. Written against the manuscript. The author's code was never executed — though in this lane, and only this one, it was read to cross-check which identities the TeX intended. Verification that existed at source: An author SymPy script, which we read but did not execute.
Check it.node legacy/research/challenges/lane/laneb-mathieu/verify.js — 70 ms at this build, a summary report and 3 mutation controls, every control rejected.
verdict
CONFIRMED
supporting identities only
named checks
—
this verifier reports a summary, not named rows — see below
the verifier's own total
126
stated by the verifier itself
mutation controls
3
deliberate corruptions of the claim — every one rejected, or this page would not build
runtime
70 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
Exactly the tori — a classification.
the problem
For which compact connected Lie groups G is the kernel of Haar integration on R(G) a Mathieu–Zhao space?
credited AI system
not recorded at source
verification at source
An author SymPy script, which we read but did not execute.
our verdict
CONFIRMEDsupporting identities only
§2 · what we certified
The ledger, as the verifier printed it at this build
Every supporting identity the classification rests on, exactly over ℚ with BigInt rational Laurent arithmetic: the weighted witness moments, the explicit abelian pair and its printed four-term expansion, the matrix-entry representatives and their invariance. Disclosure specific to this lane: the author’s Python was READ to cross-check which identities the TeX intended — its blocks match the manuscript and are the ones re-verified here — but it was never executed, and no value on this page came from it.
This verifier reports a summary rather than named rows. It states its own totals and its mutation-control outcome and stops there, so there is no per-check ledger to show and this page does not manufacture one. Its complete output at this build is reproduced verbatim:
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 3 were rejected in the run that built this page, and a control that stopped firing would refuse the page instead.
This verifier reports 3 controls rejected as a count rather than naming them individually, so there is nothing to list here beyond that count. The count is parsed from its output, not asserted.
§4 · the boundary
What this audit did NOT reach
not audited
The classification theorem itself. Confirming the identities a proof uses is not confirming the proof, and this lane is the clearest case of that distinction in the set.
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-mathieu/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.