Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: heib-bruschi-2026-conjecture-83-affine-refutation
bibkey: heib2026structural
doi: 10.48550/arXiv.2601.16161
url: https://arxiv.org/abs/2601.16161v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Algebra/HeibBruschiCenterlessIdealGraphRefutation.result

The affine Lie algebra refutes Heib–Bruschi Conjecture 83

Problem

T. Heib and D. E. Bruschi, On the structural properties of Lie algebras via associated labeled directed graphs, arXiv:2601.16161v1, attach to a basis of a Lie algebra in which every bracket of two basis vectors is a multiple of a basis vector (a minimal-graph-admissible basis) the directed graph with an edge from to , labelled , whenever is a nonzero multiple of . A vertex subset has the ideal-graph-property when no edge leaves it. Conjecture 83 states that a minimal-graph-admissible Lie algebra with trivial center either (i) has no proper non-empty vertex subset with the ideal-graph-property, or (ii) is a direct sum of components with trivial center whose every minimal graph has no such subset. The verbatim statements are in the literature note.

Issue #13676 fixes the reading over every field, as the paper’s convention “We denote any field with the symbol ” requires, with the direct sum read as an internal direct sum of ideals over an arbitrary index type.

Motivation

The paper uses the graphs to read off centers, derived and lower central series and ideals, for Lie algebras that arise in quantum dynamics. Conjecture 83 is its proposed converse to Conjecture 80 (a nonzero center forces a proper vertex subset with the ideal-graph-property): trivial center should force the graph to be strongly connected unless the algebra splits. D5/S3/Quantum/Algebra/HeibBruschiCenterlessIdealGraphRefutation.conjecture_fails shows that the converse fails already in dimension two, over every field, and result refutes the conjecture as stated.

Gap

Issue #13676 records the literature check before any Lean: arXiv lists only v1 of the paper; the first author’s later papers (arXiv 2609.15302, 2610.04001) and the only forward citation found (arXiv 2603.04916) do not discuss Conjecture 83; Zenodo phrase searches (“graph-admissible”, “ideal-graph-property”, the title phrase, the identifier) return no record; web searches return no settlement; the repository had no related result. The paper names as an example of a solvable non-nilpotent algebra but tests Conjecture 83 only against . not-found-in-searched-scope.

Route

Let with , , , so .

  1. Hypotheses hold. is admissible with , ; the center is zero because and .
  2. (i) fails. The edges are (label ) and (label ), so is a proper non-empty subset with the ideal-graph-property.
  3. Every nonzero ideal contains . If lies in an ideal, then does: by scaling when , and from when .
  4. (ii) fails. Two different components of an internal direct sum have zero intersection, so at most one is nonzero; as exactly one is, and it equals . The basis transported to it along is admissible and keeps the subset .

Falsifier

The refutation would fail if the reading of (ii) admitted a decomposition of in which no component carries , for instance a direct sum of vector spaces that are not ideals; the paper’s “direct sum” of Lie algebras requires ideals.

Evidence

The canonical source is D5/S3/Quantum/Algebra/HeibBruschiCenterlessIdealGraphRefutation.lean. Its public declarations are IsAdmissible, Edge, IdealGraphProperty, HasProperIdealGraphSubset, conjectureOver, claim, conjecture_fails and result; it imports only Mathlib.Algebra.Lie.Abelian and uses Mathlib’s LieIdeal, LieAlgebra.center, DirectSum.IsInternal and LieIdeal.topEquiv. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom. The module statement is sha256:03f8b723eb159d4644f6d1dd6c33a7a4178d57f9b4baa65c19c6c525fdf57780, the result statement sha256:b4e0d950bf87a2ff041d6ce3d2b7db1dab3357dfee2daba85e00e2c59f35220d and the claim statement sha256:08773a6e3d525df761e901ec5860871266cca8ff702a869cafa2f8c6c36470d4. The Freeze event is sha256:35ec93190d6f1ffe1019e8ade7770514b05429674e1f25e6e65e774091720cf1; it has no project-level prerequisite.

Triage

Tier 1 conjecture of a 2026 paper, preregistered in issue #13676 before any Lean. theorem; resolution refuted.

declarationproof_shapeescape_witnessadmission_basis
conjecture_failsbind-onlynoneopen-problem-resolution
resultbind-onlynoneopen-problem-resolution

The private theorems (affineBasis_admissible, affine_center_zero, affineBasis_proper_subset, ideal_contains_y, internal_has_top, admissible_map, proper_subset_map) are bind-only and are used on the proof path of result (CLAUDE.md §3.2 「有消费的辅助声明」). Utility is certified-instance with basis refutes of claim. There is no digestion atom.

What the settlement shows

Proved by result and conjecture_fails: Conjecture 83 fails over every field; the two-dimensional affine Lie algebra satisfies its hypotheses and neither conclusion.

Established inside the proof. Every nonzero ideal of contains , so has no nontrivial decomposition as an internal direct sum of ideals (ideal_contains_y, internal_has_top); admissible bases and proper subsets with the ideal-graph-property are carried along Lie isomorphisms (admissible_map, proper_subset_map).

Argued, not formalized.

  • A vertex subset with the ideal-graph-property spans an ideal: for and a basis vector , is zero or a nonzero multiple of some , and then there is an edge from to , so . The conjecture therefore fails whenever a centerless admissible algebra has a proper ideal spanned by basis vectors that no decomposition into ideals separates off. In this is the abelian ideal : it has the subalgebra complement , so , but no complementary ideal, because every nonzero ideal contains .
  • The two natural repairs of (i) also fail: restricting it to subsets that span a solvable ideal is still refuted by , since is abelian; restricting it to subsets that span a non-solvable ideal is refuted in characteristic by with the basis , where has the ideal-graph-property and the part keeps .
  • The conjecture holds for every Lie algebra that is a direct sum of simple ideals (in characteristic , every semisimple algebra): each simple component has trivial center, and by the first item a proper non-empty subset with the ideal-graph-property in a minimal graph of a component would span a proper nonzero ideal of a simple algebra.

Open. Which corrected form the authors intend (for example, (ii) replaced by a condition on the radical) is not determined by the paper.

Effect on the paper. Conjecture 83 is false as stated. The affine algebra is not a counterexample to Conjecture 80 (a nonzero center forces a proper subset with the ideal-graph-property that spans a solvable ideal), since its center is trivial, nor to Conjecture 82, since its only proper subset with the ideal-graph-property spans a solvable ideal. This settlement makes no claim about Conjecture 82 in general.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent counterexample.