we-solve (beta)

Math-2290 · mathematics · Group theory

Second homotopy of Artin classifying complexes

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
$K(\pi,1)$ conjecturette: is $\pi_2$ of Deligne complex/Salvetti complex/hyperplane complement always trivial? Find a proof using geometric/combinatorial techniques.

Formulation references: [S1], [S2].

Short English statement

$K(\pi,1)$ conjecturette: is $\pi_2$ of Deligne complex/Salvetti complex/hyperplane complement always trivial? Find a proof using geometric/combinatorial techniques.

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2290-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2290

The main theorem proves full asphericity for the Salvetti and corresponding Deligne models. The problem statement’s additional unrestricted hyperplane-complement wording lacks the Tits-cone convention needed in infinite type, so the complete triple scope is not established. This entry records partial support; complete coverage of the question is not established by this catalogue.

Second homotopy of Artin classifying complexes

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. Every finite-rank Artin Salvetti complex is claimed aspherical, allowing arbitrary Coxeter labels.

Mathematical statement of the claimed result

Result 1.
Choose an arbitrary Coxeter matrix $M$ on a finite set $S$, allowing infinite labels. Let $W$ be its Coxeter group and $X(W,S)$ the Artin Salvetti complex, with a $|T|$-cell for each spherical subset $T\subseteq S$. The source claims \[ \widetilde{X(W,S)}\text{ contractible},\qquad \pi_n(X(W,S))=0\quad\text{for all }n\ge2. \] No connectedness condition is imposed on the Coxeter diagram.

Outline of the argument

A framed category records spherical parabolic cosets and the Artin action. Weighted harmonic heights and two-point estimates organize convex layers; cohomological tests on those layers remove the higher homotopy obstruction and establish the classifying-space property.

Formal verification

For family 254, the scope includes finite-rank Salvetti contractibility, the 116-generator Artin CAT$0$ counterexample, and arbitrary parabolic intersections with closure consequences. Each has its own Comparator statement. The listed Comparator files are ArtinCAT0.lean, ArtinParabolicIntersections.lean, HarmonicArtin.lean. Named declarations include OAI.ArtinCAT0.main, OAI.HarmonicArtin.salvetti_cover_contractible. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →