Concurrent AI coding agents create a coordination problem in which cheap signals may prioritize work, but only an executable checker can establish the property being claimed. We study this separation through a property-scoped verification contract and MERGEGYM, a three-track benchmark for open-time scope forecasting, replay- conditioned conflict resolution, and scheduling. On a stratified 715-pair lineage set (167 textual conflicts), 79 conflicts (47.3%) occur despite disjoint authored file sets. This is an operationally important proxy mismatch expected from three-way merge: authored PR diffs are measured against PR-specific bases, whereas the checker compares both heads to their common merge base. A standalone lineage-union rule reaches held-out AUROC 0.877; a 12-feature logistic model reaches 0.882 [0.845, 0.917] with PR-AUC 0.661, and an untuned random forest on the same decision-time features reaches 0.902 [0.875, 0.928] with PR-AUC 0.701. At a 33.3% held-out replay budget, the logistic and random-forest models recover 81.2% and 82.9% of conflicts, respectively. Patch reconstruction succeeds for 48/79 zero- overlap conflicts and all 48 become clean; the other 31 cases are inconclusive, so this check validates the expected three-way-merge explanation rather than claiming a new Git mechanism. In T1, a zero-shot LLM reaches AUC 0.704 and LLM-plus- metadata fusion 0.740. In T3, a decision-time gate de-overlaps a median 91.7% of labeled scope collisions at 65.0% makespan inflation under frozen-label replay. Because local git merge-tree replay is already cheap in our logs (median 0.02 s), we do not claim that lineage triage saves this checker alone: when exact replay is cheap, verify everything. All empirical guarantees in this paper remain limited to textual mergeability or the explicitly stated frozen-label scheduling target.

翻译：暂无翻译