Metadata

slug: jeudy-rouleux-global-permutation-lie
bibkey: jeudyrouleux2024exchange
doi: 10.1088/1742-6596/2912/1/012043
url: https://arxiv.org/abs/2411.03952v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Algebra/JeudyRouleuxGlobalPermutationLie.result

The Jeudy–Rouleux global-permutation Lie-algebra expectation

Problem

C. Jeudy and M. Rouleux, Generalized exchange operators for a system of spin-1 particles, arXiv:2411.03952v1, Section 3.1, pp. 6–7; DOI 10.1088/1742-6596/2912/1/012043. The source is recorded in jeudyrouleux2024exchange. The named expectation is preregistered in #19130.

Moreover since that the CSCO of the P- and Q-reps are the same in this case (see [Jin], p.70), we expect that Schrödinger Hamiltonian P_S, as well as other Hamiltonians, belongs to L.

The settlement refutes the membership assertion for the Schrödinger Hamiltonian at $(S, N) = (1, 3)$ . It uses all six global permutations of the three spin labels, hence also refutes membership in the smaller Lie algebra generated by the transpositions alone. It asserts nothing about other Hamiltonians.

Statement echo

Source clause	Lean counterpart	Scope
Spin one, three particles, $H = C^{3^{3}}$	Matrix indices `Fin 3 → Fin 3`, coefficients `ℂ`	Exactly three labels at each of three particle positions
$Q (ij) = Q (ij)^{\otimes 3}$	Global-action entry in `L` is one iff $x = α \circ y$	A single label permutation acts on every particle
The $Q (α)$ generate $L$	`L`, using `LieSubalgebra.lieSpan` and all six label permutations	A larger generator set strengthens the exclusion
$P_{ij}$ exchanges particles $i, j$	Entries in `schrodingerHamiltonian` are one iff $x = y \circ swap (i, j)$	Zero-based indexing
$H_{S} (1, 3) = \sum_{⟨ i, j ⟩} P_{ij}$	`schrodingerHamiltonian`, with pairs $(0, 1), (0, 2), (1, 2)$	Each unordered pair occurs once
The Hamiltonian belongs to $L$	`claim`	Literal membership assertion
Refutation	`result : ¬ claim`	No additional hypotheses

The public definitions display the literal global-action and exchange entries; the generic matrix and Lie constructions come directly from Mathlib. The equality projector and all three auxiliary theorems are private.

Motivation

The expectation would connect particle exchange Hamiltonians with the Lie algebra generated by global spin-label permutations. These operations act on different aspects of a configuration: particle exchanges permute positions, whereas the global action permutes labels uniformly.

Gap

Equality of complete sets of commuting observables does not establish this Lie-algebra membership. A global label permutation preserves equality between any fixed pair of particle labels; particle exchanges can move that equality to another pair.

Route

Let $O$ be the diagonal projector onto configurations satisfying $x_{0} = x_{1}$ . Every global permutation preserves this relation, so it commutes with $O$ . The centralizer of $O$ is a Lie subalgebra under the matrix commutator; therefore it contains $L$ .

For $y = (0, 0, 1)$ , the Hamiltonian gives

$Hy = (0, 0, 1) + (1, 0, 0) + (0, 1, 0),$

where each configuration denotes its basis vector. Only the first summand satisfies equality of the first two labels. Consequently $H O - O H$ has entry $1$ at row $(1, 0, 0)$ and column $(0, 0, 1)$ .

Falsifier

Membership $H \in L$ would force $H O - O H = 0$ . Its displayed entry equals $1$ , contradicting that equality. The kernel-checked public conclusion is D5.S3.Quantum.Algebra.JeudyRouleuxGlobalPermutationLie.result.

Evidence

The module is JeudyRouleuxGlobalPermutationLie.lean, with its Blueprint. Its private q_commutes proves commutation of each global action with the projector; lie_span_le_commutant places the generated Lie algebra in its centralizer; commutator_entry proves the nonzero entry. The public result combines these facts. The proof uses Mathlib’s centralizer and Lie-span machinery; it has no frozen D5 prerequisites.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Experiment

The numerical checker belongs to the-omega-institute/trureturing-experiments, commit 352da164a5a41fe1a3ac2513708bc49b3f6458a1. From that repository, python3 docs/reports/jeudy-rouleux-2024-global-permutation-lie-algebra/check.py exits 0 (RESULT PASS). The script’s SHA-256 is 52f066d07dbde5dad272df429584deeb0c40cf5b230c994825cd3a0d8a0c3240.

$(d, N)$	Computed $dim L$	$H \in L$	$P_{23} \in L$	All $Q (α)$ commute with $O$	$max ∣ [H, O]_{x y} ∣$
$(3, 3)$	6	false	false	true	1
$(2, 3)$	2	false	false	true	1
$(2, 4)$	2	false	false	true	1
$(3, 4)$	6	false	false	true	1
$(4, 3)$	24	false	false	true	1

These are floating-point rank tests with tolerance $1 0^{- 8}$ and numerical commutation checks. Their tested scope is exactly the five rows. The exact Lean proof is independent of these numerical rank decisions.

Triage

What the settlement shows

Kernel-checked mechanism, $(S, N) = (1, 3)$ . The three private theorems q_commutes, lie_span_le_commutant, and commutator_entry establish that $L$ commutes with $O$ while $H$ does not; the public result establishes $H \in / L$ . Equality of the first two particle labels is the separating invariant.
Computed only, five cases. The experiment entry records $H \in / L$ and $P_{23} \in / L$ for exactly $(d, N) \in {(3, 3), (2, 3), (2, 4), (3, 4), (4, 3)}$ . The listed dimensions and commutator maxima are numerical readings. A universal theorem for $d \geq 2, N \geq 3$ , and exact single-exchange exclusions, remain open in this delivery; neither is a theorem of this module.
Open, enlarged space. Section 6’s $L = L_{1} + L_{1}^{*}$ is outside claim and result. The source describes the dual family only modulo a two-dimensional subspace. This settlement supplies no membership or exclusion theorem for that enlarged space. Matching CSCO data alone supplies no Lie-membership implication.

The nearest statement retained by the proof is the exact inclusion of $L$ in the centralizer of $O$ . The source’s other spectral and representation results are outside the refuted assertion. Any use of the Section 3.1 membership expectation as a premise for this Hamiltonian is invalid; membership in the enlarged Section 6 space requires a separate argument.

Literature status

The source and literature screen in #19130 cover arXiv:2411.03952v1, Sections 1–6. The orchestrator reports OpenAlex work W4405241585 with zero citing works, and no earlier repository or issue owner. Semantic Scholar returned HTTP 429. No settlement was found within that recorded scope. Completeness is ASSUMED-UNVERIFIED.

ASSUMED-UNVERIFIED

The literature census is not exhaustive, and worldwide priority is not established. The numerical checker does not prove a uniform family theorem. The single-exchange exclusions beyond the numerical rows and membership in Section 6’s enlarged space are not settled here.

Keyboard shortcuts

trureturing — Discovering truth