Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: coulter-do-2025-deformed-jucys-murphy-noncommutation bibkey: coulter2025weingarten doi: 10.48550/arXiv.2506.04002 url: https://arxiv.org/abs/2506.04002v1 triage: theorem motivation_gids:

  • D5/S0/Certificates/Combinatorics/DeformedJucysMurphyNoncommutation.result

Coulter–Do Conjecture 5.4(a)

Problem

Xavier Coulter and Norman Do, arXiv:2506.04002v1, Conjecture 5.4(a), page 34:

The 𝒥-operators commute when restricted to 𝒳(k) — that is, 𝒥ₘ 𝒥ₙ (v) = 𝒥ₙ 𝒥ₘ (v) for 1 ⩽ m ⩽ n ⩽ k and for all v ∈ 𝒳(k).

Here k is a positive integer, the scalars are ℂ(b) with b an indeterminate, and 𝒳(k) is the orbit of the consecutive identity pair partition under the unital algebra generated by the operators in Definition 5.1. The theorem result proves ¬ claim, with all these quantifiers retained.

Motivation

The source verifies the conjecture numerically for k ≤ 5. At k = 6 the ambient vector space has 10395 basis matchings; the conjecture concerns its cyclic orbit, rather than commutation on the whole ambient space.

Gap

This is a tier-1 published named conjecture. Issue #11521 supplies the preregistration and scoped literature check. The cited refined Hurwitz operators in arXiv:2508.06188 are different operators, so their affirmative result does not settle Definition 5.1 commutation.

Route

Pair partitions are fixed-point-free involutive partner maps on Fin (2*k), with the paper’s labels shifted down by one. The transposition action is conjugation. The charge algorithm follows alternating identity and matching edges and takes the parity of the first occurrence of the component maximum. The graph-rule correspondence is an expository identification, not an additional universally quantified Lean theorem. The weight uses the charge of the output matching, the first argument of the paper’s weight function. Finite coefficient functions represent the paper’s vector space, and Algebra.adjoin represents its generated operator algebra.

Take k = 6 and v = J₆ J₆ J₅ J₄ J₃ e₆. Its generating word places v in X(6). At T = (1 5 | 2 7 | 3 9 | 4 11 | 6 10 | 8 12), the coefficients of J₂ J₄ v and J₄ J₂ v evaluate at b = 2 to 78 and 81. A support invariant for increasing words and a forced reverse transposition reduce the certificate computations. Coefficientwise ring-homomorphism transport and the injective embedding ℤ[X] → ℂ(b) turn their integer inequality into an inequality with b an indeterminate. Evaluation applies to polynomial coefficients, not to arbitrary rational functions with possible poles.

Falsifier

The refutation would fail if the word did not lie in X(6), the target were not a pair partition, the two kernel certificates had equal values, or the polynomial embedding were not injective. The proof discharges these obligations. The source interpretation also requires charges on the output matching and the stated label shift.

Evidence

D5/S0/Certificates/Combinatorics/DeformedJucysMurphyNoncommutation.result has type ¬ claim. The public surface consists of P, e, act, walk, charge, weight, J, single, X, claim, and this sole settlement theorem. The two private content theorems establish the increasing-word support invariant and the forced predecessor coefficient. The proof uses Mathlib and the standard axioms propext, Classical.choice, and Quot.sound.

Triage

theorem: Refuted, with admission basis open-problem-resolution and preregistration #11521. No digestion atom or coverage claim is attached.

What the settlement shows

  • Proved in this module: result gives a noncommuting vector inside the generated cyclic orbit at k = 6. Restricting the ambient space to X(k) therefore does not supply the missing commutativity. The failure occurs at the first size beyond the source’s reported checks.
  • Proved in this module: the support and forced-predecessor arguments occur on the live proof path to the 78 and 81 certificates. They avoid constructing the full 10395-by-10395 operator matrices.
  • Open in this module: a general theorem equating the walk charge with the graph charge. The finite correspondence through k = 6 has independent computational evidence reported in #11521 and the delivery; it is not a proof of the unbounded identification.
  • Open in this module: full commutation in restricted scalar cases or for k ≤ 5. The source’s small-size checks remain evidence for those restricted statements; the k = 6 refutation does not contradict them.
  • Open as separately formalized consequences: a simultaneous eigenbasis for these same operators would force commutation, so the noncommuting vector obstructs the structure proposed in Conjecture 5.4(b). This implication is mathematical exposition, not a second theorem here.
  • Open: corrected weight conventions, the dimension of X(6), and the ordering-sensitive status of Conjectures 5.7(b) and 5.8. The refutation removes commutativity as a justification for order-independent products. Proposition 5.9 explicitly orders monomials and does not assume 5.4(a); this result supplies no refutation of that proposition or of 5.7(a).

ASSUMED-UNVERIFIED

The literature search is scoped and does not establish exhaustive publication priority. The universal graph-charge bridge is not separately kernel-proved. The escape-audit registration is unfinished: source reconstruction, equivalence, and actual-positive-law obligations have no compiled Reg registration; see #11521. The model-family distinctness of codex-cli and ChatGPT Pro is ASSUMED-UNVERIFIED.