OAI/Computability/UniqueGames/Machines/GraphIterationBoundsLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

One polynomial bounds every actual intermediate encoding in the concrete logarithmic graph iteration. The linear recurrence is on graph size.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.inputBits line 19
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.countedBits line 21
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.words line 23
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.count line 26
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.lengthPolynomial line 28
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.inputBits_le_countedBits line 31
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.size_le_inputBits line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.count_le line 40
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.intermediate_size line 44
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.intermediate_bits line 52
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.runtimePolynomial line 68
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphIterationBounds.runtimePolynomial_eval line 72
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.finalTable line 92
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.counterCertificate line 95
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.countedCertificate line 105

    Source documentation

    The generic repeat machine executes only the actual successive graph words. Its polynomial bound uses the proved linear growth of their semantic sizes.

    noncomputable def countedCertificate :
    TM2ComputableInPolyTime countedBits GraphTables.tableBits (finalTable H) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.finalTable

  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.computableInPolyTime line 143

    Source documentation

    One actual finite machine computes the complete logarithmic iteration.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime inputBits GraphTables.tableBits (finalTable H) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.finalTable

  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.initialCertificate line 147
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.tableCertificate line 155

    Source documentation

    The initial graph and entire repeated table transformation have concrete finite-machine executions with the same formula and table encodings.

    noncomputable def tableCertificate :
    TM2ComputableInPolyTime formulaBits GraphTables.tableBits (TableIteration.outputTable H) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineTableIteration.gapMapCertificate line 164

    Source documentation

    Actual 3SAT gap-map runtime follows from the one concrete round certificate; initialization, variable repetition, and the final CNF converter are supplied.

    noncomputable def gapMapCertificate :
    TM2ComputableInPolyTime formulaBits formulaBits (TableIteration.gapMap H) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.initial line 178
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.finalCNF line 183
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.counter line 188
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.counted line 200
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.iteration line 203
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.table line 207
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.TableIterationFiniteAlphabet.gapMap line 211