Three two-strand boxes refute Jones–Wenzl generation at a root of unity

S. M. Flores and E. Peltola, Generators, projectors, and the Jones-Wenzl algebra (2018), arXiv:1811.12364v2, Section 1, Conjecture 1.2, TeX source WJalgebra_gen-sec1-intro.tex, lines 544–546, with macros expanded and references resolved:

Item 1 in theorem 1.1 holds whenever $\max \varsigma < \bar{\mathfrak p}(q)$.

Here $q\in\mathbb C^\times$, $\nu=-q-q^{-1}$ and $\varsigma=(s_1,\ldots,s_d)$ has positive entries, with total size $n_\varsigma=\sum_i s_i$. The source also permits the exceptional multiindex $(0)$. The bound $\bar{\mathfrak p}(q)$ is infinite at $q=\pm1$ and otherwise is the order of $q^2$, interpreted as infinite when that order is infinite. The composite Jones–Wenzl projector $P_\varsigma$ places projector boxes of sizes $s_i$ side by side, and $\mathrm{JW}\varsigma(\nu)=P\varsigma\mathrm{TL}{n\varsigma}(\nu)P_\varsigma$.

Item 1 of Theorem 1.1, at lines 502–516, states that, assuming $n_\varsigma<\bar{\mathfrak p}(q)$, the unit $P_\varsigma$ and the projected boundary generators $U_i^{\mathrm{JW}}=P_\varsigma U_{s_1+\cdots+s_i}^{\mathrm{TL}}P_\varsigma$, $1\le i<d$, form a minimal generating set. The conjecture replaces the total-size hypothesis by the individual-box hypothesis.

Issue #25910 fixes the generation assertion claim: for every nonzero complex $q$, every list $\varsigma$ of positive sizes individually below $\bar{\mathfrak p}(q)$, and every $T\in\mathrm{TL}{n\varsigma}(-q-q^{-1})$, the sandwich $P_\varsigma TP_\varsigma$ belongs to the ambient unital complex subalgebra generated by $P_\varsigma$ and the $U_i^{\mathrm{JW}}$. This assertion is refuted, which suffices to refute the conjecture independently of minimality. The definitions and source locator are in the literature note.

The distinction between existence of the individual projector boxes and generation of their whole corner determines whether the source's generator description extends to arbitrary admissible root-of-unity parameters. The source connects its generating sets to generators-and-relations presentations and to applications in quantum Schur–Weyl duality and conformal field theory (introduction, lines 475–478 and 560–567).

Issue #25910 records the bounded literature check before any Lean:

• The source's v2 retains Conjecture 1.2; its statement is present in the source text quoted above.
• The orchestrator reports that Flores and Peltola (2020), arXiv:2008.06038, retains the expectation of generation beyond the total-size bound, and that Spencer (2021), Modular valenced Temperley-Lieb algebras, arXiv:2108.10011, treats cellular structure and the two-part case without settling this generation assertion for three or more boxes.
• The issue records web searches for Jones–Wenzl and valenced Temperley–Lieb generation at roots of unity, and repository searches for the authors, algebra names and arXiv identifier, with no prior settlement found.

not-found-in-searched-scope.

All the representation certificates below concern the fixed parameter and matrices defined in this module.

1. Admissible parameter. Put $r=\sqrt3$ and $q_0=\exp(\pi i/6)$. The private lemma parameter establishes $q_0\ne0$, $\bar{\mathfrak p}(q_0)=6$ and $-q_0-q_0^{-1}=-r$. Thus the positive list $\varsigma=(2,2,2)$ satisfies the individual-size restriction $2<6$.
2. Projector and witness. The private lemmas projector and generators, for exactly $q_0$ and this list, identify the composite projector and its generating set as $P=(1+r^{-1}U_1)(1+r^{-1}U_3)(1+r^{-1}U_5)$ and ${P,PU_2P,PU_4P}$. The private definition middle is $W=U_2U_1U_4U_3U_2U_5U_4$; set $Z=PWP$.
3. Representation. In the quadratic rational algebra with $\omega^2=3$, exactRelations verifies the five fixed matrices $A_i$, indexed by $i\in\mathrm{Fin},5$: $A_i^2=-\omega A_i$ for every $i$; $A_iA_jA_i=A_i$ when $i+1=j$ or $j+1=i$; and $A_iA_j=A_jA_i$ when $i+1<j$ or $j+1<i$, using the natural values of these indices. These are precisely the three relation families needed to define the complex algebra homomorphism rho after scalarEmbedding sends $\omega$ to $r$. The private lemma rho_gen identifies $\rho(U_{i+1})$ for every $i\in\mathrm{Fin},5$, and rho_box identifies $\rho(P)$ with the embedded fixed matrix exactP.
4. Separating row. For the fixed row $\ell$ defined by row, the private lemmas row_projector and row_generators give $\ell\rho(P)=\ell$ and $\ell\rho(PU_2P)=\ell\rho(PU_4P)=-(r/3)\ell$. Its coordinate numbered $6$ from zero is zero. The private lemma exactWitness gives the corresponding witness coordinate $-2\omega/3$ before scalar embedding, and row_witness establishes $(\ell\rho(Z))_6\ne0$.
5. Subalgebra obstruction. The private definition rowStabilizer is the unital complex subalgebra of matrices $M$ satisfying $\ell M=c\ell$ for some $c\in\mathbb C$. The proof of separation puts all three generator images in this subalgebra; every matrix in it has $(\ell M)_6=0$, whereas the witness does not. Consequently separation establishes $Z\notin\mathbb C[P,PU_2P,PU_4P]$ in the ambient presented algebra. Applying claim at the nonzero parameter $q_0$, the positive admissible list $(2,2,2)$ and $T=W$ contradicts this lemma, giving result : ¬ claim.

