Field crosswalk — Debate

Debate asks whether adversarial argument lets a judge select locally correct answers under idealized protocol assumptions. Preserved judge correction plus positive local truth capacity implies local truth selection — but local truth selection need not preserve the judge's correction channel.

What decision changes?

When using debate or amplification for oversight, track whether the judge's correction handles remain causally effective, not only whether local answers look true.

Debate is a scalable oversight proposal: two agents argue; a judge picks the winner. The field object is local truth selection under protocol assumptions. The book’s worry is familiar from amplification: improving local supervision can fail correction contraction — the judge may lose the handles that make their verdict causally matter.

Lean records the forward projection when judge correction and truth capacity align, and a finite separation when truth selection persists without judge-channel preservation. Native debate-game theorem matching remains deferred; the honest claim is projection plus separation on the shared finite fragment.

What debate keeps that this crosswalk does not replace: a concrete oversight protocol and training/eval procedure. The book names a failure mode of it, not a replacement protocol.

Formulas

JudgeCorrectionChannelPreserved  κtruth>0  DebateSelectsTruthLocal\mathrm{JudgeCorrectionChannelPreserved}\ \wedge\ \kappa_{\mathrm{truth}}>0\ \Rightarrow\ \mathrm{DebateSelectsTruthLocal}
Forward projection: preserved judge correction and positive truth capacity imply local truth selection. (ch29)
DebateSelectsTruthLocal  ¬JudgeCorrectionChannelPreserved\mathrm{DebateSelectsTruthLocal}\ \wedge\ \neg\mathrm{JudgeCorrectionChannelPreserved}
Non-converse separation: debate can preserve local truth while losing judge correction control. (ch41)