OAI/Computability/UniqueGames/PCP/SourceTupleBound.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial bounds for the actual tuple-body phase budgets. The budget being bounded is the one used by the checked machine traces.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.clauseRank_le_power line 18
  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.variableRank_le_power line 24
  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.leftValue_le_numberBound line 31
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.rightValue_le_numberBound line 37
  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.leftBlock_le_numberBound line 42
  6. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.rankPolynomial line 50
  7. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.numberPolynomial line 51
  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.rankPolynomial_eval line 54
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.numberPolynomial_eval line 56
  10. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.slotPolynomial line 60
  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.slotPolynomial_eval line 67
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.slotBudget_le line 76
  13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.prefixBudget_le line 95
  14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.preparePolynomial line 109
  15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.preparePolynomial_eval line 114
  16. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.setupPolynomial line 121
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.setupPolynomial_eval line 127
  18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.finishPolynomial line 135
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.finishPolynomial_eval line 139
  20. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyPolynomial line 145
  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.setupBudget_le line 148
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.finishBudget_le line 165
  23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyBudget_le line 173

    Source documentation

    One fixed polynomial bounds the actual tuple-body budget for every tuple.

    theorem bodyBudget_le (F : Target.Formula) (c : ClauseContext F u) :
    bodyBudget (D := D) F c ≤ (bodyPolynomial u D).eval (formulaBits F).length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyPolynomial

  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.fixed_parameters_body_bound line 182
  25. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyInPolynomialTime line 188

    Source documentation

    The actual body execution with the same fixed polynomial for every tuple.

    theorem bodyInPolynomialTime {Extra : Type} [DecidableEq Extra]
    (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : SourceRuntimeModel.Arena u Extra → List Bool) (h : Ready F c base) :
    Nonempty (StateTransition.EvalsToInTime (Turing.TM2.step (program initialQuery exit))
      ⟨some main, SourceRuntimeModel.canonicalState initialQuery, base⟩
      (some ⟨exit, SourceRuntimeModel.canonicalState initialQuery,
        SourceTestAppend.resultTapes SourceRuntimeModel.queryLayout base
          (SourceQueryOrder.tupleBits F u D c)⟩)
      ((bodyPolynomial u D).eval (formulaBits F).length)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.canonicalState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeModel.queryLayout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBound.bodyPolynomial