Lean · Common check

Does debate guarantee aligned oversight?

Debate asks whether adversarial argument lets a judge select locally correct answers. Lean rederives the finite debate game: with a correct judge, optimal play tracks truth; one wrong atom flips the outcome. Local truth selection need not preserve the judge's correction channel.

Short answer: Debate can make truth easier to *select* under a correct judge, but local truth selection need not preserve the judge's correction channel. Lean rederives the finite two-prover game (`debate_defender_wins_iff_true`; judge error ⇒ mis-certification via `debate_exists_claim_judge_differs_from_truth`). The κ_C separation is `local_truth_capacity_separated_from_judge_channel` (not a DebateGame theorem). Debater compute limits, training dynamics, and MB4 bridge discharge remain outside the finite spine.

Field terms

debate
scalable oversight
amplification

Stepping-stone path

Read in order — each step adds one book term, not the whole ontology.

What Lean checked (forward)

debate_value_tracks_truth — Lean source
debate_defender_wins_iff_true — Lean source
debate_judge_error_flips_outcome — Lean source

What Lean checked (separations)

debate_exists_claim_judge_differs_from_truth — Lean source counterexample
local_truth_capacity_separated_from_judge_channel — Lean source · Spine node counterexample

What Lean did not check

Debater compute limits and argument-length asymmetries (imported handle)
MB4 bridge assumptions (judge correction legitimacy in deployment)
Probabilistic judge / optimization pressure during training