The refutation must preserve the source's algebra, projectors and generation question:

• The module's TL is the quotient of the free complex algebra by rel, imposing exactly the square, adjacent triple-product and distant commutation relations. The source explicitly identifies this presentation with its diagram algebra at introduction lines 118–131. The module's gen uses the source's one-based indices on $1\le i<n$ and is zero outside that range.
• The module's qint is the Laurent sum $[k]q=\sum{j=0}^{k-1}q^{k-1-2j}$. For nonzero $q$ with $q^2\ne1$, multiplying this sum by $q-q^{-1}$ telescopes to $q^k-q^{-k}$, matching the source's quotient formula at lines 165–168. The recursion jw starts at $P_0=1$, so $[0]=0$ gives $P_1=1$ and then the source's recursion at lines 278–285; compProj uses consecutive offsets and box sizes. The concrete identity needed for the counterexample is established by projector.
• pbar uses the order of $q^2$, with infinity for infinite order and for $q=\pm1$. The counterexample's required value is established by parameter.
• Algebra.adjoin includes the ambient unit, whereas the source's corner uses $P_\varsigma$ as its unit. Every expression generated inside the corner from that unit and its boundary generators is also in the ambient adjoin. Nonmembership even in this ambient subalgebra therefore suffices. No faithful representation is required: membership would force membership of its image in rowStabilizer.
• The module restricts to positive list entries, excluding the source's exceptional $(0)$; the counterexample uses three positive entries. Its total size is $6=\bar{\mathfrak p}(q_0)$, so it lies outside the strict hypothesis of Theorem 1.1.

The canonical source is D5/S3/Quantum/Algebra/JonesWenzlGenerationRefutation.lean.

• Proof. It defines claim : Prop and proves result : ¬ claim.
• Axioms. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.
• Escape registrations. result is the designated refutation result of the utility header and is exempt. The module has no other public theorem.

Frozen state: Golden/Frozen/state/D5/S3/Quantum/Algebra/JonesWenzlGenerationRefutation.lean.json.

Declaration statements:

• result: sha256:03045f1a3313826bf976b8292264dae37a0f93d89d9bab6a6d8edec5f2653262;
• claim: sha256:c9088af2ce5424237051346dbf8aa7a6af53ea2800a6639965bf09436e32cb33.

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

The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2. The refutation is a certified instance with basis refutes. There is no digestion atom.

What the settlement shows

Proved by result: it is false that, for every nonzero complex $q$, every list $\varsigma$ of positive natural sizes with each $s\in\varsigma$ satisfying $s<\bar{\mathfrak p}(q)$, and every $T\in\mathrm{TL}{n\varsigma}(-q-q^{-1})$, the sandwich $P_\varsigma TP_\varsigma$ belongs to the ambient unital complex subalgebra generated by $P_\varsigma$ and all $P_\varsigma U_{s_1+\cdots+s_i}P_\varsigma$ with $1\le i<d$.

Computed, not formalized: None.

Argued, not formalized.

• Mechanism and missing condition. Existence of each box does not ensure that its projected boundary operators generate all sandwiches. For the fixed counterexample, row_projector and row_generators preserve the line spanned by the fixed row $\ell$, while row_witness shows that the sandwich $Z$ leaves it: a multiple of $\ell$ has coordinate $6$ zero. Sums, products and scalar multiples of line-preserving operators still preserve that line. Thus the obstruction concerns generation itself, before any question of a minimal generating set.
• Nearby statements. Restoring $n_\varsigma<\bar{\mathfrak p}(q)$ gives precisely the source's Theorem 1.1, whose hypothesis excludes this counterexample. The source's Corollary 3.6 states generation for two positive boxes under $\max(s_1,s_2)<\bar{\mathfrak p}(q)$ (WJalgebra_gen-appD-genlem-subsec2.tex, lines 95–102); the present counterexample requires three boxes. The module supplies no characterization for other lists or root orders, and does not settle generation when $n_\varsigma>\bar{\mathfrak p}(q)$ or the extension of Theorem 1.1, item 2, beyond its stated range; these questions remain open here.
• Effect on the paper. The source's active references to Conjecture 1.2 discuss the proposed extension and its special cases (introduction, lines 539–556); no other named theorem is identified there as conditional on the conjecture. Theorem 1.1 retains its strict total-size hypothesis. A presentation of the full counterexample corner cannot use only $P,PU_2P,PU_4P$: adding relations to those generators only identifies more expressions and cannot supply the missing sandwich. Thus the proposed general extension of that generator description is unavailable. This conclusion does not assess the later quantum Schur–Weyl or conformal-field-theory applications mentioned in the introduction.

The literature check is bounded and does not establish exhaustive worldwide novelty or priority. The readings of arXiv:2008.06038 and Spencer's arXiv:2108.10011, the citation listings and the web and repository searches reported in #25910 were not independently reproduced. The issue's diagram-algebra dimensions, control parameters and four-box computation were not independently reproduced and are not used as formal conclusions here.

The source's presentation-to-diagram identification, the general interpretation of the recursive projectors, the Laurent-sum comparison with its quantum integers, and the corner-unit comparison are not separate Lean theorems in this module; the concrete parameter, projector and separation certificates are on the proof path of result. The source's positive generation results are not formalized here. The consequences discussed in "Argued, not formalized" are not additional formalized conclusions. The other parameter ranges, alternative generating sets and downstream applications named above remain unverified here.