OAI/Computability/UniqueGames/Reduction/CloneTable.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Reduction.CloneTable.cloneName line 17

    Source documentation

    A total bounded-name helper. Every index used by the table is below 48, and cloneName_value removes the remainder operation on those indices.

    def cloneName (v : Fin n) (i : Nat) : Fin (n * 48) :=
…
  2. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.cloneName_value line 23
  3. def OAI.UniqueGamesTheorem.Reduction.CloneTable.cloneEquation line 27
  4. def OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedEquations line 32
  5. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.length_flatMap_map line 35
  6. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedEquations_length line 45
  7. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedEquations_nonempty line 49
  8. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.cloned_sourceList line 56

    Source documentation

    Exact equality of typed ordered lists, not just permutation or equal counts.

    theorem cloned_sourceList (S : Source) :
    (FiniteSource.cloned S).sourceList = clonedEquations S.sourceList := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.FiniteSource.cloned, OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedEquations

  9. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.cloned_ofList_sourceList line 70
  10. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.source_reconstructed line 75
  11. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.ofList_congr line 86
  12. def OAI.UniqueGamesTheorem.Reduction.CloneTable.eraseEquation line 92
  13. def OAI.UniqueGamesTheorem.Reduction.CloneTable.natCloneEquation line 97

    Source documentation

    Numeric machine target: no remainder, bounded-name proofs, or function lookup is needed in the three generated variable names.

    def natCloneEquation (e : Equation Nat) (t : Nat × Nat × Nat) : Equation Nat :=
…
  14. def OAI.UniqueGamesTheorem.Reduction.CloneTable.natClonedEquations line 100
  15. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.erase_cloneEquation line 103
  16. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.erase_clonedEquations line 110
  17. def OAI.UniqueGamesTheorem.Reduction.CloneTable.cloneEquationWords line 120
  18. def OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedBodyWords line 124
  19. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.cloneEquation_words line 127
  20. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedEquations_words line 134
  21. def OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput line 143
  22. def OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInputWords line 148
  23. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput_equations line 152
  24. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput_source line 157
  25. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput_words line 165
  26. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput_decodes line 170
  27. theorem OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput_bits_length_le line 177

    Source documentation

    A size bound for the actual serialized intermediate table. This is not a machine-time bound.

    theorem clonedInput_bits_length_le (input : SourceEncoding.Input) :
    (SourceEncoding.inputBits (clonedInput input)).length ≤
      48 * input.variables + distinctTriples.length * input.equations.length + 2 +
        distinctTriples.length * input.equations.length * (144 * input.variables + 2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits, OAI.UniqueGamesTheorem.Reduction.CloneTable.clonedInput