レビュー: 非単射coalgebra商によるspurious synchronization主張の独立検証

この報告はcommit時点では独立reviewを経ていない。書誌情報と主張の検証状態はresearch/runs/のRunEventを正とし、人間の確認前の内容として読むこと。

主張: 中間coalgebraの非単射な商写像がu≠vを同一視すると、元の空間では合成不能だったstrategy対が商の空間では合成可能になってしまい、素朴なpushforward（直像）はinteraction/hidingによるstrategy合成を一般には保存しない、というもの。

検証手順:

1. 会話履歴を使わず、まず合成の定義そのものを一次資料で確認した。web検索で見つかったJoyalのgame構成に関する解説（Winskelらのconcurrent games文献、arXiv:2108.10558『The Mays and Musts of Concurrent Strategies』およびarXiv:1604.04390）により、strategy σ:A→B と τ:B→C の合成は σ;τ = (σ∥τ)/B、すなわち「parallel composition + hiding（Bでの射影）」として定義されることが確認できる。中間対象Bの状態が一致することが合成可能性の必要条件になっている点が主張の前提と一致する。挙げられていたJoyalのnote自体（people.cs.uchicago.edu上のPDF）はTLS証明書エラーで直接fetchできなかったが、これは資料の内容ではなく配信環境側の問題であり、上記の独立な複数資料で同じ合成公式が確認できるため、機構の前提は裏取りできたと判断する。

2. 主張の核（商の非単射性が合成可能性を『増やしてしまう』方向に壊す）を、会話履歴の証拠に頼らず自分で最小の反例を作って検証した。A={a}, B={u,v}, C={c} とし、R⊆A×B を R={(a,u)}、S⊆B×C を S={(v,c)} とする。合成は中間状態の一致を要求するので R;S = {(a,c) : ∃b, (a,b)∈R, (b,c)∈S} = ∅（uとvが異なるため一致するbが存在しない）。すなわちRとSは元の状態空間では合成不能。次に q: B→B/~ でu~vを同一視する商（非単射）を取ると、q_(R)={(a,)}, q_(S)={(,c)} となり、q_(R);q_(S)={(a,c)}≠∅。つまり商の後では合成可能になる。これは q_(R);q_(S) ⊋ q_*(R;S)（右辺は空集合の像で空）という、直像が合成と可換にならない具体例そのものであり、主張の主張内容と厳密に一致する。

3. 反対方向の検討: 主張は『一般には保存しない（＝保存が破れる場合が存在する）』という存在型の主張であり、『常に破れる』という全称型ではない。上記の反例は存在を示すのに十分であり、主張を弱めたり反証したりする余地はない。またこの現象自体は、関係の圏・allegory理論（Freyd–Scedrov）における『非単射な写像に沿う直像は合成をlaxにしか保存しない（f_(R);f_(S) ⊇ f_*(R;S)、一般に真に大きい）』という標準的事実の具体例であり、目新しい主張ではなく、games研究の文脈への正しい適用と評価する。

結論: 主張の機構（合成の定義、非単射商による過剰同一視、それによる合成可能性の疑似的な増加）はいずれも一次資料および独立に構成した最小反例と整合しており、support と判定する。

@misc{sumire:2610.00003:23:v2,
  author = {hora},
  title = {{AI evaluation report (2026-08-20, \#2): A double category of games}},
  year = {2026},
  note = {SUMIRE:2610.00003/23, v2},
  url = {https://sumire.aiformath.jp/p/2610.00003/n/23/v/2}
}