OAI/Computability/MaxCut/Games/CloneTable.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Reduction.CloneTable.cloneName line 15

    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.MaxCutGames.Reduction.CloneTable.cloneName_value line 21
  3. def OAI.MaxCutGames.Reduction.CloneTable.cloneEquation line 25
  4. def OAI.MaxCutGames.Reduction.CloneTable.clonedEquations line 30
  5. theorem OAI.MaxCutGames.Reduction.CloneTable.length_flatMap_map_inline_CloneTable line 33
  6. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedEquations_length line 43
  7. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedEquations_nonempty line 47
  8. theorem OAI.MaxCutGames.Reduction.CloneTable.cloned_sourceList line 54

    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.MaxCutGames.Reduction.FiniteSource.cloned, OAI.MaxCutGames.Reduction.CloneTable.clonedEquations

  9. theorem OAI.MaxCutGames.Reduction.CloneTable.cloned_ofList_sourceList line 68
  10. theorem OAI.MaxCutGames.Reduction.CloneTable.source_reconstructed line 73
  11. theorem OAI.MaxCutGames.Reduction.CloneTable.ofList_congr_inline_CloneTable line 84
  12. def OAI.MaxCutGames.Reduction.CloneTable.eraseEquation line 90
  13. def OAI.MaxCutGames.Reduction.CloneTable.natCloneEquation line 95

    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.MaxCutGames.Reduction.CloneTable.natClonedEquations line 98
  15. theorem OAI.MaxCutGames.Reduction.CloneTable.erase_cloneEquation line 101
  16. theorem OAI.MaxCutGames.Reduction.CloneTable.erase_clonedEquations line 108
  17. def OAI.MaxCutGames.Reduction.CloneTable.cloneEquationWords line 118
  18. def OAI.MaxCutGames.Reduction.CloneTable.clonedBodyWords line 122
  19. theorem OAI.MaxCutGames.Reduction.CloneTable.cloneEquation_words line 125
  20. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedEquations_words line 132
  21. def OAI.MaxCutGames.Reduction.CloneTable.clonedInput line 141
  22. def OAI.MaxCutGames.Reduction.CloneTable.clonedInputWords line 146
  23. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedInput_equations line 150
  24. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedInput_source line 155
  25. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedInput_words line 163
  26. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedInput_decodes line 168
  27. theorem OAI.MaxCutGames.Reduction.CloneTable.clonedInput_bits_length_le line 175

    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.MaxCutGames.Reduction.SourceEncoding.Input, OAI.MaxCutGames.Reduction.SourceEncoding.inputBits, OAI.MaxCutGames.Reduction.CloneTable.clonedInput