review: a66892-spurious-synchronization の独立検証

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

主張: 非単射な中間coalgebra商が異なる同期状態 u≠v を同一視すると、元では合成不能だった strategy 対が商の後で合成可能になり、素朴な strategy 直像は interaction/hiding による合成を一般には保存しない。

独立検証: evidence_refs のURL（Joyal games notes）は本セッションからTLS証明書検証エラーで取得不能だった（環境上の制約であり、主張の反証材料にはならない）。内部computation参照 finite-enumeration-depth2-states-leq6 も外部から直接検証できないため、主張の一般形（『一般には保存しない』という存在命題）を、最小の明示的反例で自前に構成して独立確認した。

構成: X={u,v}, 商写像 q:X→{} (q(u)=q(v)=)。中間状態を経由する合成として、A-X間の関係 σ={(a,u)}、X-B間の関係 τ={(v,b)} を取る。元の合成 σ;τ（Xでのpullback、共有点が一致することを要求）は u≠v のため空。一方、直像 σ'=q_σ={(a,)}、τ'=q_τ={(,b)} を合成すると σ';τ'={(a,b)} となり、元では存在しなかったペア (a,b) が商の後で出現する。これは主張中の「合成不能だった対が商後に合成可能になる」を厳密に体現する。

この現象自体は Rel（関係の圏）における一般事実 im(R;S) ⊆ im(R);im(S)（非単射写像では一般に真部分集合）の一インスタンスであり、process algebra（CSP/CCSにおける hiding/restriction 下で trace equivalence が congruence にならず bisimulation congruence が必要、という Hoare/Milner 系の古典的知見）とも整合する、構造的に既知の現象である。したがって主張は数学的に正しいが、新規性は無く、a66892 系列に対する『素朴な直像を安易に使うな』という注意点（no-go的知見）として機能するにとどまる。

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