other

FDEB

Lean spine source

Declarations: debate_separated_from_judge_correction, debate_truth_is_correction_projection

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem debate_separated_from_judge_correction :
    DebateSelectsTruthLocal debateSeparationStep ∧
      ¬ JudgeCorrectionChannelPreserved debateSeparationStep :=
  debate_truth_separated_from_judge_correction_step

theorem debate_truth_is_correction_projection
    (s : DebateCorrectionStep) :
    DebateTruthAsJudgeCorrectionProjection s → DebateSelectsTruthLocal s :=
  debate_truth_is_judge_correction_projection s