OAI/Computability/MaxCut/Games/TranslationTarget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Integration.TranslationTarget.IsTranslationInstance line 14
2. structure OAI.MaxCutGames.Integration.TranslationTarget.PolynomialGapReduction line 22

   Source documentation

   The full output form asserted in Theorem 1.1, including both real gaps, the actual polynomial-time machine, and one fixed binary alphabet.

   structure PolynomialGapReduction (ε δ : ℝ) extends RealTarget.PolynomialGapReduction ε δ where
   …

   Mentions: OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction

3. def OAI.MaxCutGames.Integration.TranslationTarget.ofRational line 28
4. theorem OAI.MaxCutGames.Integration.TranslationTarget.for_all_real_of_dyadic line 41

   Source documentation

   Full dyadic certificates suffice for all positive real tolerances, retaining the exact same translation coordinates and actual program in each instance.

   theorem for_all_real_of_dyadic
       (certificates : ∀ m n : Nat,
         ∃ p : Complexity.PolynomialGapReduction
           (DyadicErrors.dyadicError m) (DyadicErrors.dyadicError n),
         ∃ s : Nat, ∃ coordinates : Fin p.alphabet ≃ BinaryLinear.Vector s,
           ∀ formula, IsTranslationInstance coordinates (p.reduce formula))
       (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
       Nonempty (PolynomialGapReduction ε δ) := by
   …

   Mentions: OAI.MaxCutGames.Integration.DyadicErrors.dyadicError, OAI.MaxCutGames.Integration.BinaryLinear.Vector, OAI.MaxCutGames.Integration.TranslationTarget.IsTranslationInstance, OAI.MaxCutGames.Integration.TranslationTarget.PolynomialGapReduction

5. theorem OAI.MaxCutGames.Explicit.UniformTarget.copy_length line 62
6. def OAI.MaxCutGames.Explicit.UniformTarget.construct line 70
7. theorem OAI.MaxCutGames.Explicit.UniformTarget.vertices line 78
8. theorem OAI.MaxCutGames.Explicit.UniformTarget.edge_count line 81
9. theorem OAI.MaxCutGames.Explicit.UniformTarget.count_append_inline_UniformTarget line 85
10. theorem OAI.MaxCutGames.Explicit.UniformTarget.count_copies line 90
11. theorem OAI.MaxCutGames.Explicit.UniformTarget.count line 100
12. theorem OAI.MaxCutGames.Explicit.UniformTarget.maxSatisfied line 105
13. theorem OAI.MaxCutGames.Explicit.UniformTarget.value line 119
14. theorem OAI.MaxCutGames.Explicit.UniformTarget.mem_original line 129
15. theorem OAI.MaxCutGames.Explicit.UniformTarget.translations line 136
16. theorem OAI.MaxCutGames.Explicit.UniformTarget.flatMap_copies line 143
17. theorem OAI.MaxCutGames.Explicit.UniformTarget.encode_copies line 151
18. theorem OAI.MaxCutGames.Explicit.UniformTarget.gameWords_construct line 160

    Source documentation

    The complete output keeps the two first headers and scales the edge count.

    theorem gameWords_construct {q : Nat} (C : Nat) (hC : 0 < C) (g : Instance q) :
        gameWords (construct C hC g) =
          [g.vertices, q, C * g.constraints.length] ++
            copyMajor C (g.constraints.flatMap constraintWords) := by
    …

    Mentions: OAI.MaxCutGames.Explicit.UniformTarget.construct

19. theorem OAI.MaxCutGames.Explicit.UniformTarget.gameBits_construct line 168