OAI/Computability/UniqueGames/Machines/MachineExpanderFamilyBoundsLemmas.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Bounds for materializing the actual expander family

The costs use the encoded old and new rotation tables, and the already checked table-machine polynomial. The finite sum follows the actual recursive table family. These arithmetic lemmas introduce no execution assumptions and make no claim that the output is polynomial in an isolated binary level parameter.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 21
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 27
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 32

    Source documentation

    The complete unary encoding, including every word delimiter, is counted.

    theorem wordLength_add_one_le {v q N : Nat} (G : Table v q) (hv : v ≤ N) :
    (encodeWords (rotationWords G)).length + 1 ≤ (q + 1)^2 * (N + 1)^2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 43
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 81
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 87
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 99
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 102
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 105
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 109
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 114
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 117
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 120
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 126
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 154

    Source documentation

    All actual resize costs plus the counted-loop overhead.

    theorem familyBudget_le {d : Nat} (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (level : Nat) :
    familyBudget H level ≤
      (resizeCoefficient d + 4) * (vertexCount (degree d) level + 1)^5 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient

  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 168
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 178
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 183

    Source documentation

    For the fixed base graph, the bounded padding level has a polynomial cost in the requested unary size, including size zero.

    theorem familyBudget_at_boundedLevel_le
    (H : Table (cloudSize PCP.Expanders.baseDegree) PCP.Expanders.baseDegree) (k : Nat) :
    familyBudget H (PCP.PreprocessingLevels.boundedLevel k) ≤ inputCoefficient * (k + 1)^5 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient

  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cycleWords line 215

    Source documentation

    The six nonempty tape roles that may occur between expansion phases.

    def cycleWords (remaining : Nat) (word current vertex count result suffix : List Bool) :
    Tape → List Bool
  | .inl (.inl .table) => word
  | .inl (.inl .inputVertex) => vertex
  | .inl (.inr .vertexCount) => count
  | .inl (.inr .result) => result
  | .inr .remainingLevel => encodeWord remaining ++ suffix
  | .inr .currentSize => current
  | _ => []

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 225
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 229
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 234
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.copyFrame line 244
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.returnFrame line 249
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installedFrame line 254
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 258
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 263
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 275
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 289
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 300
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 317
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 328
  33. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 344
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 359

    Source documentation

    The resize certificate is built from actual primitive and table executions; its caller supplies no phase trace or computational hypothesis.

    noncomputable def resizeInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (G : Table v (degree d)) (remaining : Nat) (state : State ρ d) (suffix : List Bool) :
    ResizeRun positive H growth G remaining state suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.ResizeRun