Metadata
slug: flores-peltola-2018-jones-wenzl-generation-refutation
bibkey: florespeltola2018generators
doi: 10.48550/arXiv.1811.12364
url: https://arxiv.org/abs/1811.12364v2
triage: theorem
motivation_gids:
- D5/S3/Quantum/Algebra/JonesWenzlGenerationRefutation.result
Three two-strand boxes refute Jones–Wenzl generation at a root of unity
Problem
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 .
Here , and has positive entries, with total size . The source also permits the exceptional multiindex . The bound is infinite at and otherwise is the order of , interpreted as infinite when that order is infinite. The composite Jones–Wenzl projector places projector boxes of sizes side by side, and .
Item 1 of Theorem 1.1, at lines 502–516, states that, assuming , the unit and the projected boundary generators , , 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 , every list of positive sizes individually below , and every , the sandwich belongs to the ambient unital complex subalgebra generated by and the . This assertion is refuted, which suffices to refute the conjecture independently of minimality. The definitions and source locator are in the literature note.
Motivation
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).
Gap
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.
Route
All the representation certificates below concern the fixed parameter and matrices defined in this module.
- Admissible parameter. Put and . The private lemma
parameterestablishes , and . Thus the positive list satisfies the individual-size restriction . - Projector and witness. The private lemmas
projectorandgenerators, for exactly and this list, identify the composite projector and its generating set as and . The private definitionmiddleis ; set . - Representation. In the quadratic rational algebra with ,
exactRelationsverifies the five fixed matrices , indexed by : for every ; when or ; and when or , using the natural values of these indices. These are precisely the three relation families needed to define the complex algebra homomorphismrhoafterscalarEmbeddingsends to . The private lemmarho_genidentifies for every , andrho_boxidentifies with the embedded fixed matrixexactP. - Separating row. For the fixed row defined by
row, the private lemmasrow_projectorandrow_generatorsgive and . Its coordinate numbered from zero is zero. The private lemmaexactWitnessgives the corresponding witness coordinate before scalar embedding, androw_witnessestablishes . - Subalgebra obstruction. The private definition
rowStabilizeris the unital complex subalgebra of matrices satisfying for some . The proof ofseparationputs all three generator images in this subalgebra; every matrix in it has , whereas the witness does not. Consequentlyseparationestablishes in the ambient presented algebra. Applyingclaimat the nonzero parameter , the positive admissible list and contradicts this lemma, givingresult : ¬ claim.
Falsifier
The refutation must preserve the source’s algebra, projectors and generation question:
- The module’s
TLis the quotient of the free complex algebra byrel, 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’sgenuses the source’s one-based indices on and is zero outside that range. - The module’s
qintis the Laurent sum . For nonzero with , multiplying this sum by telescopes to , matching the source’s quotient formula at lines 165–168. The recursionjwstarts at , so gives and then the source’s recursion at lines 278–285;compProjuses consecutive offsets and box sizes. The concrete identity needed for the counterexample is established byprojector. pbaruses the order of , with infinity for infinite order and for . The counterexample’s required value is established byparameter.Algebra.adjoinincludes the ambient unit, whereas the source’s corner uses 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 inrowStabilizer.- The module restricts to positive list entries, excluding the source’s exceptional ; the counterexample uses three positive entries. Its total size is , so it lies outside the strict hypothesis of Theorem 1.1.
Evidence
The canonical source is D5/S3/Quantum/Algebra/JonesWenzlGenerationRefutation.lean.
- Proof. It defines
claim : Propand provesresult : ¬ claim. - Axioms. It uses only the standard axioms
propext,Classical.choiceandQuot.sound; nosorry,native_decide, or new axiom. - Escape registrations.
resultis the designated refutation result of theutilityheader 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.
Triage
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 , every list of positive natural sizes with each satisfying , and every , the sandwich belongs to the ambient unital complex subalgebra generated by and all with .
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_projectorandrow_generatorspreserve the line spanned by the fixed row , whilerow_witnessshows that the sandwich leaves it: a multiple of has coordinate 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 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 (
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 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 : 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.
ASSUMED-UNVERIFIED
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.