The stable commutator length of a relator is not a one-relator group invariant
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Let $S,S'$ be sets and let $r\in F(S)'\setminus\{e\}$, $r'\in F(S')'\setminus\{e\}$ be relators with $\langle {S} \; | \; {r} \rangle \cong\langle{S'} \;| \; {r'}\rangle$. Does this imply that $\text{scl}_S r=\text{scl}_{S'}r'$?
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
Claude Opus 5; Harmonic Aristotle (Lean formalisation)
Two systems, and the paper is more specific in its body than in its formal statement. The AI use statement reads only: "Claude Desktop with Opus 5 assisted in designing and orchestrating the computational search for candidate counterexamples." Section 4 puts it more strongly: "Claude Desktop with Opus~5 designed and orchestrated an exhaustive search through $\operatorname{Aut}(F_2)$-orbits of words of length at most 20." Candidates were then filtered by first homology of low-index subgroups, Alexander polynomials and homomorphism counts to small finite groups, with explicit isomorphisms constructed for those the invariants did not separate.
Co-developed rather than assisted on the strength of the second sentence: the author formulated the target - pairs in different $\operatorname{Aut}(F_2)$-orbits whose one-relator groups are nonetheless isomorphic, which is exactly the configuration that leaves scl unconstrained - and the model designed and ran the search that found one.
A second system appears in the same paragraph and is recorded here because the submission omitted it: the Lean formalisation of the six identities "produced with the assistance of Harmonic's Aristotle". That is the artifact this entry's verification rests on.
Unreviewed, lowered from Lean-verified on inspection. A labelling correction, not a doubt about the mathematics.
The theorem has two halves - the groups are isomorphic, and the relators have different scl - and only the first is formalised. The Lean file says so itself: "(The paper computes scl r = 1 ≠ 1/2 = scl r' with scallop; see scl/.)" So the half that makes this a counterexample is a computation, not a machine-checked proof, and Lean-verified additionally requires the formal statement to be independently anchored, which an author's own repository is not.
What the Lean does establish, and it is not nothing: one file, 282 lines, with no sorry, no admit, no native_decide and no declared axiom. It builds the two homomorphisms explicitly and proves they compose to the identity in both directions, so the isomorphism is constructed rather than asserted. Not built here - no Lean toolchain on this machine, and it pins v4.28.0.
The scl values were not reproduced here either. They are reproducible in principle: scl/setup_scallop.sh fetches and patches Alden Walker's scallop, and compute_scl.py rechecks every value the paper quotes against it, exiting non-zero on disagreement. It needs a C++11 compiler with GLPK and GMP, none present on this machine.
Checked independently on 30 August 2026: both relators have exponent sum zero in both generators, so both do lie in $F'$ as the question requires; both are cyclically reduced, length 20, distinct, and match the abstract exactly.
A negative answer to Heuer and Löh's question: the isomorphism type of a one-relator group $\langle S \mid r\rangle$ does not determine $\mathrm{scl}_S(r)$. The witnesses are $r=\mathtt{aabABabABBAbaabABBAb}$ and $r'=\mathtt{aabABabABabABBAbaBAb}$, both length 20 in $F_2'$, with $\langle a,b \mid r\rangle\cong\langle a,b\mid r'\rangle$ but $\mathrm{scl}(r)=1$ against $\mathrm{scl}(r')=1/2$.
The mechanism is what made the search finite: $\mathrm{scl}$ is an $\operatorname{Aut}(F_2)$-invariant, so a pair in *different* orbits whose one-relator groups happen to be isomorphic has its two scl values unconstrained by each other. The search was for that configuration among words of length at most 20.
Scope: it settles the question as posed and nothing wider. It does not say which invariants do determine scl, and this is a single pair rather than a construction giving arbitrary gaps.
Known method families
computation (source-reported)
Source-reported tools: computation.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.