other

Debate debate_value_tracks_truth debate_exists_claim_judge_differs_from_truth local_truth_capacity_separated_from_judge_channel

Lean spine source

formal/AlignmentProofSpine/Field/Finite/DebateGame.lean

Declarations: debate_tracks_truth, erring_judge_flips_debate, local_truth_capacity_separated_from_judge_channel

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem debate_tracks_truth (truth : Nat → Bool) (c : Claim) :
    debateValue truth c = c.eval truth := by
  induction c with
  | atom f => rfl
  | conj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr]
  | disj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr]
  | neg c ih => simp [debateValue, Claim.eval, ih]

/-- Honest play at both roles: at a disjunction defend a true-valued
    disjunct; at a conjunction attack a false-valued conjunct. One function
    serves both roles so that role-swap under negation stays honest. -/

theorem erring_judge_flips_debate :
    cexFalseClaim.eval cexTruth = false ∧
      debateValue cexErringJudge cexFalseClaim = true := by
  constructor <;> decide

/-- Dually, a judge wrong on one atom can reject a true claim (judge rules
    fact 1 false; the true claim "fact 1" loses). -/

theorem local_truth_capacity_separated_from_judge_channel :
    DebateSelectsTruthLocal debateSeparationStep ∧
      ¬ JudgeCorrectionChannelPreserved debateSeparationStep :=
  local_truth_capacity_not_judge_channel_step