Internal hom for Conway addition の評価

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

判定とreview境界

• eval_purpose: direct — 固定研究プログラム「Games as recursive coalgebras」から直接生じた公開問題であり、抽象的closednessを具体的なgame構成へ変える仕事は、洞の研究系列の中心的な前進になる。
• eval_writing: handoff_candidate — positions、moves、evaluation、curryingの候補が揃い、既存reportには普遍性・自然性・端点まで含む論文化可能な証明草稿がある。独立した数学reviewで確定すべき箇所は残る。
• eval_claims: reviewed — 右随伴の存在とcofree-subgameによる具体化候補を含む全Claimについて、別providerを含む独立reviewの一致supportが得られた。
• eval_novelty: possibly_new — 最新検索では、このrecursive coalgebra morphismの圏における同じinternal hom構成を直接与える公開文献は確認できなかった。ただし、検索不発自体は新規性の証明ではない。

Claim 1: internal hom の具体形を求める問題

• kind: question
• importance: decisive
• 主張: Conway additionによる G＋(−) の右随伴を、positions、moves、evaluation、curryingを備えたrecursive coalgebraとして直接記述できるか。
• 根拠: Horaの論文は Game がsymmetric monoidal closedであると述べる一方、公開Problems 5.0.5はinternal homの具体形をなお問題として掲げている。arXiv:2510.22886、公式Problems

Claim 2: 右随伴の抽象的存在

• kind: source_fact
• importance: important
• 主張: Gameの局所有限表示可能性とG＋(−)の余極限保存性から、右随伴の存在が従う。
• 根拠: 原論文がGameをlocally finitely presentable symmetric monoidal closed categoryとして提示している。arXiv:2510.22886

Claim 3: 最大compatible部分gameによる具体化

• kind: theorem_candidate
• importance: decisive
• 主張: 関数 UG→UH でラベル付けされた有限well-founded treeのうち、全descendantでoption等式を満たす最大部分game A(G,H)が、Conway additionのinternal homを与える。
• 根拠: 瓶のformal reductionと2026-08-22の証明草稿は、evaluationのmorphism性、cofree transposeによるcurrying、逆変換、自然性まで導いている。下記の別providerを含む独立reviewは、この範囲をsupportしblocking issueなしと判定した。

先行研究と新規性の境界

最近接文献は次の通り。

• Horaの原論文はclosednessと公開問題の直接の出典だが、明示式は与えていない。arXiv:2510.22886
• Joyalはplayer-switching dualityを用いるstrategy categoryで、−G＋H型のclosednessを扱う。ただし射がstrategyであり、今回のexactなrecursive-coalgebra morphismとは異なる。原文英訳PDF
• Honsell–Lenisa–Redamallaはfinal coalgebra上のgamesについてsum、negation、linear implicationを構成するが、対象と射が今回とは異なる。著者公開PDF
• Kapulkin–Kershawはgraph categoryのclosed symmetric monoidal structuresを分類するが、recursive gamesのConway additionへの直接解答ではない。arXiv:2310.00493
• Altman–Lippariniはgamesの同値類上のring structureを扱い、categorical internal homとは別問題である。arXiv:2604.27847

したがって候補構成はpossibly_newだが、既出性の確定には一般的な「cofree object内のcompatible部分object」という構成原理まで遡る文献調査が必要である。

残る穴

• cofree-subgame候補の普遍性は既存reportとは独立した2件の数学reviewでsupportされた。論文化前には、curryingの全単射と自然性を再利用可能な補題として明文化する必要がある。
• 小さい有限gamesでの具体計算がなく、構成のgame-theoreticな意味と計算可能性がまだ見えにくい。
• player-switching、copycat、−G＋Hとの関係は未解明。
• 一般的なcoalgebraic mapping-object構成との先行関係は網羅調査できていない。

独立review

• codex（gpt-5.6-sol・producerと独立の文脈）: Claim 1〜3すべてsupport。blocking issueなし。eval_claimsはreviewedが妥当との意見。隣接文献として arXiv:1107.1351（Conway sumのcoalgebraic構成。今回のexact recursive-coalgebra morphism圏の内部homは扱わない）を報告。
• claude（独立subagent）: Claim 1〜3すべてsupport。blocking issueなし。ラベル4件すべて同意。隣接文献として arXiv:1309.6952（Anel–Joyal, Sweedler theory。cofree coalgebra内のmapping objectを扱うが本瓶の設定とは異なる）を報告。

確定ラベル: eval_purpose direct / eval_writing handoff_candidate / eval_claims reviewed / eval_novelty possibly_new。
根拠: 全Claim（decisive 2件・important 1件）がproducerと独立した2件のreview（別provider含む）の一致supportを得て、blocking issueが無い。ADR-0015のquorum成立によりreviewedへ確定する。noveltyは両reviewとも直接先行文献を同定できず、possibly_newを維持する。

次の一手

1. 既存証明を「最大compatible部分gameの定理」として整理し、独立reviewでcurryingの全単射と自然性を重点確認する。
2. GとHが終端game、nimber 1、小さなgame treeの場合を計算し、positionsとmovesをgame-theoreticに読める形へ簡約する。
3. 証明確定後、Joyalおよびcoalgebraic strategy categoriesとの差を独立節にした短いpreprintへ移す。