問い #232

A5 proof-certificate search ## Trigger 全60元 alphabet版の $A_5$ word problem が height $\leq1$ だった場合、それを computer program で feasible に check できるか、実際に探索する会話から生まれた。結論は「候補 certificate の検証は exact にできるが、60-state DFA だけからの無構造な全探索は feasible でない」という分離である。 ## Idea 標準評価 \[ \pi:\underline{A_5}^*\twoheadrightarrow A_5 \] の単位元 fiberについて、height-$1$ certificate を次のいずれかで与える。 1. 対象言語と等価な generalized regular expression $E$ で、star nesting depth が高々 $1$ のもの。 2. star-free language $K$ と、marked factorization \[ \ker\eta_{K^*}\subseteq\ker\pi \] を示す有限データ。 certificate が与えられれば、DFA equivalence、最短 distinguishing word、$K$ の aperiodicity、$K^*$ の syntactic morphism、$A_5$ への factorization を有限計算で exact に検証できる。したがって proof discovery と proof checking を分離し、小さな deterministic verifier を最終関門にする。 ## Computational observation generalized-regex AST の素朴な size enumeration はすでに size $4$ で約 $1.07$ GiB に達し、size $5$ で破綻した。よって「高さ $1$ の式が存在するなら全式を順に列挙する」という探索は、60-state DFA に対して現実的でない。 探索対象を、star-free return codes、marked syntactic congruences、既知の token / anchor decompositions など、有限の構造を持つ certificate family に限定する必要がある。 ## Goal $A_5$ の yes/no 解決を、信頼できる certificate pipeline にする。肯定側では一つの explicit witness を見つければよい。否定側では [[w9v6hw]] により、任意の star-free $K$ が $\pi$ を分離できないことを示す universal obstruction が必要である。 ## Status 現時点で witness も universal obstruction も得られていない。計算結果は undecided であり、height $\geq2$ を示してはいない。 ## 追記（2026-08-27・AI採掘）: 952状態 architecture の完全 no-go 証明書 2026-07-25 の探索（ChatGPT 会話「理論的ゴリ押し」）で、一つの certificate family が**完全に閉じた**。15 個の easy first-return root automata の同期積（952 状態、各成分 aperiodic）について、全 \(2^{952}\) 個の受理集合 \(F\) に対し \[ \ker\eta_{K_F^*}\not\subseteq\ker\mu \] が成り立つ。証明は 5 組の語対の relation-collision 条件を厳密 DNF 化し、その連言が充足不能であることを示す。発見には Z3 を使ったが、公開証明は 66,616 ノードの case-split proof DAG として独立検証可能（検証約 45 秒）。 これは「この architecture からは肯定側 witness が出ない」という exact な排除であり、Computational observation 節の方針（無構造全探索の放棄、構造つき certificate family への限定）の最初の完全な実行例である。同時期の関連結果（height-one flattening・全 60 元アルファベットへの生成系消去）は [[w9v6hw]] 側に記録する。