{"id":"c27fe49d-ae55-4cfb-85c1-22d3452a1075","arxiv_id":"2511.03388","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Monotone bounded-depth formula size for graph homomorphism polynomials equals n^{λ_Δ(H)}, where λ_Δ(H) is the minimum cost of a baggy elimination tree of product depth Δ.","lead":"The paper introduces a new graph decomposition, baggy elimination trees, and proves that the smallest monotone formula for colored graph isomorphism polynomials at fixed multiplication depth is exactly n to a new graph parameter. This completes a research program that had already characterized monotone circuits, ABPs, and unbounded-depth formulas by graph parameters.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Definition 7 prints 'iff' where the proof and examples need only 'edge ⇒ comparable'; λ_Δ(H) as literally defined is not the parameter Theorem 1 proves.","rationale":"The reader's weakest assumption identifies exactly the same load-bearing concern: Definition 7's 'if and only if' is contradicted by the paper's own P7 example and by the parse-tree lifting construction, and the central theorem depends on the one-directional interpretation. I agree with the reader's conditional verdict. The theorem's overall structure — a characterization of Δ-product-depth monotone formula size by the minimum cost of a one-way baggy elimination tree — is plausible and the proof sketches for the upper and lower bounds are coherent once the definition is corrected to 'edge ⇒ comparable'. However, the paper as submitted is not self-consistent: Theorem 1 refers to a parameter that is not the one the proof handles. This is a genuine correctness risk for the central claim, though it is repairable by a one-word fix.\n\nA secondary issue is the off-by-one error in Sections 5–6. For F_{b,Δ+1}, the standard elimination tree has Δ+1 singleton bags on a root-to-leaf path, with the last bag non-core, so the cost is Δ+1 and product depth Δ. The same lower bound follows from treedepth considerations. Thus the claimed Θ(n^Δ) in Section 5 should be Θ(n^{Δ+1}). This does not invalidate the separation statements (the stated lower bounds are weaker than what the corrected bound gives), but it does affect the corollaries as written. The reader's conditional verdict remains appropriate; a revision fixing Definition 7 and the parameter choices in Sections 5–6 would likely make the main theorem and applications correct.","tokens_in":7579,"tokens_out":24411,"duration_ms":217620,"concrete_test":"Take the Figure 1 baggy elimination tree for P7 and check it against Definition 7 as printed: enumerate all pairs in the same bag (e.g., {2,4}) and all ancestor-descendant pairs (e.g., {1,4}) and test whether each is an edge of P7. Under the literal 'iff' the tree is invalid; under the one-way reading it is valid. Then, as a sharper check, re-derive the LCA-lifting lower-bound argument in Section 4 while replacing the 'iff' in Definition 7 by the one-way implication 'if {u,v} ∈ E(H), then u and v are in the same bag or in ancestor-descendant bags'. If the constructed B is accepted without any step requiring the converse, the theorem as proven is for the corrected parameter and the printed Definition 7 must be amended.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition 7 defines a baggy elimination tree by the condition that {u,v} ∈ E(H) iff u and v are in the same bag or in ancestor-descendant bags. This equivalence is the basis for the parameter λ_Δ(H) appearing in Theorem 1. But the paper's own Example 1/Figure 1 for P7 violates the 'if' direction: the root bag {2,4,6} contains non-adjacent vertices, and non-adjacent pairs such as (1,4) are in ancestor-descendant bags. Under the literal printed definition this tree is invalid, so λ_Δ(P7) would be a different — presumably larger — quantity, and the claimed Θ(n^{λ_Δ(H)}) upper bound is not the one being proved.\n\nThe upper-bound construction in Section 4 only needs the forward direction: edges within a bag or between ancestor and descendant bags are exactly the edges whose variables are multiplied, while non-edges placed in comparable bags simply generate no monomial and cause no obstruction. The lower-bound LCA-lifting argument also proves only the forward direction: for an edge {u,v}, the leaf for the variable x_{(u,·),(v,·)} is a descendant of both LCA(u) and LCA(v), forcing those two LCAs to be comparable; nothing forces incomparable vertices to have incomparable LCAs. Thus the theorem's proof establishes the result for the one-way condition, not for the printed 'iff'. The central characterization is internally inconsistent as written: the statement of Theorem 1 uses a parameter that is not the one constructed in its own proof.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces the notion of a baggy elimination tree (BET), a generalization of elimination trees in which each node carries a bag of vertices, together with two parameters: product depth and cost. It defines λ_Δ(H) as the minimum cost of a BET for H of product depth at most Δ, and claims in Theorem 1 that the Δ-product-depth monotone formula complexity of the coloured isomorphism polynomial ColIso_H is Θ(n^{λ_Δ(H)}) for every connected H on more than two vertices. The upper bound is proved by a recursive formula whose structure mirrors a BET; the lower bound is proved by lifting a parse tree to a BET. The paper then derives two applications: a separation between bounded-depth monotone circuits and formulas, and a depth hierarchy for monotone formulas.","tokens_in":8006,"tokens_out":29197,"duration_ms":281946,"significance":"If Theorem 1 is correct, it supplies the missing bounded-depth formula characterization in the programme of Komarath–Pandey–Rahul and Bhargav–Chen–Curticapean–Dwivedi, and the BET cost is a new graph parameter that connects monotone formula complexity to tree structure. The proof strategy is plausible and the lower-bound construction is nontrivial. However, as written the paper contains a load-bearing inconsistency in the central definition and off-by-one errors in both application sections. The central theorem appears defensible after a local fix, but the advertised applications are not established as stated.","major_comments":[{"comment":"Definition 7 requires that {u,v} ∈ E(H) if and only if u and v are in the same bag or in ancestor-descendant bags. This is internally contradicted by Example 1 and Figure 1: the root bag {2,4,6} contains non-adjacent vertices, and non-adjacent pairs such as (1,4) are in ancestor-descendant bags. The parse-tree lifting in Section 4 (Figure 2) also places non-adjacent vertices in comparable bags. All proofs use only the forward direction: every edge must have its endpoints in the same bag or in ancestor-descendant bags. Under the literal 'iff' definition, the example tree is invalid and λ_Δ is a different, larger parameter; Theorem 1 would not apply. The definition must be changed to the one-way condition. This is load-bearing for the main theorem.","section":"Section 3, Definition 7"},{"comment":"The text states that the Δ-product-depth monotone formula complexity of ColIso_{F_{b,Δ+1}} is Θ(n^Δ) by Theorem 1 and the treedepth lower bound. This is off by one. F_{b,Δ+1} has treedepth Δ+1. As the paper itself notes in Section 3, any BET of cost c can be converted to an elimination tree of cost c, so λ_Δ(F_{b,Δ+1}) ≥ Δ+1. The natural elimination tree has product depth Δ and cost Δ+1, so λ_Δ(F_{b,Δ+1}) = Δ+1. Therefore Theorem 1 gives Θ(n^{Δ+1}), not Θ(n^Δ). Consequently, the derivation of Theorem 2 is incorrect; the claimed Ω(N^{Δ/2}) lower bound happens to remain true, but the stated Θ(n^Δ) and the 'almost-optimal' claim are not supported.","section":"Section 5, Theorem 2"},{"comment":"The proof of Theorem 4 asserts that ColIso_{F_{b,Δ+1}} has O(n^Δ)-size monotone formulas of product depth Δ. This repeats the same off-by-one: the correct upper bound is O(n^{Δ+1}). With this correction, the claimed lower bound Ω(n^{b+Δ}) for product depth Δ−1 does not imply Ω(s(N)^k) for s(N) of order n^{Δ+1} (or n^Δ), because (b+Δ)/(Δ+1) = k − (k−1)/(Δ+1) < k. Thus Theorem 4's depth hierarchy is not established by the given construction. The family or the parameter b must be reworked, or the theorem statement weakened.","section":"Section 6, Theorem 4"}],"minor_comments":[{"comment":"The sentence 'Assume without loss of generality that 1,...,d are the vertices of H appearing in g and its ancestors' should be phrased as 'at least these vertices' or 'the first d vertices on that path', because the path chosen may contain more than d vertices. The argument still works, but the current wording is imprecise.","section":"Section 4, lower bound"},{"comment":"The example gives an O(n^4) formula of product depth two for P7, but a smaller O(n^3) formula of product depth two exists via the standard elimination tree of P7. This is not an error, but the example may mislead readers about the optimality of the construction.","section":"Section 3, Example 1"},{"comment":"The remark claims optimality 'up to constant factors independent of Δ in the exponent of n'. Even after correcting the formula complexity to n^{Δ+1}, the gap between the circuit upper bound O(n^2) and the formula lower bound n^{Δ+1} is a factor of Δ+1 in the exponent, not a constant independent of Δ. The wording should be revised.","section":"Section 5, Remark 2"},{"comment":"The definition of product depth counts internal nodes even if their bag contains only pendant vertices. This is a valid choice, but it interacts subtly with the off-by-one issues in Sections 5–6; the paper would benefit from an explicit example showing the product depth of the natural elimination tree of F_{b,Δ+1}.","section":"Section 3, Definition 7"}],"recommendation":"major_revision","confidential_remarks":"The main theorem appears salvageable after fixing Definition 7 to the one-way condition, and the lower-bound proof is structurally sound. However, the two application theorems contain systematic off-by-one errors that are not cosmetic: Theorem 4's hierarchy claim, as stated, does not follow from the given family. The authors will need to either find a different construction for the depth hierarchy or substantially weaken the theorem. This is more than a local typo fix, but it is not a rejection of the central characterization."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe short version: this paper introduces a genuinely new graph parameter, baggy elimination tree cost at bounded product depth, and uses it to give the missing bounded-depth formula characterization in the programme started by Komarath–Pandey–Rahul and continued by Bhargav–Chen–Curticapean–Dwivedi. The main theorem is plausible and the proof structure is credible. But the submitted version has a load-bearing definitional error and off-by-one mistakes in the applications. It needs revision, not acceptance.\n\nWhat is good: the baggy elimination tree is a natural generalization of elimination trees, and defining λ_Δ as the minimum cost at product depth Δ gives exactly the right kind of graph parameter for formulas. The upper bound (recursive formula following the tree) is clean and I believe correct. The lower bound uses the LCA-lifting technique from [7] and, once you interpret the definition the way the proof uses it, the argument holds together. This is a real contribution to the subfield.\n\nThe soft spots are serious. Definition 7 says an edge exists iff its endpoints are in the same or ancestor-descendant bags. But the paper's own example for P7 puts non-adjacent vertices 2,4,6 together in the root bag, and both the upper and lower bound proofs only need the forward direction (edge implies comparable). As literally defined, λ_Δ is a different quantity and the theorem does not match its proof. The fix is easy — change 'iff' to 'if' — but without it, the central statement is incoherent.\n\nThe applications also have off-by-one errors. Section 5 claims ColIso_{F_{b,Δ+1}} has Θ(n^Δ) formula complexity at product depth Δ; the correct exponent is Δ+1 by a simple cost argument. Section 6's Theorem 3 proves a lower bound for F_{b,Δ+2}, but Theorem 4 uses F_{b,Δ+1} with b=(k−1)Δ+1; the indices do not line up. These errors shift the separation and hierarchy exponents, though I suspect the qualitative claims survive a careful fix.\n\nFor whom? Anyone working on monotone algebraic complexity or graph homomorphism polynomials. The conceptual framework is worthwhile and I would cite the corrected version. As submitted, it deserves a serious referee, but the referee should be told to focus on Definition 7 and Sections 5–6.","headline":"A genuinely new characterization of bounded-depth monotone formula complexity via baggy elimination trees, with a fixable but load-bearing definitional error and off-by-one mistakes in the applications.","tokens_in":8420,"tokens_out":9182,"would_cite":true,"duration_ms":85745,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"For any connected pattern graph H with more than two vertices, the smallest monotone formula of product depth Δ computing the colored isomorphism polynomial ColIso_H has size Θ(n^{λ_Δ(H)}), where λ_Δ(H) is the minimum cost of a baggy elimin","keywords":["graph homomorphism polynomials","colored isomorphism polynomials","baggy elimination tree","bounded-depth monotone formulas","treedepth","monotone circuit vs formula separation","algebraic complexity","product depth"],"falsifier":"Take a small pattern such as the 4-cycle C_4 and compute λ_2(C_4) under the one-way reading; then determine the true minimum size of a product-depth-2 monotone formula for ColIso_{C_4}. If the exponent of n in that size is not λ_2(C_4), the main theorem is false.","tokens_in":7503,"feed_emoji":"🌳","tokens_out":7734,"duration_ms":71637,"temperature":0.7,"pith_summary":"This paper pins down the exact (up to constant factors) size of monotone arithmetic formulas of bounded product depth that compute the colored isomorphism polynomial of a pattern graph H. It introduces baggy elimination trees, a generalization of the elimination trees behind treedepth, and defines λ_Δ(H) as the cheapest such tree of product depth Δ. The main theorem states that the Δ-product depth monotone formula complexity of ColIso_H is Θ(n^{λ_Δ(H)}) for every connected H with more than two vertices. This completes a program that had already characterized monotone circuits by (bounded-depth) treewidth and monotone algebraic branching programs by (bounded-depth) pathwidth, leaving formulas as the last model. The characterization yields a near-optimal circuit-vs-formula separation at every fixed product depth and a strict depth hierarchy for monotone formulas.","feed_headline":"Baggy tree cost dictates bounded-depth formula size","feed_subtitle":"The smallest depth-Δ monotone formula has size n^{λ_Δ(H)}, closing the bounded-depth complexity picture.","key_machinery":"Baggy elimination trees: a rooted tree whose nodes carry bags (subsets of vertices of H) covering V(H), such that every edge of H appears either inside one bag or across ancestor-descendant bags. The cost of a root-to-leaf path is the sum of its bag sizes; product depth counts internal nodes on the path, with non-core leaves (bags containing only pendant vertices) excluded. λ_Δ(H) is the minimum over all baggy elimination trees of product depth at most Δ of the maximum path cost. This parameter does the work of the proof: the upper bound converts an optimal tree directly into a formula, and the lower bound converts any parse tree into a tree with cost bounded by the exponent of n, forcing th","core_discovery":"The paper's central claim is that the bounded-depth monotone formula complexity of the colored isomorphism polynomial ColIso_H is governed exactly by a new graph parameter, λ_Δ(H). A baggy elimination tree for H is a rooted tree in which each node carries a bag of vertices of H and every edge of H has its two endpoints in the same bag or in ancestor-descendant bags; the product depth is the maximum number of internal nodes on a root-to-leaf path (excluding leaves that contain only pendant vertices), and the cost of a path is the sum of its bag sizes. λ_Δ(H) is the minimum possible cost of any such tree with product depth at most Δ. Theorem 1 proves that the Δ-product depth monotone formula s","pith_inferences":["A natural next step is to study the complexity of computing λ_Δ(H); an efficient algorithm for fixed Δ would turn the characterization into a practical predictor of monotone formula size for a given pattern H.","This suggests the parse-tree-to-decomposition lower bound is transferable: other polynomials whose monomials are products indexed by the edges of a pattern graph (e.g., subgraph polynomials) should exhibit the same λ_Δ characterization.","The near-tight circuit-vs-formula gap suggests that the real obstruction is the gap between bounded-depth treewidth and the new baggy-elimination-tree cost; graphs where those two parameters diverge more sharply may yield even stronger separations than the ones proven here."],"forward_implications":["For every fixed connected H with more than two vertices, the Δ-product-depth monotone formula size of ColIso_H is Θ(n^{λ_Δ(H)}), so the graph parameter completely determines the exponent.","The characterization completes the programme that had already linked monotone circuits to treewidth variants and monotone ABPs to pathwidth variants, leaving formulas as the final model.","Theorem 2 gives a near-optimal circuit-vs-formula separation: at every fixed product depth, some constant-degree family has O(N)-size monotone circuits of depth Δ but requires Ω(N^{Δ/2})-size monotone formulas of the same depth.","Theorem 4 establishes a strict depth hierarchy: for any Δ≥1 and constant k≥2, a constant-degree family can be computed by O(s(N))-size formulas of depth Δ but requires Ω(s(N)^k)-size formulas of depth Δ−1.","Because λ_Δ(H) is always at most the treedepth of H, the new parameter refines treedepth and recovers the known unbounded-depth treedepth characterization as a special case."],"fun_headline_variants":["λ_Δ(H) pins down depth-Δ monotone formulas","Baggy tree cost sets depth-Δ formula size exactly","New parameter completes bounded-depth complexity trichotomy","Depth-Δ formula size = n^{λ_Δ(H)} for homomorphism polys","Bounded-depth formula complexity solved via baggy trees"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The theorem stands or falls with the intended one-way reading of a baggy elimination tree: every edge of H must be covered by a bag or by ancestor-descendant bags, but non-edges may also sit in such positions; the printed 'if and only if' would define a different parameter and break the Θ(n^{λ_Δ(H)}) result.","fun_headline_variants_meta":{"raw":{"variants":["λ_Δ(H) pins down depth-Δ monotone formulas","Baggy tree cost sets depth-Δ formula size exactly","New parameter completes bounded-depth complexity trichotomy","Depth-Δ formula size = n^{λ_Δ(H)} for homomorphism polys","Bounded-depth formula complexity solved via baggy trees"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000232,"raw_usage":{"total_tokens":1407,"prompt_tokens":909,"completion_tokens":498,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":653,"completion_tokens_details":{"reasoning_tokens":413}},"tokens_in":653,"tokens_out":498,"duration_ms":5519,"temperature":1.0,"reasoning_tokens":413,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T23:59:10.144574+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a small pattern such as the 4-cycle C_4 and compute λ_2(C_4) under the one-way reading; then determine the true minimum size of a product-depth-2 monotone formula for ColIso_{C_4}. If the exponent of n in that size is not λ_2(C_4), the main theorem is false.","supporting_citations":[],"review_version":1}