{"id":"16b8597d-f95c-4b0d-85c8-019ebe13dff1","arxiv_id":"2502.03028","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper proves the first basis theorem for graded gl₂-foams via a new 'linear Gray rewriting modulo' framework.","lead":"This paper develops a new rewriting theory for diagrammatic algebras and uses it to prove the first basis theorem for graded gl₂-foams, an object used in categorification and quantum topology. If correct, it provides a general algorithmic tool for finding bases in many diagrammatic algebras.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The basis proof hinges on Lemma 4.14 identifying T-normal forms with reduced foams, whose proof is deferred to the author's thesis; a gap here would invalidate the application of Basis-From-Convergence.","rationale":"The reader's weakest-assumption analysis identifies Lemma 4.14, and I agree that this is the load-bearing concern. The paper's main novelty is the rewriting framework; its advertised application is the basis theorem for graded gl2-foams. That application rests on applying Theorem 3.36 to T, and Theorem 3.36 only produces a basis when the monomial T+-normal forms are known and scalar-coherent. Lemma 4.14 is the statement that supplies exactly that input. Because the proof is deferred to the author's thesis rather than included, an independent check of this lemma is necessary before the central claim can be considered fully verified. The confluence proof itself is long and diagram-heavy, and a misclassified branching would also break convergence, but the paper gives considerably more detail there. The deferred lemma is a cleaner, explicitly identified gap. I do not see an internal inconsistency that would force rejection; the concern is an omitted proof of a key step, which is addressable. Hence the reader's CONDITIONAL verdict stands unchanged.","tokens_in":62948,"tokens_out":5758,"duration_ms":54277,"concrete_test":"Reproduce the proof of Lemma 4.14 from the cited thesis proposition in the paper: (i) show every reduced foam is a T+-normal form by checking that none of the sources of dd, dm, bb⟲, bb⟳, nc, sq can be projectively E-congruent to a reduced foam, paying special attention to the edge case of a single dot on a disk whose boundary is an i-strand (where dm might apply); (ii) show every non-reduced foam admits a T+-rewriting step by constructing, from a non-disk component or a component with at least two dots, an applicable rule (bb for a closed strand, dd/dm for repeated dots). If both directions check out, the stated proof of Theorem 4.10 is complete; if not, the basis claim is unsupported by the rewriting argument.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 4.10 is derived from Basis-From-Convergence Theorem 3.36 applied to the context-dependent sub-system T. For that theorem to output reduced families, Lemma 4.14 must be exactly right: monomial T+-normal forms must coincide, up to foam isotopy, with reduced foams. The lemma is stated in §4.2.2 and its proof is omitted, deferred to [Sch24, Proposition 1.6.5]. If the identification fails in either direction, the argument collapses: if some reduced foam is not a T+-normal form, then reduced families are not contained in the module of normal forms; if some T+-normal form is not E-congruent to a reduced foam, then reduced families do not span NFS/⟨E⟩. In both cases Basis-From-Convergence does not produce Theorem 4.10. Lemma 4.14 is also used in Corollary 4.16 to establish scalar-coherence of E on the relevant normal forms. The surrounding confluence classification (Propositions 4.26, 4.35, 4.36) is intricate, but Lemma 4.14 is the most direct unverified link: it translates the geometric notion 'sl(F) is a union of disks with at most one dot each' into the syntactic notion 'no T-rewriting step applies', and the paper gives no proof of that translation.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a rewriting framework for diagrammatic algebras, called linear Gray rewriting modulo, and applies it to prove a basis theorem for the graded-2-category GFoam_d of graded gl_2-foams. Sections 2 and 3 introduce linear Gray polygraphs, tamed congruence, context-dependent termination, and a Basis-From-Convergence theorem, while Section 4 constructs a rewriting system for GFoam_d, analyzes its confluence modulo foam isotopies, and derives Theorem 4.10. The main result is the first proof of the basis conjecture for GFoam_d, which underlies the higher-representation-theoretic construction of odd Khovanov homology in [SV23].","tokens_in":63183,"tokens_out":6019,"duration_ms":53375,"significance":"If correct, the paper is significant both as a proof of a concrete basis theorem for graded gl_2-foams and as a general methodology for studying presentations of diagrammatic algebras. Its strengths are the explicit framework, the detailed strategy for classifying branchings modulo a non-coherent equivalence, and the reduction of a substantial geometric statement to a finite list of confluence checks. The exposition is careful and the paper makes good use of running examples. However, the proof is long and depends on several technical statements whose proofs are deferred or sketched; in particular, the identification of normal forms with reduced foams is load-bearing and is not proved in the paper.","major_comments":[{"comment":"Lemma 4.14 is stated without proof and deferred to [Sch24, Proposition 1.6.5]. This lemma supplies the identification between monomial T+-normal forms and reduced foams that is required for the application of the Basis-From-Convergence Theorem 3.36; both inclusions are needed. Since Corollary 4.16 also relies on it, this is a load-bearing step. The proof should be given in the paper, or the dependency should be replaced by a verifiable argument; a citation to a thesis is not enough for this point.","section":"§4.2.2, Lemma 4.14"},{"comment":"The proof of Lemma 4.22 is a sketch. It asserts that after sliding strands one either reaches an independent branching or is in the case of 'precisely one cap or one cup' in common, leading to four critical branchings, but the case where both a cup and a cap are shared is not discussed and the four branchings are not derived. This classification is the basis for convergence of Z modulo E and hence for Proposition 4.6 and Corollary 4.16; a complete case analysis is required.","section":"§4.3, Lemma 4.22"},{"comment":"In the proof of Lemma 4.27, the statement 'we use coherence of E (Proposition 4.6) to present the isotopy e as a composition of E-naturalities' appears to ask for more than Proposition 4.6 provides. Proposition 4.6 asserts equality of scalars for parallel E-morphisms with the same bijection on dots and strands; it does not, by itself, give a decomposition of an arbitrary isotopy into braided-like and pivotal naturalities. Since the confluence proofs in Proposition 4.26 rely on this decomposition, a proof of the claimed normalization is needed.","section":"§4.4.2, Lemma 4.27"},{"comment":"The proof of Lemma 4.35 acknowledges that the Contextualization Lemma 3.62 does not apply to the first critical sq-branching in Fig. 4.3, and then invokes an argument 'essentially the same as Lemma 3.66' together with Lemma 4.33. This is only sketched; as these critical branchings are needed for Proposition 4.18, a detailed verification of this final case should be included.","section":"§4.4.4, Lemma 4.35"}],"minor_comments":[{"comment":"Lemma 4.14 has a grammatical typo: 'A foam is a T+-normal form is and only if it is reduced' should be 'if and only if'. Also, the preorder ≻ is written with '#dd' in the last component; the notation should be '#di' (or '#d_d') to match the preceding '#d_i'.","section":"§4.2.2"},{"comment":"For the sq relation, 'the two pieces of i-strands' is ambiguous because sq involves four strand pieces; please specify the distinctness condition precisely.","section":"§4.2.2, Definition 4.13"},{"comment":"The distinction between the non-coherence of E noted in Remark 3.26 and the scalar-coherence on reduced foams established in Corollary 4.16 is important; a sentence making it explicit that Corollary 4.16 concerns only monomial normal forms would prevent confusion.","section":"§3.5.1 / §4.2.2"},{"comment":"Several proofs say 'similar arguments apply' (e.g., for type sq in Lemma 4.31 and in Lemma 4.35); given the length of the paper, a short appendix or a more detailed figure for these cases would improve verifiability.","section":"§4.4"}],"recommendation":"major_revision","confidential_remarks":"The main concern is the reliance on the author's thesis for Lemma 4.14 and related normal-form facts; if these are accepted, the rest is credible. The paper is within scope for the journal and likely to be influential. I would advise requesting the missing proof and a complete treatment of the sketched critical branchings before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does something real: it proves the first basis theorem for the graded gl2-foam 2-category GFoam_d, which underlies the higher-representation-theoretic construction of odd Khovanov homology. The rewriting framework it introduces—linear Gray rewriting modulo, with tamed congruence and context-dependent termination—is a genuine new tool, and the paper is refreshingly explicit about where previous work (Alleaume, Dupont) has gaps. The proof of the basis theorem itself is a serious piece of work: the classification of critical branchings is intricate, and the use of a context-dependent subsystem T to get termination is clever.\n\nThe soft spot is exactly where the stress-test note points: Lemma 4.14, which identifies T-normal forms with reduced foams, is stated without proof and deferred to the author's thesis. This is load-bearing—if that lemma fails, the Basis-From-Convergence theorem does not produce the claimed basis. The paper explicitly says the proof is in [Sch24, Prop. 1.6.5], so it's not hidden; but for a journal submission, a key lemma deferred to a thesis is a real problem. A referee needs to see that proof, or at least a detailed sketch. The rest of the confluence analysis is plausible, though I'd want a careful referee to check the critical branchings in Figures 4.2–4.4; they're not machine-checked, but that's normal in this area.\n\nThe citation of the author's own thesis for Lemma 4.14 is fine—it's a legitimate reference, and the lemma is a geometric claim about reduced foams, separate from the rewriting theory. The paper is written accessibly, with a long introduction and a state-of-the-art overview that makes the main ideas understandable.\n\nBottom line: this is a substantial contribution that deserves a serious referee. The main fix is to include a proof of Lemma 4.14 (or a summary long enough to convince a careful reader). I'd send it to peer review without hesitation, with the expectation of a request for major revision on that point.","headline":"First proof of the gl2-foam basis theorem via a genuinely new higher rewriting framework, but the load-bearing Lemma 4.14 is deferred to the thesis.","tokens_in":63719,"tokens_out":2062,"would_cite":true,"duration_ms":19142,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18M30","18N10","57K18","68Q42"],"pacs":[],"model":"deepseek-v4-flash","headline":"Rewriting theory proves the graded gl2-foam basis theorem.","keywords":["rewriting theory","diagrammatic algebras","graded gl2-foams","basis theorem","categorification","odd Khovanov homology","rewriting modulo","tamed congruence"],"falsifier":"Find two parallel 1-morphisms W, W' in GFoam_d for which a reduced family satisfies a nontrivial linear relation in Hom_GFoam_d(W,W'), or exhibit a reduced foam that is not a T-normal form (or a T-normal form that is not reduced); the second check is a direct inspection of the rewriting rules and would settle the deferred Lemma 4.14.","tokens_in":62716,"feed_emoji":"🧶","tokens_out":4496,"duration_ms":42832,"temperature":0.7,"pith_summary":"This paper establishes a basis theorem for the graded-2-category of graded gl2-foams, a diagrammatic algebra built from coloured strands, dots, cups, caps, and crossings: any reduced family of foams between two parallel 1-morphisms is a basis of the corresponding Hom module. This was a conjecture underlying the higher-representation-theoretic construction of odd Khovanov homology, and the paper gives the first proof. The proof is algorithmic and intrinsic, built from a new rewriting theory for diagrammatic algebras that combines linear rewriting, higher rewriting, and rewriting modulo structural relations such as pivotality. The reader should take the result as evidence that rewriting methods can replace concrete faithful representations as the standard tool for hom-basis problems in categorification.","feed_headline":"Rewriting theory proves the graded gl2-foam basis theorem","feed_subtitle":"A modular rewriting argument yields the first proof that reduced foams form bases, anchoring odd Khovanov homology.","key_machinery":"The carrying object is a linear Gray rewriting system modulo: a pair (R,E) of linear 3-sesquipolygraphs with the same underlying 2-sesquipolygraph, where E contains the graded interchangers and foam isotopies (braid-like, pitchfork, and zigzag relations) and R contains the foam relations dd, dm, bb, nc, and sq. The load-bearing work is done by the context-dependent subsystem T, the lexicographic preorder comparing numbers of shadings, closed strands, and dots, and the notion of a ≻-tamed congruence, which replaces confluence in the linear setting; convergence of T+ together with scalar coherence of E on reduced foams feeds the Basis-From-Convergence Theorem.","core_discovery":"The central claim is Theorem 4.10: for any two parallel 1-morphisms W and W' in the graded-2-category GFoam_d, any reduced family defines a basis of the k-module Hom_GFoam_d(W,W'). Since GFoam_d is presented by the linear Gray polygraph GFoam_d = E ⊔ R, the paper proves the basis conjecture for GFoam_d stated in [SV23]. The proof works by splitting the generators into oriented rewriting rules R and unoriented modulo rules E, defining a context-dependent subsystem T whose normal forms are exactly the reduced foams, and showing that T+ is convergent via a tamed version of Newman's lemma. Convergence then feeds the Basis-From-Convergence Theorem, turning normal-form representatives into an actual basis once the modulo data is shown scalar-coherent on reduced foams.","pith_inferences":["The confluence computations force relations among the scalars X, Y, Z only at critical branchings, suggesting that many scalar deformations beyond the two named variants should also admit bases; this deformation-theoretic reading is implicit in the paper's perspective section.","The branch classification modulo is structured enough that it could be turned into a Buchberger-style completion algorithm, making basis theorems for diagrammatic algebras computer-checkable in future work.","Because the identification of normal forms with reduced foams is deferred to the companion thesis, a direct finite enumeration for small d would give an independent check of that load-bearing step.","The same tamed-congruence technology may transfer to super-2-categories such as the 2-Kac–Moody superalgebra, where non-monomial modulo rules currently block the theory."],"forward_implications":["Hom-spaces of GFoam_d are free k-modules with bases indexed by subsets of boundary circle components, so the odd Khovanov homology construction in [SV23] rests on a proven foundation.","A second deformation GFoam'_d, obtained by admissible scalar choices, satisfies the same basis theorem and corresponds topologically to type Y in odd Khovanov homology.","The rewriting machinery gives intrinsic, algorithmic basis proofs without a concrete faithful representation, opening a route to hom-basis theorems for other diagrammatic algebras.","The classified critical branchings yield explicit coherence data and syzygies for GFoam_d, paving the way toward studying higher structures and deformations of diagrammatic algebras."],"supporting_citations":[{"why":"Defines the graded-2-category GFoam_d, states the basis conjecture, and shows that the higher-representation-theoretic construction of odd Khovanov homology relies on it.","marker":"[SV23]"},{"why":"Supplies the deferred proof of Lemma 4.14, the identification of T-normal forms with reduced foams that the basis argument depends on.","marker":"[Sch24]"},{"why":"Provides the framework of n-sesquicategories and Gray polygraphs that the paper linearizes and extends to rewriting modulo.","marker":"[FM22]"},{"why":"Introduces rewriting modulo in diagrammatic algebras, the inspiration for treating pivotality and other categorical properties as unoriented modulo rules.","marker":"[Dup22]"},{"why":"Develops linear rewriting theory whose Basis-From-Convergence principle is adapted here to the higher modulo setting.","marker":"[GHM19]"},{"why":"Supplies the earlier higher linear rewriting theory that the paper refines with tamed congruence and context-dependent termination.","marker":"[All18a]"}],"fun_headline_variants":["First proof of basis theorem for graded gl2-foams via modular rewriting","Modular rewriting yields first basis proof for graded gl2-foams","Graded gl2-foam basis shown via rewriting modulo"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof relies on Lemma 4.14, stated without proof and deferred to the author's thesis, that the rewriting-normal forms of the subsystem T are exactly the reduced foams; if that identification fails, the basis theorem does not follow from the rewriting argument.","fun_headline_variants_meta":{"raw":{"variants":["First proof of basis theorem for graded gl2-foams via modular rewriting","Modular rewriting yields first basis proof for graded gl2-foams","Graded gl2-foam basis shown via rewriting modulo"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00024,"raw_usage":{"total_tokens":1486,"prompt_tokens":882,"completion_tokens":604,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":498,"completion_tokens_details":{"reasoning_tokens":543}},"tokens_in":498,"tokens_out":604,"duration_ms":5726,"temperature":1.0,"reasoning_tokens":543,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T10:07:58.150053+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find two parallel 1-morphisms W, W' in GFoam_d for which a reduced family satisfies a nontrivial linear relation in Hom_GFoam_d(W,W'), or exhibit a reduced foam that is not a T-normal form (or a T-normal form that is not reduced); the second check is a direct inspection of the rewriting rules and would settle the deferred Lemma 4.14.","supporting_citations":[],"review_version":1}