OAI/Computability/MaxCut/PCP/PreprocessingStageMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Executable, codec-compatible stage maps for the actual preprocessing constructor. The decomposition below is an equality of its existing functions; runtime certificates must be supplied by the respective concrete machines.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.BaseTable line 12
  2. def OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.regular line 14
  3. def OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.padding line 17
  4. def OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.familyAt line 21
  5. def OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.paddedOverlay line 26
  6. def OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.lazy line 31
  7. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.output_eq line 36

    Source documentation

    Exact equality with the original executable constructor, including all chosen row coordinates and the actual fixed base table.

    theorem output_eq (H : BaseTable) (t : GraphTables.Table) :
    PreprocessingTables.output H t =
      lazy ((internalDegree + 1) + internalDegree)
        (paddedOverlay H (internalDegree + 1) (regular H t)) := rfl
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.BaseTable, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.output, OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.lazy, OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.paddedOverlay, OAI.MaxCutGames.Foundations.PCP.PreprocessingStageMaps.regular