OAI/Computability/UniqueGames/Reduction/SourceIncidenceLemmas.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Reduction.SourceIncidence.toIncidence line 14
  2. theorem OAI.UniqueGamesTheorem.Reduction.SourceIncidence.failedEquation_eq line 17
  3. theorem OAI.UniqueGamesTheorem.Reduction.SourceIncidence.failureCount_eq line 24
  4. def OAI.UniqueGamesTheorem.Reduction.SourceIncidence.occurrenceList line 36

    Source documentation

    The full occurrence is the displayed equation together with a fresh index.

    def occurrenceList (source : List (CloneGap.Equation Name)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation

  5. theorem OAI.UniqueGamesTheorem.Reduction.SourceIncidence.cloned_occurrence_gap line 39
  6. theorem OAI.UniqueGamesTheorem.Reduction.SourceIncidence.source_to_incidence_soundness line 58
  7. abbrev OAI.UniqueGamesTheorem.Reduction.FiniteSource.Name line 80
  8. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.clonedSource line 82
  9. abbrev OAI.UniqueGamesTheorem.Reduction.FiniteSource.Occurrence line 84
  10. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.occurrences line 86
  11. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.rawEquation line 89
  12. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.finiteName line 94

    Source documentation

    Total conversion; membership proofs below establish that every index used by the construction is already below 48, so the remainder changes none.

    def finiteName (s : ActualSource.Source) (v : Fin s.variables × Nat) : Name s :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.FiniteSource.Name

  13. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.mapEquation line 97
  14. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.equation line 100
  15. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.satisfied_map line 103
  16. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.mem_cart line 106
  17. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.distinctTriple_bounds line 116
  18. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.distinctTriples_nonempty line 123
  19. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned_member_properties line 128
  20. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.raw_properties line 139
  21. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.finiteName_injective_on line 148
  22. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.names_distinct line 154
  23. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.raw_map_occurrences line 163
  24. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.occurrences_length line 167
  25. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.clonedSource_nonempty line 171
  26. instance OAI.UniqueGamesTheorem.Reduction.FiniteSource.(instance at line 177) line 177
  27. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.indexed_failure_count line 180
  28. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.indexed_gap line 187
  29. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.indexed_completeness_count line 196
  30. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.incidenceEquation line 207
  31. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.incidence_question_predicate line 210
  32. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.incidence_failure_gap line 219
  33. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.incidence_soundness line 229
  34. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.nameEquiv line 238

    Source documentation

    Executable row-major encoding of the finite clone names.

    def nameEquiv (s : ActualSource.Source) : Name s ≃ Fin (s.variables * 48) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.FiniteSource.Name

  35. def OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned line 241
  36. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned_length line 247
  37. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned_distinct line 252
  38. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.count_ofFn line 259
  39. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned_gap line 266
  40. theorem OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned_completeness_count line 281