{"id":"d7cbee55-98e6-4165-9e0d-fb2a29bf1fd3","arxiv_id":"2502.00676","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For every fixed k and every MSO2 graph property, there is an optimal O(log n)-bit proof labeling scheme for graphs of pathwidth at most k, implying O(log n)-bit certification of F-minor-free graphs for any fixed forest F.","lead":"The paper presents proof labeling schemes that certify any property expressible in monadic second-order logic on graphs with bounded pathwidth using O(log n)-bit labels. This is optimal and answers an open question about locally certifying forest-minor-free graphs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: after stress-testing Proposition 4.6 and the recursive certification, the argument appears sound.","rationale":"The reader's weakest_assumption correctly identifies Proposition 4.6 as the most intricate and load-bearing part of the proof, and I agree that a hidden congestion factor there would break the O(log n) label size. However, on detailed inspection the congestion accounting appears sound: the order of v*_C along P within each class is forced, prefix/suffix congestion inside a component is additive with the inductive bound, and the recurrence g(k) = 2 + g(k-1) + 2k f(k-1) accounts for all contributions. I also examined the certification of T-nodes in Lemma 6.5 and found that the potentially unbounded depth of the internal tree T does not cause label blow-up, because each edge carries only the basic information of its own node and the immediate children's Tree-merge values. The simulation of virtual edges in Theorem 1 can be implemented by having each vertex filter labels for which it is an endpoint, so the G' edge-label verifier is faithfully simulated. The observed typos are local and do not change the proofs. Overall, the central claim withstands this stress test, and the reader's ACCEPT verdict should remain unchanged.","tokens_in":27438,"tokens_out":44329,"duration_ms":446600,"concrete_test":"Implement the recursive construction of Proposition 4.6 and exhaustively test all connected interval graphs of width k <= 4 with up to 10 intervals: for each interval representation, run the described lane partition and embedding, compute the maximum congestion on each original edge, and compare with g(k) and h(k). If any instance exceeds the bound, the theorem's O(log n) label size collapses; if none does, the weakest step in the paper is empirically supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After stress-testing the central construction, I do not find a load-bearing objection. The riskiest step is Proposition 4.6, whose inductive congestion accounting in Case 2.2 (Section 4.2) could in principle hide a factor growing with the number of components. I checked the two places where such a factor could enter: (1) the order of the attachment vertices v*_C along the path P is forced by interval overlap and disjointness of component intervals, so for a fixed (i,j,ell) each edge of P is used by at most one middle subpath; (2) prefix and suffix paths inside a component C are at most one per lane, so their combined congestion on any edge of C is at most 2 f(k-1), which is exactly what the recurrence adds. Additivity with Case 1 and Case 2.1 is explicit, so the total bound g(k) is consistent. I also checked Lemma 6.5: although the internal tree T of a T-node can be deep, each edge in a node G' carries only the O(log n)-bit basic information of G' and its immediate children's Tree-merge values, so label size does not grow with the depth of T. The typographical errors (e.g., Observation 4.9 and the duplicated tau_in in Section 5.4) do not affect the argument. No significant objection identified.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a proof labeling scheme (PLS) for every MSO2 graph property on graphs of pathwidth at most k, using O(log n)-bit vertex labels, thereby improving the O(log^2 n)-bit scheme of Fraigniaud et al. for bounded treewidth. The approach is based on a new structural decomposition: every bounded-pathwidth graph admits an interval representation whose intervals can be partitioned into O(1) lanes, and the resulting \"completion\" (connecting each lane into a path and connecting lane starts) embeds into the original graph with O(1) congestion. The completed graph is shown to be a k-lane recursive graph with a bounded-depth hierarchical decomposition, which allows certifying the execution of Courcelle-style dynamic programming over homomorphism classes with O(log n)-bit labels. As a corollary, using the Robertson-Seymour Excluding Forest Theorem, the class of F-minor-free graphs for every fixed forest F is certified with O(log n)-bit labels, answering an open question of Bousquet, Feuilloley, and Pierron.","tokens_in":134,"tokens_out":8011,"duration_ms":392607,"significance":"If correct, the result is a significant advance in local certification: it gives an optimal O(log n)-bit meta-theorem for all MSO2 properties on bounded-pathwidth graphs, and it resolves a concrete open question on forest minor-free classes. The paper is self-contained relative to standard tools (Courcelle's theorem, the Excluding Forest Theorem, and the KKP lower bound) and does not introduce fitted parameters. The constants f(k), g(k), h(k) are explicit, and the congestion analysis gives a concrete O(1) bound depending only on k. The construction of k-lane recursive graphs and the certification of their homomorphism classes are original and appear to be mechanistically sound. The main risk is the subtle congestion accounting in Proposition 4.6, which is terse; however, I checked the two places where a component-count factor could hide and found that the additive argument is consistent. The paper is not machine-checked, but the proof structure is detailed enough for a careful reader to verify. Overall, this is a strong and publishable contribution.","major_comments":[],"minor_comments":[{"comment":"The proof contains a false equality: it reads \"max_{v in S} R_v = R_{v_ed} = min_{v in V} L_v\", but the second equality should be \"= max_{v in V} R_v\". The observation itself is correct, but this typo should be fixed.","section":"§4.2, Observation 4.9"},{"comment":"In the description of the E-node created for a V-insert operation, the equation \"tau_in^i(G*) = v, and tau_in^i(G*) = tau_i\" repeats the same symbol; the second occurrence should be \"tau_out^i(G*)\". Please correct this.","section":"§5.4, Proposition 5.6 Case 1"},{"comment":"The claim that for each triple (i,j,ell) each edge of P participates at most once in the middle portions of the crossing-edge paths is correct, but it is not fully justified in the text. A short explanation using the order of the attachment vertices v*_C along P and the pairwise disjointness of the intervals {I_C : C in C_i} from Lemma 4.10 would make the congestion bound easier for readers to verify.","section":"§4.2, Case 2.2"},{"comment":"In the B-node paragraph, \"in-teriminals\" and \"out-teriminals\" are typos for \"in-terminals\" and \"out-terminals\". Elsewhere in the same lemma, the phrase \"the right in-terminal\" should probably be \"the corresponding in-terminal\".","section":"§6.2, Lemma 6.5"},{"comment":"The statement that (pathwidth <= k) is an MSO2 graph property would benefit from a citation, e.g., to the standard Courcelle/Arnborg-Lagergren-Seese literature, since it is load-bearing for the self-certification of bounded pathwidth.","section":"§1.4"}],"recommendation":"minor_revision","confidential_remarks":"I concur with the positive assessment from the reader's report: after stress-testing Proposition 4.6 and the bounded-depth recursive certification, I found no load-bearing gap. The paper is technically strong and the result is a natural fit for this venue. The minor comments are mostly typos and requested clarifications; none affect the validity of the main theorem. I recommend minor revision rather than immediate accept only because a few localized proof passages should be expanded for reader confidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know up front. First, this is a real advance, not an incremental tweak: it improves the bounded-treewidth result from O(log^2 n) to optimal O(log n) for bounded pathwidth, and it answers Bousquet–Feuilloley–Pierron's question about forest-minor-free graphs. Second, the part I was most suspicious of, the congestion analysis in Proposition 4.6, survived my stress-test. The paper is worth engaging with seriously.\n\nWhat is actually new: the k-lane recursive graph decomposition, the low-congestion embedding that completes a lane partition, and the bounded-depth hierarchical decomposition that lets you certify a Courcelle-style dynamic program with only O(1) congestion overhead. The meta-theorem covers all MSO2 properties, so the applications (planarity, Hamiltonicity, k-colorability, minor-freeness, etc.) come as corollaries of one clean mechanism rather than a pile of bespoke schemes. The proofs are detailed and mostly self-contained; the reliance on Courcelle's theorem and the Robertson–Seymour Excluding Forest Theorem is standard and appropriate.\n\nThe soft spots are real but minor. Proposition 4.6, Case 2.2, is the densest stretch of the paper; the congestion accounting for the middle portions of crossing paths is compressed, and a reader has to fill in why the interval structure keeps each edge of P from being reused too often. I checked the two places where a hidden factor could creep in, and both are fine: the order of the attachment vertices along P is forced by interval disjointness, and the prefix/suffix costs inside a component stay bounded by f(k-1) per lane. There are also several typos, most notably in Observation 4.9's proof (\"max R_v = R_ved = min L_v\" should be max R_v) and a duplicated tau_in in Proposition 5.6 Case 1. None of these affect the argument.\n\nThe lower bound argument is correct: O(log n) is optimal because any scheme that accepts paths and rejects cycles needs that many bits.\n\nWho gets value from this: anyone working in local certification, distributed graph verification, or meta-theorems for bounded-width graph classes. It moves a known open problem to a definitive answer and provides a toolbox that is likely to be reused.\n\nMy recommendation: send it to peer review. The typos will be caught, and the authors should be asked to expand the proof of Proposition 4.6 slightly, but this is a solid, significant paper that deserves referee time.","headline":"The paper delivers a genuinely new optimal O(log n) certification meta-theorem for bounded-pathwidth graphs and resolves the forest-minor-free open question; the hardest congestion proof holds up under scrutiny.","tokens_in":28242,"tokens_out":1490,"would_cite":true,"duration_ms":17605,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68W15","05C83","05C85"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that any graph property expressible in MSO2 logic—planarity, Hamiltonicity, k-colorability, and more—can be locally certified with O(log n)-bit vertex labels on graphs of bounded pathwidth, and that this label size is…","keywords":["proof labeling schemes","local certification","pathwidth","monadic second-order logic","Courcelle's theorem","graph minors","F-minor-free graphs","distributed verification"],"falsifier":"Construct a width-3 interval representation where a long $v_{st}$-$v_{ed}$ path interleaves many small connected components between consecutive vertices of $S$, and count how many crossing paths in Case 2.2 of Proposition 4.6 use a single edge of that path; if the count grows with the number of components, the claimed $O(1)$ congestion bound is false.","tokens_in":27256,"feed_emoji":"🏷️","tokens_out":5076,"duration_ms":47331,"temperature":0.7,"pith_summary":"The paper establishes a meta-theorem for local certification: for any fixed integer $k$ and any graph property $\\phi$ expressible in MSO2 logic, the property \"the graph satisfies $\\phi$ and has pathwidth at most $k$\" can be certified by a proof labeling scheme with $O(\\log n)$-bit vertex labels. This improves the previous $O(\\log^2 n)$-bit result for bounded treewidth and matches the $\\Omega(\\log n)$ lower bound that already applies to the simplest such classes. As a corollary, combining the result with the Excluding Forest Theorem of Robertson and Seymour shows that graphs excluding any fixed forest $F$ as a minor can be certified with $O(\\log n)$-bit labels, answering an open question. The proof rests on a new decomposition of bounded-pathwidth graphs into $O(1)$ lanes whose completion embeds into the original graph with $O(1)$ congestion.","feed_headline":"Optimal O(log n)-bit certificates for bounded-pathwidth graphs","feed_subtitle":"Every MSO2 property on bounded-pathwidth graphs now gets the smallest possible proof labels.","key_machinery":"The load-bearing objects are $k$-lane recursive graphs: $k$-lane graphs (graphs with in- and out-terminals assigned to lanes) closed under two merge operations—Bridge-merge, which joins two graphs on disjoint lane sets by adding one edge between out-terminals, and Tree-merge, which glues child in-terminals to the parent's out-terminals along a tree. The paper proves such graphs have hierarchical decompositions of depth at most $2k$ (Observation 5.5), and that the homomorphism class of an MSO2 property is computable over these merges (Proposition 6.1). The bridge from arbitrary bounded-pathwidth graphs to these recursive graphs is Proposition 4.6, which constructs a lane partition of a width-$k$ interval representation with congestion at most $h(k)$ for the completion.","core_discovery":"The central discovery is that bounded-pathwidth graphs, viewed through their interval representations, admit a lane partition into $O(f(k))$ lanes whose \"completion\"—adding edges to link consecutive intervals in each lane and to connect lane starts—can be embedded back into the original graph with $O(1)$ congestion per original edge, for constant $k$. The completed graph is a $k$-lane recursive graph built by Bridge-merge and Tree-merge operations, and any such graph can be generated by a hierarchical decomposition of depth at most $2k$. Because the decomposition has constant depth, each original edge belongs to only $O(1)$ nodes of the decomposition, so the dynamic-programming homomorphism classes from Courcelle's theorem can be certified edge-by-edge at constant congestion overhead, yielding $O(\\log n)$-bit edge labels and, after the standard edge-to-vertex transformation, $O(\\log n)$-bit vertex labels.","pith_inferences":["If the lane-based ideas could be adapted to handle the disconnected bags of a tree decomposition, the bounded-treewidth analogue might drop from $O(\\log^2 n)$ to $O(\\log n)$; by the Excluding Grid Theorem that would also imply optimal certification of $H$-minor-free graphs for every planar $H$.","A concrete stress-test family consisting of many small connected components interleaved along the $v_{st}$-$v_{ed}$ path would reveal whether the $O(1)$ congestion bound in Proposition 4.6 is truly independent of the number of components, since that independence is the load-bearing part of the argument.","The $k$-lane recursive graph toolbox may be reusable beyond certification—for example as a structural primitive for distributed approximation, routing, or decomposition algorithms on pathwidth-bounded networks."],"forward_implications":["For every fixed $k$ and every MSO2 property $\\phi$, the property \"$\\phi$ and pathwidth at most $k$\" is certifiable with $O(\\log n)$-bit labels, and this is optimal because the same lower bound holds for paths versus cycles.","Any fixed forest $F$ yields an $O(\\log n)$-bit proof labeling scheme for $F$-minor-free graphs, thereby resolving the open question about certifying tree-minor-free and forest-minor-free graph classes.","The certification works by verifying an execution of Courcelle-style dynamic programming, so it applies uniformly to a broad list of properties, including planarity, Hamiltonicity, $k$-colorability, perfect matching, and having a vertex cover of given size.","The construction produces $O(\\log n)$-bit edge labels in bounded-degeneracy graphs, and the standard transformation to vertex labels preserves the $O(\\log n)$ bound because bounded-pathwidth graphs have bounded degeneracy."],"supporting_citations":[{"why":"Introduces proof labeling schemes and supplies the $\\Omega(\\log n)$ lower bound that makes the new label size optimal.","marker":"[KKP10]"},{"why":"Establishes the previous $O(\\log^2 n)$-bit meta-theorem for bounded treewidth, the bound this paper improves.","marker":"[FMR+24]"},{"why":"Proves Courcelle's theorem, providing the MSO2 homomorphism-class machinery (Proposition 2.4) used to certify properties.","marker":"[Cou90]"},{"why":"Independently rediscovers the linear-time MSO2 meta-algorithm on recursively constructed graph families, supplying the recursive-graph framework.","marker":"[BPT92]"},{"why":"The Excluding Forest Theorem, which bounds the pathwidth of $F$-minor-free graphs and turns Theorem 1 into Corollary 1.2.","marker":"[RS83]"},{"why":"Poses the open question about certifying tree-minor-free graphs with $O(\\log n)$ bits, which Corollary 1.2 answers affirmatively.","marker":"[BFP24]"},{"why":"Provides the edge-certification to vertex-certification transformation (Proposition 2.1) needed to state the final vertex-label result.","marker":"[FFM+23]"}],"fun_headline_variants":["Optimal O(log n) certification for bounded pathwidth","Bounded-pathwidth graphs: optimal log n proof labels","All MSO properties on bounded pathwidth: O(log n) certificates","Pathwidth-bounded MSO gets optimal log n certificates","Log n-bit local proofs for all bounded-pathwidth properties"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire construction rests on the claim that any width-$k$ interval representation of a connected graph can be partitioned into $O(1)$ lanes so that the completed graph embeds into the original graph with $O(1)$ congestion, independent of the number of connected components.","fun_headline_variants_meta":{"raw":{"variants":["Optimal O(log n) certification for bounded pathwidth","Bounded-pathwidth graphs: optimal log n proof labels","All MSO properties on bounded pathwidth: O(log n) certificates","Pathwidth-bounded MSO gets optimal log n certificates","Log n-bit local proofs for all bounded-pathwidth properties"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000871,"raw_usage":{"total_tokens":3795,"prompt_tokens":990,"completion_tokens":2805,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":606,"completion_tokens_details":{"reasoning_tokens":2721}},"tokens_in":606,"tokens_out":2805,"duration_ms":21506,"temperature":1.0,"reasoning_tokens":2721,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T18:10:21.331504+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a width-3 interval representation where a long $v_{st}$-$v_{ed}$ path interleaves many small connected components between consecutive vertices of $S$, and count how many crossing paths in Case 2.2 of Proposition 4.6 use a single edge of that path; if the count grows with the number of components, the claimed $O(1)$ congestion bound is false.","supporting_citations":[],"review_version":1}