OAI/Optimization/Tropical/TruffetCounterexample.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A forced pair of tropical substitutions with a strictly better feasible point.

  1. lemma OAI.TruffetV4Counterexample.fin3_two_ne_one line 10
  2. lemma OAI.TruffetV4Counterexample.fin3_two_ne_zero line 12
  3. lemma OAI.TruffetV4Counterexample.coeff_one_add_neg_one line 14
  4. theorem OAI.TruffetV4Counterexample.Row.ext line 18
  5. theorem OAI.TruffetV4Counterexample.State.ext line 25
  6. lemma OAI.TruffetV4Counterexample.initial_crossRowRestriction line 34
  7. lemma OAI.TruffetV4Counterexample.advance_first line 49
  8. lemma OAI.TruffetV4Counterexample.advance_second line 64
  9. lemma OAI.TruffetV4Counterexample.first_forced line 79
  10. lemma OAI.TruffetV4Counterexample.second_forced line 88
  11. lemma OAI.TruffetV4Counterexample.final_terminal line 98
  12. lemma OAI.TruffetV4Counterexample.finite_search_domain line 101
  13. lemma OAI.TruffetV4Counterexample.output_backsubstitution line 109
  14. lemma OAI.TruffetV4Counterexample.output_cost_and_feasible line 115
  15. lemma OAI.TruffetV4Counterexample.better_feasible_and_cost line 121
  16. theorem OAI.TruffetV4Counterexample.finite_execution_not_optimal line 126

    Distinct definitions of this name: ComparatorChallenges/TruffetCounterexample.lean:118 (same statement text; different proof or body). Qualify references as OAI.TruffetV4Counterexample.finite_execution_not_optimal@path.