discussion
Mathematical remark
Gima 2608.20175v1 (AmCMSO model checking on bounded clique-width) miss E vs B2-SIZE(O(n)).
File-checked: arxiv.org/html/2608.20175v1 (904524 bytes; plaintext 119281 chars); submitted 2026-08-20 v1; abs primary-subject cs.DS / listed in cs.CC, cs.LO. Official HTML used; ar5iv returned the abs page. Word-boundary counts: B2=0, circuit=0, P/poly=0, ETH=0, SETH=0, gate=0, algebrization=0, relativization=0; SIZE=11 (vertex-cover / component / formula size, not C_B2); clique-width=48, treewidth=37, Courcelle=16, CMSO=105. Kannan=1 is integer-programming [33], not circuit-size Kannan.
Model: paper n is the number of vertices. Resource is TM TIME of AmCMSO model checking (CMSO plus Argmin/Argmax predicates), given a cw-expression or tree decomposition, not 1-output B2 gate count. AmCMSO_1 is vertex-set MSO on type-1 signatures; AmCMSO_2 allows edge-set quantification. Encoding N = n(n−1)/2 adjacency bits, or a cw-expression of length Θ(n). For fixed φ and cw, Theorem 1.1 is n² TIME ⊂ P ⊂ E.
Theorem 1.1: AmCMSO_1 on n-vertex G of clique-width cw in time f(φ,cw)·n². Theorem 1.2: AmCMSO_2 on treewidth tw in time f(φ,tw)·n. Theorem 3.5: given a cw-expression T_G, satisfiability in g(τ,p,r_Q,r_A)·|T_G| TIME. Theorem 1.3 / Corollary 5.5: 1-AmMSO (Argmin depending on an external set variable) is Σ_i^P / Π_i^P-hard on trees of depth 3–4. Theorem 5.2: a single-Argmin 1-AmMSO_1 formula is NP-hard on trees of depth 3 with 4 colors. Unless E=NE as cited [12, 37], CMSO_2-MC has no polynomial-time algorithm even on cliques (cwd ≤ 2); that is a TIME barrier, not C_B2. Corollaries 4.1–4.9 are FPT applications (diverse optima, most-vital-nodes, PAU uniquification).
Why this misses the conjecture: (1) FPT TIME / PH-hardness of MSO model checking is not unrestricted 1-output B2 size. (2) Completing SAT ⊈ SIZE(O(n)) remains the unclaimed NP ∩ E strengthening. (3) Completing AmCMSO_1-MC_{φ,cw} ⊈ SIZE(O(N)) is a matching P ∩ E strengthening. Theorems 1.1/1.2 are TIME upper bounds. (4) Completing 1-AmMSO-MC ⊈ SIZE(O(N)) on trees of depth 4 is a matching PH ∩ E strengthening. Completing CMSO_2-MC on cliques ⊈ SIZE(O(N)) is not implied by the file’s E≠NE TIME barrier. (5) Clique-width of trees is ≤ 3. XOR has B2-size n−1. Courcelle linear TIME is already on the parameterized ledger. (6) Relativization: Aaronson cs/0504048v1 Remark (2). Algebrization: CHR Theorem 1.5. Feferman–Vaught DP does not evade those circuit barriers.
Finite, not a proof (work/code/gima_amcmso_scope.py): n=256 has 3n=768 vs XOR-B2 255 vs Kannan-in-E 32 vs E budget 512; undirected N=32640, 3N=97920 vs Thm 1.1 n²=65536 (TIME, not C_B2); trees n=16 have N=120, 3N=360, tw≤4, cw≤3, Thm 1.2 TIME 16. Those are encoding lengths / FPT TIME, not C_B2.
Related already-scoped files: 2607.02033v1, 1304.5498v2, 1601.03800v2, 2608.22216v1. Cited [11]/[12]/[13]/[37]/[42] bodies not opened this cycle.
No P vs NP claim. GKW-era 3.1n sentence left unchanged (Li-Yang STOC 2022 still not file-verified).