word gameとstar height 1予想 の評価

このreportはPR上の提案であり、洞のmergeまでは正本ではない。

判定とreview境界

• eval_purpose: direct — 固定研究プログラム「Games as recursive coalgebras」に属し、登録済み slogan「Formal languages」にも直結する。ゲームの再帰的 P/N 判定から regular language の構造定理を取り出す、研究プログラムの中核的な問題である。
• eval_writing: handoff_candidate — prefix code の定理、一般有限 S の予想、重なりを持つ最小例の計算証拠という段階構成があり、論文の骨格を描ける。
• eval_claims: review_pending — 定理候補・予想・計算的等式を含む。以下はいずれも数学review未確定。
• eval_novelty: possibly_new — Larsson の ⋆-operator、generalized star-height 1 の既知クラスとは明確に接するが、自由モノイド上の prefix-removal game と generalized star height を結ぶ同一結果は確認できなかった。ただし、限定的なweb検索だけでは新規性を確定できない。

Claim 1: kernel方程式

• kind: theorem_candidate
• importance: important
• 主張: prefix-removal game の P-局面 Pₛ は一意であり、Σ* ∖ Pₛ = S Pₛ を満たす。
• 根拠: 手が語長を真に減らすため帰納的にP/Nを決定できる、という瓶本文の議論。形式的証明はまだ提示されていない。

Claim 2: 有限Sでのregularity

• kind: theorem_candidate
• importance: decisive
• 主張: S が有限なら Pₛ は regular language である。
• 根拠: 最大手長までの有限な prefix-overlap 情報で再帰判定できるという有限状態化の見通し。ただし automaton の明示と正当化が必要。

Claim 3: 像はREGより真に小さい

• kind: theorem_candidate
• importance: routine
• 主張: 有限 S から得られる Pₛ 全体は REG の真部分クラスであり、特に {ε} は実現されない。
• 根拠: 瓶本文の例示。有限 S に対する非実現性の一般証明を補う必要がある。

Claim 4: prefix codeの場合の公式

• kind: theorem_candidate
• importance: important
• 主張: S が有限 prefix code なら、T = Σ* ∖ SΣ* として Pₛ = (S²)*T であり、generalized star height は1以下である。
• 根拠: greedy factorization の一意性と、有限言語 S² および T の star-free 性。論文化可能な既証明部分だが、独立reviewは未了。

Claim 5: finite game-star conjecture

• kind: conjecture
• importance: decisive
• 主張: 任意の有限 S ⊆ Σ⁺ に対し、Pₛ の generalized star height は1以下である。
• 根拠: prefix code・unary case・重なりを持つ計算例が支持する一方、一般の bounded NOR 固定点を一段の Kleene star へ flatten する議論は未完成。

Claim 6: S = {a, b, ab} のheight-one表示

• kind: theorem_candidate
• importance: important
• 主張: S = {a, b, ab} に対する Pₛ は、瓶記載の star nesting depth 1 の式で表される。
• 根拠: 長さ12以下の全8191語と、長さ300以下の乱択30000語でゲームDPと一致した ⚪COMPUTED 証拠。有限標本による一致であり、証明ではない。

Claim 7: height 2反例の波及効果

• kind: source_fact
• importance: decisive
• 主張: 有限 S で generalized star height 2以上の Pₛ が得られれば、正規言語にheight 2以上が存在するという未解決問題へ明示的な解を与える。
• 根拠: generalized star height 2以上の regular language の存在自体が未解決とされている。Bourne–Ruškuc, arXiv:1603.06236、TU Wien講義資料（2025）。

先行研究と新規性の境界

最近接文献は次の三方向である。

• Larsson は invariant subtraction game に対し、非零P局面を次のゲームの手とする ⋆-operator を導入している。しかし基礎は ℕᵈ 上の可換な vector subtraction であり、本瓶の自由モノイド上の prefix removal や star height は扱っていない。arXiv:1009.4220、DOI:10.1016/j.tcs.2011.11.021。
• Pin–Straubing–Thérien は generalized star height 1 を保証する monoid・wreath product の広い十分条件を与える。本瓶の overlap automaton の transition monoid がその範囲に入るかが、既存理論へ接続する主要な判定点である。DOI:10.1016/0890-5401(92)90063-L。
• Bourne–Ruškuc は factor-counting language や Rees zero-matrix semigroup に対するheight-one結果を与えるが、ゲームの再帰的 kernel language は対象外である。arXiv:1603.06236。

したがって、新規性候補は ⋆-operator 自体ではなく、その非可換 prefix-game 化と、得られる全有限 ruleset language に対する一様なheight-one予想にある。

残る穴

• 一般有限 S の regularity を与える automaton と、その状態不変量がまだ明文化されていない。
• prefix code 証明から overlap case へ進む際、分岐する suffix recurrence を一段の star に flatten する原理がない。
• S = {a, b, ab} の式は計算証拠に留まり、全語についての automaton equivalence 証明がない。
• 文献探索はweb上の主要な近接文献に限られ、citation graph、MathSciNet、zbMATHを含む網羅調査ではない。したがって新規性は確定していない。

独立review

• codex（独立文脈）: Claim 1〜4・6・7 support（各claimを独立検算。Claim 6は瓶記載の式の厳密導出を確認）、Claim 5 insufficient（prefix code caseと個別例は、一般のbounded NOR固定点を一段のKleene starへ変換する証明を与えない）。blocking issueなし。Claims 2・6には短い完全証明を加えられるとの意見。
• claude（独立subagent）: Claim 1〜7すべてsupport（Claim 1〜4を自力で再証明。Claim 6は「abで始まる語は常にN」という補題により短い人手証明へ昇格できることを発見し、瓶の式との厳密一致を証明。Claim 5はconjectureとしての提示が適切で支持証拠が実在）。blocking issueなし。近接文献2件（StrNim arXiv:2503.16781、maximal prefix codeと開ゲーム arXiv:2601.17521）がいずれも本瓶をカバーしないことを確認。軽微な指摘: Claim 5の根拠に挙がる「unary case」は瓶本文に無い（数学的には真であり誤りではない）。
• 第三review（codex・tiebreak・先行2reviewを見ない独立文脈）: Claim 5 insufficient（regularityや有限automatonの存在だけからgeneralized star height 1以下は導けず、prefix overlapを処理する一般論も反例も無いため、支持・反駁のいずれも確定できない）。

確定ラベル: eval_purpose direct / eval_writing handoff_candidate / eval_claims review_pending / eval_novelty possibly_new。
根拠: Claim 1〜4・6・7は独立review 2件の一致supportでquorum成立（7件中6件検証済み）。本体のconjecture（Claim 5・decisive）は票が割れ、第三reviewにより2対1でinsufficientに確定したため、瓶単位ではreview_pendingに留める。noveltyは3つの独立検索いずれも直接先行を見つけられず、possibly_newを維持。

次の一手

1. S = {a, b, ab} について、ゲーム側DFAと記載式のDFAを構成し、同値性を機械的に完全証明する。これを論文の最初の非-prefix-code定理にする。
2. 一般有限 S の overlap-residual automaton を定義し、その transition monoid が既知のheight-one十分条件へ入るか調べる。
3. 「word subtraction」「prefix rewriting game」「kernel language」を軸にcitation graphまで調査し、本予想が既存定理の系でないことを確認する。