{"id":"28c659a0-f4e1-4bc1-b1e3-fd54f51c1550","arxiv_id":"2509.09657","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For the parameterized circuit classes para-AC0 and para-AC0-up-arrow, linear-, logtime-, and FO-uniform circuit families define identical complexity classes.","lead":"The paper defines parameterized versions of linear, logtime, and first-order uniformity for Boolean circuit families, and proves that for the shallow parameterized classes para-AC0 and para-AC0-up-arrow they all yield the same complexity classes. This gives a convenient way to verify uniformity claims in parameterized circuit complexity without wrestling with logtime machines.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The logtime→FO inclusion (Theorem 21, (2)⇒(3)) rests on Theorem 12, which is stated but never proved; the paper only says it can be proved like Lemma 24.","rationale":"The reader's weakest_assumption identifies the unproved Theorem 12 as the key load-bearing premise, and the text confirms this: Lemma 20's proof is the only place where logtime-D-uniformity is shown to imply FO-D-uniformity, and it passes through Para(linear-BD-uniform AC0) = Para(FO), which requires Theorem 12. The paper itself flags the stronger family-level analogue as open, so Theorem 12 is not a harmless folklore citation. A second issue, the apparent misapplication of Theorem 14 in Lemma 25, is real but less damaging: that step can be repaired using Theorem 12, Lemma 24, and Lemma 18, all already in the paper. The conditional verdict is appropriate: the central claim is plausible and the gaps are likely fixable, but the current manuscript does not contain a complete proof of a theorem on which the main result directly depends. I found no reason to reject the paper's overall approach, and the class-level nature of the equivalences is stated honestly in the conclusion.","tokens_in":21502,"tokens_out":29754,"duration_ms":335348,"concrete_test":"Write out the missing proof of Theorem 12 by specializing Lemma 24 to the non-parameterized case (i.e., take k=0 and apply the simgate construction) and combining it with Lemma 18. Verify that this proof does not invoke Lemma 20, Theorem 21, or any assumption equivalent to the open DTIMER(n)=DTIME(n) problem. If the derivation can be completed without such an assumption, the main theorem is salvageable by reorganizing the proof; if it cannot, the logtime→FO direction is unsupported.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Lemma 20 derives logtime-D-uniform ⇒ FO-D-uniform via the chain: DTIMER(log n + g(k)) ⊆ linear-BD-uniform para-AC0 (Lemma 19) = Para(linear-BD-uniform AC0) (Theorem 14) = Para(FO) by Theorem 11 and Theorem 12 = para-FO. The step Para(linear-BD-uniform AC0) = Para(FO) depends entirely on Theorem 12, the class-level equality linear-BD-uniform AC0 = logtime-D-uniform AC0. But Theorem 12 is asserted as a 'folklore extension' and no proof is included; the paper says only that it can be proved similarly to Lemma 24. Since the stronger family-level equivalence is explicitly stated to be open in the same section, the class-level claim is not a routine corollary of the cited literature. If Theorem 12 is not supplied, the inclusion logtime-D-uniform para-AC0 ⊆ FO-D-uniform para-AC0 is not established, and the central equality in Theorem 21 collapses. The later Lemma 24 likely provides a route to prove Theorem 12, but the manuscript does not make that dependence explicit or prove it before Lemma 20 uses it. This is a genuine missing-support issue, not merely a stylistic gap.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines parameterized analogues of three direct uniformity conditions for Boolean circuit families—linear-BD-uniformity, logtime-D-uniformity, and FO-D-uniformity—along with extended variants, and proves that for the shallow parameterized classes para-AC0 and para-AC0^↑ these conditions induce the same complexity classes (Theorem 21 and Corollary 31). The proof strategy is: first show linear-BD ⇒ logtime-D ⇒ FO-D for individual circuit families (Lemmas 18 and 20); then prove the reverse inclusions up to equivalent families by a layered simulation using 'simgates' that evaluate gates of a logtime- or FO-uniform circuit by querying its direct connection language; a substitution lemma (Lemma 23) is used to compose the query-answering circuits. Applications to uniformity claims in the recent parameterized-circuit literature are discussed in Sections 6 and 7.","tokens_in":21804,"tokens_out":9492,"duration_ms":110110,"significance":"If the identified proof gaps are repaired, this is a useful and timely contribution. It removes a real ambiguity in the parameterized circuit-complexity literature, where logtime-uniformity is often invoked informally or left as an exercise, and it extends the classical Barrington–Immerman–Straubing equivalence to the parameterized setting, including the non-constant-depth class para-AC0^↑. The simgate construction and the substitution lemma are interesting technical tools in their own right. The paper also contains substantial appendix proofs and is honest about limitations, noting that the equivalences hold at the class level rather than the family level and that the conversion has a polynomial overhead gap.","major_comments":[{"comment":"Theorem 12, the equality linear-BD-uniform AC0 = logtime-D-uniform AC0, is stated as folklore with only 'can be proved similarly' and no proof. This equality is load-bearing: Lemma 20 derives logtime-D-uniform ⇒ FO-D-uniform through the chain Lemma 19 → Theorem 14 → Theorems 11 and 12 → para-FO, and the step '= Para(FO)' depends entirely on Theorem 12. The manuscript itself notes that the stronger family-level equivalence is open, so Theorem 12 is not a routine corollary of cited results. Please supply a proof (a non-parameterized version of Lemma 24 appears to provide exactly the needed argument), or an explicit citable source containing a proof, and state this dependency before Lemma 20 uses it.","section":"§2.5, Theorem 12; used in §3, Lemma 20"},{"comment":"The step 'Theorem 11 gives that (LD(C),π4) is in Para(logtime-D-uniform AC0), which by Theorem 14 is equal to logtime-D-uniform para-AC0' misstates Theorem 14. Theorem 14 is stated for linear-BD-uniform para-AC0 and Para(linear-BD-uniform AC0), not for logtime-D-uniform para-AC0. The intended conclusion can be obtained only by additionally applying Theorem 12 and Lemma 18 (or by proving a logtime analogue of Theorem 14). As written, this is a direct misapplication at a load-bearing point of the proof of (3)⇒(1) in Theorem 21. Please rewrite this step and make the full chain explicit.","section":"§4.2, Lemma 25"}],"minor_comments":[{"comment":"The definition of FO-D-uniformity says '(LD(C),π4) is in para-FO', but Definition 1 requires a parameter function κ : 2* → N, while π4 is a string projection. The intended parameter is |π4(w)|, i.e. |z'|. Please add an explicit convention that π4 is shorthand for the parameter function κ(w)=|π4(w)|, consistently with Table 1.","section":"§3, Definition 17"},{"comment":"The line 'From the inclusions ... = Para(FO) by Theorems 11 and 12' mixes inclusions and equalities; what is meant is a chain of class inclusions and equalities. Clarify the notation to avoid suggesting that Theorem 12 is being cited for an inclusion rather than a class equality.","section":"§3, Lemma 20"},{"comment":"In the runtime analysis, the text says 'this takes O(g(k) log log n) bits' and later 'also O(g(k) log log n) bits for some computable g'. These should be 'time', not 'bits'. Also, the sentence 'Managing the finite number of special steps ... take O(log n + g(k)) time each' should say 'takes' for grammatical agreement.","section":"Appendix B.4, proof of Lemma 30"},{"comment":"The final subcircuit that propagates the output of the correct simgate is described only briefly. Since this is part of the construction whose uniformity is being claimed, a sentence explaining how the output-gate information is obtained from LD(C) in the same complexity bound would help the reader verify that the admissible numbering and the connection language check remain uniform.","section":"§4.2, Lemma 24"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for cs.CC and addresses a genuine gap in the parameterized circuit-complexity literature. The main theorem is credible and the simgate construction is promising, but the missing proof of Theorem 12 and the misapplication of Theorem 14 in Lemma 25 are load-bearing and need to be fixed before publication. I do not see grounds for rejection: both issues are repairable within the manuscript's own framework, and the appendix already contains most of the necessary technical material."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague, here's my take on arXiv:2509.09657.\n\nThe paper does something genuinely useful: it gives the first systematic treatment of uniformity for parameterized Boolean circuit classes. The definitions of linear-BD-, logtime-D-, and FO-D-uniformity in the parameterized setting are natural, and the main theorem (for para-AC0 and para-AC0↑ these three notions yield the same classes) is exactly the kind of toolkit the area needs. The simgate layering construction is new and, as far as I can tell, sound in its own right. The authors also deserve credit for being straight about what they don't prove—the class-level versus family-level distinction and the size blow-up in their conversion are stated plainly.\n\nThat said, there are two holes in the proof as written, and both are load-bearing. First, Lemma 20 uses Theorem 12, the folklore equivalence linear-BD-uniform AC0 = logtime-D-uniform AC0, to chain logtime-D-uniformity into FO-D-uniformity. The paper only says it can be proved 'similarly' to Lemma 24, and points out that the stronger family-level equivalence is actually open. Since the central equality in Theorem 21 rests on this step, the proof is incomplete without a proof of Theorem 12. The authors likely have the argument—the simgate construction in Lemma 24 should adapt—but it needs to be written out.\n\nSecond, Lemma 25's proof appears to misapply Theorem 14. Theorem 14 says linear-BD-uniform para-AC0 equals Para(linear-BD-uniform AC0). The proof of Lemma 25 uses it to jump from Para(logtime-D-uniform AC0) to logtime-D-uniform para-AC0. That is not what the theorem states. There may be an intended use of Theorem 12 there, or a separate argument, but as written the implication from FO-D-uniform to linear-BD-uniform is not established by the cited results.\n\nThese are not fatal objections to the ideas. I suspect both can be fixed with the techniques already in the paper. But they are genuine gaps, not stylistic ones, and the main theorem does not go through as written. A referee should ask for a real proof of Theorem 12 and a corrected chain in Lemma 25.\n\nBottom line: this is a solid, niche contribution for people working on parameterized circuit complexity and descriptive complexity. The definitions alone could become the standard reference. I would send it to a serious referee rather than desk reject, and condition acceptance on filling those two holes.","headline":"A real contribution to parameterized uniformity, but the main proof rests on an unproved folklore claim and a misapplied theorem—both likely fixable, so it should go to peer review with requests for revision.","tokens_in":22282,"tokens_out":3073,"would_cite":true,"duration_ms":30387,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q15","68Q19"],"pacs":[],"model":"deepseek-v4-flash","headline":"For shallow parameterized circuit classes, three different uniformity conditions — linear-time, logtime, and first-order — define the same class of problems.","keywords":["parameterized complexity","circuit complexity","uniformity","AC⁰","para-AC⁰","logtime uniformity","first-order definability","circuit families"],"falsifier":"A separation of the two non-parameterized classes in Theorem 12 — an AC⁰ language with a linear-BD-uniform circuit family but no equivalent logtime-D-uniform family — would falsify the parameterized equivalence, since the non-parameterized case embeds into para-AC⁰ with constant parameter. The first place to look is whether the paper's simgate construction actually preserves logtime-uniformity when depth and parameter are constant, since that construction is the only evidence given for Theorem 12.","tokens_in":21402,"feed_emoji":"⚙️","tokens_out":8215,"duration_ms":92821,"temperature":0.7,"pith_summary":"In parameterized circuit complexity, shallow circuit classes like para-AC⁰ and para-AC⁰↑ are usually defined with a uniformity condition that says the circuits must be easy to construct, but the precise condition used in the literature is often left vague or unproved. The paper formalizes parameterized analogues of three standard uniformity conditions — linear-time (with bound f(k)+n), logtime random-access, and first-order definable — and proves that, when imposed on para-AC⁰ or para-AC⁰↑, they all yield the same class of parameterized problems. The main result (Theorem 21) is the equality of the three classes; an extended version covers uniformity notions that describe paths through circuits. This matters because logtime-uniformity is technical and rarely proved directly: the theorem makes FO-definability a sufficient certificate for the existence of a logtime-uniform family, which substantiates uniformity claims in recent literature and repairs a known gap. The proof works by a layered 'simgate' construction: from an FO-uniform or logtime-uniform family, one builds a linear-BD-uniform family by simulating each gate with a block that queries the original circuit's connection language.","feed_headline":"First-order descriptions yield logtime-uniform shallow circuits","feed_subtitle":"For para-AC⁰ and para-AC⁰↑, all three uniformity conditions pick out the same problems.","key_machinery":"The load-bearing mechanism is the parameterized direct connection language LD(C), the set of strings ⟨G,a,p,z,z′⟩ describing gate types and predecessor relations of each circuit Cn,k, together with its binary version LBD(C). Uniformity conditions are defined by the decision complexity of these languages: linear-BD-uniformity requires DTIME(n+f(k)), logtime-D-uniformity requires DTIMER(log n+f(k)) on random-access Turing machines, and FO-D-uniformity requires the language to be in parameterized first-order logic. The equivalences are proved by a substitution lemma (Lemma 23) showing that linear-BD-uniform families are closed under replacing marked gates by other linear-BD-uniform families, an","core_discovery":"The central claim is Theorem 21: for both para-AC⁰ and para-AC⁰↑, the classes of parameterized problems decided by linear-BD-uniform, logtime-D-uniform, and FO-D-uniform circuit families coincide. In other words, the three parameterized uniformity conditions — defined here for the first time in a unified way — are interchangeable at the level of complexity classes for shallow families. The paper also proves the analogous statement for extended uniformity notions (logtime-E-uniform and FO-E-uniform), where the connection language contains paths, and derives the self-uniformity corollary that (FO-D-uniform para-AC⁰↑)-uniform para-AC⁰↑ equals FO-D-uniform para-AC⁰↑. The authors intend this as a","pith_inferences":["The proof actually shows more than the statement: the simgate construction gives an explicit algorithm converting an FO-D-uniform description into a linear-BD-uniform family, so in principle one can mechanically extract a logtime-uniform family rather than merely knowing one exists.","Because the conversion costs a polynomial blow-up in size (roughly from O(f(k)n^c) to O(f'(k)n^{3c+1})), the equivalence is not a work-preserving simulation; any theorem that relies on exact circuit sizes for parameterized parallel complexity would need a different, finer-grained argument.","The same layered-simulation strategy may transfer to other parameterized circuit classes where a substitution lemma holds, so the 'three uniformities are one' phenomenon could recur for e.g. parameterized ACC or NC-like classes, though the paper does not claim this."],"forward_implications":["To prove logtime-uniformity of a shallow parameterized circuit family, it suffices to give a first-order description of its direct connection language; this is typically far easier than designing a logtime random-access Turing machine.","The equivalence holds separately for para-AC⁰ (constant depth) and para-AC⁰↑ (depth f(k)), so the convenience applies to the full range of shallow parameterized circuit classes.","Extended uniformity notions that trace paths in circuits — logtime-E-uniform and FO-E-uniform — collapse to the same classes as well, so path-based uniformity adds no extra power for these classes.","The result gives (FO-D-uniform para-AC⁰↑)-uniform para-AC⁰↑ = FO-D-uniform para-AC⁰↑, meaning a family that is uniform in a strong sense is itself FO-D-uniform.","The framework yields a descriptive-complexity counterpart: the union over computable f of para-FO[f(k)] equals FO-D-uniform para-AC⁰↑, linking logtime-uniformity to iterated first-order logic."],"fun_headline_variants":["Three uniformity notions, one class for shallow parameterized circuits","Uniformity trifecta: linear, logtime, FO all equal for para-AC⁰","Proving logtime uniformity? Use FO descriptions for shallow families","Parameterized uniformity: one proof for three conditions in shallow circuits","Shallow parameterized circuits: uniformity conditions collapse"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof that logtime-D-uniformity implies FO-D-uniformity for parameterized families rests on the unproved folklore equivalence between linear-BD-uniform AC⁰ and logtime-D-uniform AC⁰ (Theorem 12); if that non-parameterized equivalence should fail, the main chain collapses even though the paper states it can be proved by the same simgate argument.","fun_headline_variants_meta":{"raw":{"variants":["Three uniformity notions, one class for shallow parameterized circuits","Uniformity trifecta: linear, logtime, FO all equal for para-AC⁰","Proving logtime uniformity? Use FO descriptions for shallow families","Parameterized uniformity: one proof for three conditions in shallow circuits","Shallow parameterized circuits: uniformity conditions collapse"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000887,"raw_usage":{"total_tokens":3636,"prompt_tokens":687,"completion_tokens":2949,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":431,"completion_tokens_details":{"reasoning_tokens":2859}},"tokens_in":431,"tokens_out":2949,"duration_ms":23177,"temperature":1.0,"reasoning_tokens":2859,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T18:44:50.931395+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A separation of the two non-parameterized classes in Theorem 12 — an AC⁰ language with a linear-BD-uniform circuit family but no equivalent logtime-D-uniform family — would falsify the parameterized equivalence, since the non-parameterized case embeds into para-AC⁰ with constant parameter. The first place to look is whether the paper's simgate construction actually preserves logtime-uniformity when depth and parameter are constant, since that construction is the only evidence given for Theorem 12.","supporting_citations":[],"review_version":1}