OAI/Analysis/RecursivePotentials/Challenge.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Proved construction certificates and a statement-preservation check for the self-contained Comparator challenge. All eleven original conclusions are retained.

  1. def OAI.RecursivePotentials.rec_mainOriginalStatement line 14
  2. def OAI.RecursivePotentials.rec_completionOriginalStatement line 23
  3. def OAI.RecursivePotentials.stop_all_radiiOriginalStatement line 27
  4. def OAI.RecursivePotentials.XJoined_separated_familiesOriginalStatement line 30
  5. def OAI.RecursivePotentials.Variable.spaceOriginalStatement line 39
  6. def OAI.RecursivePotentials.Variable.lp_model_exactOriginalStatement line 50
  7. def OAI.RecursivePotentials.Variable.one_sided_modulus_zeroOriginalStatement line 58
  8. def OAI.RecursivePotentials.Variable.no_equivalent_AUCOriginalStatement line 61
  9. def OAI.RecursivePotentials.Variable.sixth_stabilityOriginalStatement line 64
  10. def OAI.RecursivePotentials.Variable.cubic_stabilityOriginalStatement line 68
  11. def OAI.RecursivePotentials.Variable.weak_tailOriginalStatement line 72
  12. def OAI.RecursivePotentials.OriginalResults line 79
  13. theorem OAI.ComparatorModel.RecursivePotentials.rootStatement_iff line 132
  14. theorem OAI.ComparatorModel.RecursivePotentials.zeroStatement_iff line 136
  15. theorem OAI.ComparatorModel.RecursivePotentials.sourceNormStatement_iff line 140
  16. theorem OAI.ComparatorModel.RecursivePotentials.result0_iff line 144
  17. theorem OAI.ComparatorModel.RecursivePotentials.result1_iff line 146
  18. theorem OAI.ComparatorModel.RecursivePotentials.result2_iff line 150
  19. theorem OAI.ComparatorModel.RecursivePotentials.result3_iff line 152
  20. theorem OAI.ComparatorModel.RecursivePotentials.variableCoordinate_eq line 156

    Source comment

    Compare the finite-rank projections pointwise, so the statement comparison does not repeatedly unfold the completion and operator-space instances.
    private theorem variableCoordinate_eq (s : Variable.Node) :
    Variable.coordinate s = _root_.OAI.RecursivePotentials.Variable.coordinate s := rfl

    Mentions: OAI.ComparatorModel.RecursivePotentials.Variable.Node, OAI.ComparatorModel.RecursivePotentials.Variable.coordinate

  21. theorem OAI.ComparatorModel.RecursivePotentials.variableBasis_eq line 159
  22. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_apply line 162
  23. theorem OAI.ComparatorModel.RecursivePotentials.originalVariableProjection_apply line 166
  24. theorem OAI.ComparatorModel.RecursivePotentials.variableAddCommMonoid_eq line 175
  25. theorem OAI.ComparatorModel.RecursivePotentials.variableModule_eq line 179
  26. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_sum_eq line 183
  27. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_apply_eq line 191
  28. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_eq line 196
  29. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_toLinearMap_eq line 200
  30. theorem OAI.ComparatorModel.RecursivePotentials.variableProjection_finiteDimensional_iff line 206
  31. theorem OAI.ComparatorModel.RecursivePotentials.variableFiniteTotalSupport_iff line 212
  32. theorem OAI.ComparatorModel.RecursivePotentials.result4_iff line 218
  33. theorem OAI.ComparatorModel.RecursivePotentials.result5_iff line 224
  34. theorem OAI.ComparatorModel.RecursivePotentials.result6_iff line 226
  35. theorem OAI.ComparatorModel.RecursivePotentials.result7_iff line 228
  36. theorem OAI.ComparatorModel.RecursivePotentials.result8_iff line 230
  37. theorem OAI.ComparatorModel.RecursivePotentials.result9_iff line 232
  38. theorem OAI.ComparatorModel.RecursivePotentials.result10_iff line 234
  39. theorem OAI.ComparatorModel.RecursivePotentials.results_iff_original line 236
  40. theorem OAI.ComparatorModel.RecursivePotentials.main_iff_original line 251

    Source documentation

    Packaging the construction obligations preserves the original eleven statements.

    theorem main_iff_original : MainClaim ↔ _root_.OAI.RecursivePotentials.OriginalResults := by
…

    Mentions: OAI.ComparatorModel.RecursivePotentials.MainClaim

  41. theorem OAI.ComparatorModel.RecursivePotentials.main line 259

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: OAI.ComparatorModel.RecursivePotentials.MainClaim

    Proof uses: Iff.mpr, OAI.RecursivePotentials.OriginalResults, OAI.ComparatorModel.RecursivePotentials.main_iff_original, And.intro, OAI.RecursivePotentials.rec_mainOriginalStatement, And, OAI.RecursivePotentials.rec_completionOriginalStatement, OAI.RecursivePotentials.stop_all_radiiOriginalStatement, OAI.RecursivePotentials.XJoined_separated_familiesOriginalStatement, OAI.RecursivePotentials.Variable.spaceOriginalStatement, OAI.RecursivePotentials.Variable.lp_model_exactOriginalStatement, OAI.RecursivePotentials.Variable.one_sided_modulus_zeroOriginalStatement, OAI.RecursivePotentials.Variable.no_equivalent_AUCOriginalStatement, OAI.RecursivePotentials.Variable.sixth_stabilityOriginalStatement, OAI.RecursivePotentials.Variable.cubic_stabilityOriginalStatement, OAI.RecursivePotentials.Variable.weak_tailOriginalStatement, OAI.RecursivePotentials.rec_main, OAI.RecursivePotentials.rec_completion, OAI.RecursivePotentials.stop_all_radii, OAI.RecursivePotentials.XJoined_separated_families and 7 more

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:955 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.main@path.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.