Classical K(pi,1) conjecture

PDF p. 1: §1.1, opening paragraph

In the finite-rank geometric convention, let $(W,S)$ be a Coxeter system with $S$ finite; $W$ need not be finite. Let ${\mathcal{X}}^{\mathbb{C}}$ be its classical complexified complement, put $Y={\mathcal{X}}^{\mathbb{C}}\mathrm{/}W$, choose $Z\in {\mathcal{X}}^{\mathbb{C}}$, and let $\bar{Z}\in Y$ be its orbit. Use the Artin–Tits group $A={\pi }_1(Y,\bar{Z})$ with its supplied identification with the presented Artin group. Is $Y$ aspherical, meaning ${\pi }_n(Y,\bar{Z})=0$ for every $n\ge 2$?

Equivalently, does this specified quotient $Y$ have the homotopy type of a $K(A,1)$, with the fundamental-group identification transported to the CW model? This is the article's classifying-space question in the usual homotopy-type sense. The question concerns $Y$ itself; the existence of some unrelated $K(A,1)$ does not answer it.

Reflecting hyperplanes, fundamental chamber and Tits cone

Classical complexified hyperplane complement

Artin–Tits group, pure subgroup and positive lifts

Higher homotopy group by based cubes

Coverings preserve the higher-homotopy obstruction to K(pi,1)

Eilenberg--Mac Lane space

Homotopy equivalences, homotopy inverses and spaces of the same homotopy type

For this item, write $K_W=\mathrm{Sal}({\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{e}}^{\circ },\mathcal{H})$ for the full simplicial CW complex of The Salvetti order complex and its finite CW case: its vertices are the incident facet–chamber pairs, its simplices are their finite chains in the supplied Salvetti poset, and its realization has the weak topology. Use the $W$-action induced by $w(F,C)=(wF,wC)$ from Linear symmetries act on the Salvetti model. Define the full standard Artin Salvetti complex in this subdivided convention to be ${\mathrm{Sal}}_A=K_W\mathrm{/}W$, with the quotient topology. All dimensions of $K_W$ are included.

The finite-rank cone is convex and the arrangement is locally finite by Basic Tits-cone properties; the proof of Classical free action and covering exact sequence identifies this dual reflection system as a Vinberg system. Thus the Coxeter quotient comparison of Independent Salvetti homotopy-model input applies to these exact objects and gives a homotopy equivalence ${\mathrm{Sal}}_A\to Y$.

Paris, §3.2 Theorem 3.3 and §3.3, identifies the preceding quotient with the standard Artin Salvetti CW space. Its cell decomposition has one cell of dimension $\mathrm{\mid }T\mathrm{\mid }$ for every $T\subseteq S$ such that $W_T=⟨T⟩$ is finite; the attaching maps are the projections of the characteristic maps of the Coxeter Salvetti cells described on printed p.398. This includes every spherical subset, rather than only the presentation 2-skeleton. The quotient is a CW complex, though generally not a regular CW complex. This construction is imported from that independent source.

A universal cover $p:{\stackrel{}{\mathrm{Sal}}}_A\to {\mathrm{Sal}}_A$ means a covering map with simply connected total space, as in Universal covering spaces. Paris, §4.1 Proposition 4.2, supplies such a cover for this full complex. Contractible means that its identity map is homotopic to a constant map, equivalently that the space is homotopy equivalent to a point in the sense of Homotopy equivalences, homotopy inverses and spaces of the same homotopy type. Neither the existence of this cover nor the construction of the complex asserts that it is contractible.

The established comparison above supplies CW homotopy type for $Y$. Asphericity and the equivalence between vanishing higher homotopy groups and having the homotopy type of a $K(A,1)$ use Coverings preserve the higher-homotopy obstruction to K(pi,1), Higher homotopy group by based cubes, Eilenberg--Mac Lane space and Homotopy equivalences, homotopy inverses and spaces of the same homotopy type. The chosen $\bar{Z}$ and the identification $A={\pi }_1(Y,\bar{Z})$ come from Artin–Tits group, pure subgroup and positive lifts; the cited asphericity supplier explains how an unbased homotopy equivalence transports this identification by a basepoint path. No CW structure on the underlying quotient $Y$ is required by this formulation.

The frozen article, dated July 30, 2026, reports this conjecture open in general in §1.1. This is its historical status statement.

A subsequent manuscript, Harmonic heights and the Artin K(pi,1) conjecture (September 23, 2026), claims in Theorem 1.1 that ${\stackrel{}{\mathrm{Sal}}}_A$, the universal cover of the full standard Artin Salvetti complex specified above, is contractible for every finite set of standard generators, including infinite Coxeter groups, infinite edge labels and disconnected diagrams. The full complex, including its higher cells, is essential to that claim.

As checked on November 13, 2026, the MathVet HarmonicArtin row reports a successful comparator run, and the cert-machine HarmonicArtin entry reports acceptance by both Lean and nanoda kernels of the exact formal challenge. These are independent reported machine checks of a specified formal model. The fidelity and kernel reports distinguish that model from its intended interpretation as the geometric space in the conjecture.

The present status is therefore recorded as a claimed solution with independent machine-check reports, under mathematical evaluation here. This item supplies neither a proof of the claimed solution nor an unconditional assertion that the conjecture remains open or has been settled. It is retained as the article's question with an explicit status qualification and supplies no proof premise to established items.

The original §1.1 says that the quotient is conjecturally a classifying space, starting from a Coxeter system without an explicit rank phrase. The finite-rank convention above makes explicit the geometric setting used by the local complement and Artin-group definitions. The article's §2.2 follows Iyama–Wemyss for the dual reflection space and invokes Vinberg's reflection framework; its Proposition 3.6 proof uses finite dimension. Iyama–Wemyss §§1.1–1.3 explicitly use an $n\times n$ Coxeter matrix and nodes $\{1,\dots ,n\}$. Paris §1 likewise defines Coxeter graphs on finite sets and Vinberg systems in finite dimension. This supports a finite-rank reading of the geometric question while preserving every Coxeter type; it is not a claim that the article explicitly stated a global rank assumption.

The algebraic definition of a Coxeter system can also allow infinitely many generators. No infinite-rank geometric complement or equivalence to a Salvetti colimit is specified or asserted here. Extending the literal geometric formula to that setting would require additional topological conventions and a verified equivalence; the finite-rank machine-check reports do not provide that extension.

The source reading was limited to the passages and files specified in the citation metadata. In particular, the complete categorical proof and Lean dependency closure of the 2026 claim were not independently validated, and the reported kernel checks were not replayed. The established Salvetti comparison is used here to supply CW homotopy type and to fix the conventional complex named in the status report. It is not used to convert the 2026 claim into an accepted theorem. The historical source-reading limits in the unchanged status citations are retained; the present adjudication's additional Paris reading is recorded separately in that reference's metadata.