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

The rank-two Poisson conjecture

An explicit counterexample: polynomials R, T, D, S in ℚ[x,q,p,z] with prescribed bracket relations. A conjecture about rank-two Poisson structures.

tl;dr
  • The finding. CONFIRMED — the explicit counterexample. 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. Verification that existed at source: The author’s own scripts, which we neither derived from nor executed.
  • Check it. node legacy/research/challenges/lane/laneb-poisson/verify.js — 400 ms at this build, a summary report and 2 mutation controls, every control rejected.
verdict
CONFIRMED
the explicit counterexample
named checks
this verifier reports a summary, not named rows — see below
the verifier's own total
this verifier prints no total of its own
mutation controls
2
deliberate corruptions of the claim — every one rejected, or this page would not build
runtime
400 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

fieldas recorded at source
the claimAn explicit counterexample: polynomials R, T, D, S in ℚ[x,q,p,z] with prescribed bracket relations.
the problemA conjecture about rank-two Poisson structures.
credited AI systemnot recorded at source
verification at sourceThe author’s own scripts, which we neither derived from nor executed.
our verdictCONFIRMED the explicit counterexample
§2 · what we certified

The ledger, as the verifier printed it at this build

All six bracket relations ({D,R} = 1, {S,T} = 1 and the four vanishing ones) hold identically and exactly; the 4×4 symbolic Jacobian determinant is identically 1; and the three claimed points each map exactly to their stated image. A counterexample is an existence claim, so certifying the exhibit IS certifying the claim — the only lane in this set where that is true.

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:

All claimed identities hold exactly (bracket relations, det J = 1, three-point fiber).
Mutation control 1 (R -> R + 1/7): rejected, 3 failing checks. OK
Mutation control 2 (bracket sign swapped): rejected, 2 failing checks. OK
Elapsed: 0.4s
VERDICT: CONFIRMED
§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 2 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
1R -> R + 1/7 — rejected, 3 failing checks
2bracket sign swapped — rejected, 2 failing checks
§4 · the boundary

What this audit did NOT reach

not audited

The author’s surrounding prose beyond the extracted definitions. Nothing load-bearing: the counterexample stands or falls on the exhibit, and the exhibit holds.

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-poisson/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.