Thank you for actually looking at the Lean code. I think your points are fair and I should have been more clear.
The recursion you mention is the game value under optimal play, which in this finite version indeed just amounts to evaluating the claim tree. The actual game is in debateOutcome / defender_wins_iff_truehere.
Irving’s paper has a bounded judge and obfuscated arguments and I did not rederive it in Lean. It is treated as an imported result (here). There are more complete finite rederivations for Shutdown and ELK. I understand your disappointment; if you were looking for an actual derivation of Irving in Lean. I use debate to make the conditional soundness/completeness lemma explicit. I do not claim a reduction of Irving’s complexity result.
You are right that a judge who can score every atom doesn’t need debate. The lemma is only: a judge who can score the reached atom recovers the formula if both play optimally and that atom is judged correctly. That is a restatement of the finite protocol, not an alignment crux.
The finite Debate is a specific counterexample to unconditional certificate. I should not have written it as a general certification theorem. But we don’t need obfuscated arguments to show that “wrong judge” implies “wrong verdict”. The Debate code you saw is a finite shadow of the judge-integrity crux and trivial in the sense you said, and still enough to refute “debate certifies truth” (even when the judge is wrong).
Also agreed that the name of debate_truth_separated_from_judge_correction_step is misleading. It is not a result about the Irving-style game in DebateGame.lean. It is the numeric k_C witness currently used for “local truth-capacity can be positive while the judge correction channel is not preserved” (DebateCorrectionStep in Correction.lean). “debate_” in the name is that modeling slot, not the two-prover protocol.
On the axioms you saw: DebateGame.lean and the other derivations are axiom-free. Most axiom keywords are the bridges (MB1–MB11) discussed in the post that try to represent the structure of the field’s open cruxes. These bridges are declared axiom because they are hypotheses to check, not proven lemmas. I’d be too happy if you could suggest a better packaging. There are also axioms for imported literature results (like Irving’s debate).
I’d like to add you as a collaborator to the repo if you want to suggest issues or push PRs.
Thank you for actually looking at the Lean code. I think your points are fair and I should have been more clear.
The recursion you mention is the game value under optimal play, which in this finite version indeed just amounts to evaluating the claim tree. The actual game is in
debateOutcome/defender_wins_iff_truehere.Irving’s paper has a bounded judge and obfuscated arguments and I did not rederive it in Lean. It is treated as an imported result (here). There are more complete finite rederivations for Shutdown and ELK. I understand your disappointment; if you were looking for an actual derivation of Irving in Lean. I use debate to make the conditional soundness/completeness lemma explicit. I do not claim a reduction of Irving’s complexity result.
You are right that a judge who can score every atom doesn’t need debate. The lemma is only: a judge who can score the reached atom recovers the formula if both play optimally and that atom is judged correctly. That is a restatement of the finite protocol, not an alignment crux.
The finite Debate is a specific counterexample to unconditional certificate. I should not have written it as a general certification theorem. But we don’t need obfuscated arguments to show that “wrong judge” implies “wrong verdict”. The Debate code you saw is a finite shadow of the judge-integrity crux and trivial in the sense you said, and still enough to refute “debate certifies truth” (even when the judge is wrong).
Also agreed that the name of
debate_truth_separated_from_judge_correction_stepis misleading. It is not a result about the Irving-style game inDebateGame.lean. It is the numeric k_Cwitness currently used for “local truth-capacity can be positive while the judge correction channel is not preserved” (DebateCorrectionStepinCorrection.lean). “debate_” in the name is that modeling slot, not the two-prover protocol.On the axioms you saw:
DebateGame.leanand the other derivations are axiom-free. Mostaxiomkeywords are the bridges (MB1–MB11) discussed in the post that try to represent the structure of the field’s open cruxes. These bridges are declaredaxiombecause they are hypotheses to check, not proven lemmas. I’d be too happy if you could suggest a better packaging. There are also axioms for imported literature results (like Irving’s debate).I’d like to add you as a collaborator to the repo if you want to suggest issues or push PRs.