OAI/Analysis/TracialSplitting/Challenge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The construction certificates are proved here, outside the self-contained challenge. main_iff_original checks that packaging them preserves the original assertion.

  1. def OAI.CurrentMain.OriginalGammaStatement line 14
  2. theorem OAI.ComparatorModel.CurrentMain.statement_iff_original line 62

    Source documentation

    The asserted conclusion, including all hypotheses, is definitionally unchanged.

    theorem statement_iff_original : Statement.{uNuclear} ↔
    _root_.OAI.CurrentMain.OriginalGammaStatement.{uNuclear} := Iff.rfl
  3. theorem OAI.ComparatorModel.CurrentMain.main_iff_original line 66

    Source documentation

    The existential construction requirements do not change the original assertion.

    theorem main_iff_original : MainClaim.{uNuclear} ↔
    _root_.OAI.CurrentMain.OriginalGammaStatement.{uNuclear} := by
…
  4. theorem OAI.ComparatorModel.CurrentMain.main line 75

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:600 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.main@path.