OAI/Computability/UniqueGames/PCP/TableIteration.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Iteration of the concrete stored-table round, with the original formula's actual initial graph size controlling the number of rounds.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.run line 18
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.runTables line 22

    Source documentation

    The same data computation on all validated tables; positivity is an invariant, and is erased from the runtime path.

    def runTables (H : BaseTable) : Nat → GraphTables.Table → GraphTables.Table :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.run_val line 25
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.iterationCount line 33
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output line 35
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.outputTable line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_val line 40
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.gapMap line 43
  9. opaque OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.degreeData line 47

    Source documentation

    A checked initialized degree avoids evaluating enormous fixed logarithms while applying polynomial identities. Its bound is part of the stored data.

    opaque degreeData : {n : Nat // sizeFactor ≤ 2 ^ n} :=
…
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.polynomialDegree line 50
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.sizeFactor_le_power line 52
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.run_completeness line 55
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_completeness line 59
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.gapMap_completeness line 63
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_darts_positive line 69
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.gapMap_nonempty line 73
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.run_size line 76
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_size line 80
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.initial_size_le line 85
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_size_le_input line 88
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.tableSizePolynomial line 96
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 99
  23. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.tableBitsPolynomial line 104
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.output_bits_le line 107
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.formulaBitsPolynomial line 112
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.TableIteration.gapMap_bits_le line 115