OAI/Computability/UniqueGames/Games/ProductSoundness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The final graph product inherits the alphabet-independent repetition estimate through its proved uniform occurrence law and arbitrary-local-strategy bridge. The only input soundness premise is the base graph's actual finite maximum.

  1. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_soundness_rate line 26
  2. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_soundness line 33
  3. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.product_explicit_soundness line 39
  4. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_soundness_rate line 54
  5. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_soundness line 62
  6. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.binaryProduct_explicit_soundness line 69
  7. theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_soundness_rate line 92

    Source documentation

    Soundness for the actual globally numbered, fully tabulated output.

    theorem output_soundness_rate (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t)
    (hvalue : Integration.InstanceValue.value H ≤ 1 - (1 : ℝ) / 800) :
    Integration.InstanceValue.value (output H presentation t ht) ≤
      (1 - (1 : ℝ) / 10240000) ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output

  8. theorem OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output_soundness line 103