OAI/Computability/UniqueGames/Reduction/RealTargetLemmas.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction line 28

   Source documentation

   A fixed-alphabet gap reduction from 3SAT, including its actual finite-machine polynomial runtime, with the two approximation thresholds expressed over ℝ.

   structure PolynomialGapReduction (ε δ : ℝ) where
   …

2. def OAI.UniqueGamesTheorem.Integration.RealTarget.ofRational line 44

   Source documentation

   A genuine rational-error certificate supplies every weaker real threshold. The input and output encodings and finite transition program remain identical.

   def ofRational {e d : RationalError} {ε δ : ℝ}
       (p : Complexity.PolynomialGapReduction e d)
       (hε : (GapSemantics.errorValue e : ℝ) ≤ ε)
       (hδ : (GapSemantics.errorValue d : ℝ) ≤ δ) : PolynomialGapReduction ε δ where
   …

   Mentions: OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue, OAI.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction

3. theorem OAI.UniqueGamesTheorem.Integration.RealTarget.for_all_real_of_dyadic line 63

   Source documentation

   It suffices to construct the full machine-backed reduction for dyadic errors. This theorem does not assert that those certificates have been built.

   theorem for_all_real_of_dyadic
       (certificates : ∀ m n : Nat, Nonempty
         (Complexity.PolynomialGapReduction
           (DyadicErrors.dyadicError m) (DyadicErrors.dyadicError n)))
       (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
       Nonempty (PolynomialGapReduction ε δ) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError, OAI.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction

4. def OAI.UniqueGamesTheorem.Integration.InstanceValue.maxSatisfied line 94

   Source documentation

   The maximum number of satisfied occurrences among all vertex labelings.

   def maxSatisfied {q : Nat} (g : Instance q) : Nat :=
   …

5. def OAI.UniqueGamesTheorem.Integration.InstanceValue.value line 100

   Source documentation

   The usual instance value: the largest satisfied fraction of its stored constraint list. The denominator is positive by the Instance invariant.

   noncomputable def value {q : Nat} (g : Instance q) : ℝ :=
   …

6. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.countSatisfied_le_maxSatisfied line 103
7. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.maxSatisfied_le_length line 111
8. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.maxSatisfied_attained line 117
9. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.value_attained line 126
10. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.labeling_rate_le_value line 132
11. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.satisfactionRate_le_value line 140

    Source documentation

    This value uses the same rate already defined for the encoded gap target.

    theorem satisfactionRate_le_value {q : Nat} (g : Instance q)
        (labeling : Fin g.vertices → Fin q) :
        (GapSemantics.satisfactionRate g labeling : ℝ) ≤ value g := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.GapSemantics.satisfactionRate, OAI.UniqueGamesTheorem.Integration.InstanceValue.value

12. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.value_nonneg line 145
13. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.value_le_one line 148
14. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.value_mem_unitInterval line 154
15. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.exists_rate_ge_iff line 158

    Source documentation

    Existential real completeness is precisely a lower bound on instance value.

    theorem exists_rate_ge_iff {q : Nat} (g : Instance q) (hq : 0 < q) (a : ℝ) :
        (∃ labeling : Fin g.vertices → Fin q,
          a ≤ (countSatisfied labeling g.constraints : ℝ) / g.constraints.length) ↔
          a ≤ value g := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value

16. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.forall_rate_le_iff line 170

    Source documentation

    Universal real soundness is precisely an upper bound on instance value.

    theorem forall_rate_le_iff {q : Nat} (g : Instance q) (hq : 0 < q) (b : ℝ) :
        (∀ labeling : Fin g.vertices → Fin q,
          (countSatisfied labeling g.constraints : ℝ) / g.constraints.length ≤ b) ↔
          value g ≤ b := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value

17. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.completeAt_iff_value line 181
18. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.soundAt_iff_value line 186
19. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.realTarget_completeness line 192

    Source documentation

    The unchanged real target certificate gives literal val(U) ≥ 1 - ε.

    theorem realTarget_completeness {ε δ : ℝ}
        (p : RealTarget.PolynomialGapReduction ε δ) (formula : Formula)
        (hformula : formula.Satisfiable) :
        1 - ε ≤ value (p.reduce formula) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction, OAI.UniqueGamesTheorem.Integration.InstanceValue.value

20. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.realTarget_soundness line 201

    Source documentation

    The unchanged real target certificate gives literal val(U) ≤ δ.

    theorem realTarget_soundness {ε δ : ℝ}
        (p : RealTarget.PolynomialGapReduction ε δ) (formula : Formula)
        (hformula : ¬ formula.Satisfiable) :
        value (p.reduce formula) ≤ δ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction, OAI.UniqueGamesTheorem.Integration.InstanceValue.value

21. theorem OAI.UniqueGamesTheorem.Integration.InstanceValue.realTarget_value_guarantees line 209
22. structure OAI.UniqueGamesTheorem.Integration.TranslationTarget.PolynomialGapReduction line 230

    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.UniqueGamesTheorem.Integration.RealTarget.PolynomialGapReduction

23. def OAI.UniqueGamesTheorem.Integration.TranslationTarget.ofRational line 236
24. theorem OAI.UniqueGamesTheorem.Integration.TranslationTarget.for_all_real_of_dyadic line 249

    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.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError, OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector, OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance, OAI.UniqueGamesTheorem.Integration.TranslationTarget.PolynomialGapReduction

25. def OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedConstraint line 277
26. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedConstraint_satisfied line 283
27. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedConstraint_permutation line 287
28. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.count_map line 290
29. def OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedInstance line 299
30. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedInstance_vertices line 305
31. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedInstance_constraints line 309
32. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.embedInstance_length line 313
33. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.count_embed line 317
34. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.satisfactionRate_embed line 323
35. def OAI.UniqueGamesTheorem.Integration.VertexEmbedding.extendLabeling line 332

    Source documentation

    The extension is only used as a semantic witness, not by the instance constructor.

    noncomputable def extendLabeling {n m q : Nat} (f : Fin n → Fin m)
        (labeling : Fin n → Fin q) (defaultLabel : Fin q) (v : Fin m) : Fin q := by
    …

36. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.extendLabeling_apply line 337
37. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.extendLabeling_comp line 346
38. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.soundAt_embed line 352
39. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.completeAt_embed line 360
40. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.completeAt_embed_iff line 368
41. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.soundAt_embed_iff line 378
42. theorem OAI.UniqueGamesTheorem.Integration.VertexEmbedding.isTranslationInstance_embed_iff line 387
43. abbrev OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.E line 410
44. abbrev OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.Ambient line 411
45. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.tau line 415
46. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.hBasis line 416
47. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.firstBasis line 417
48. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.secondBasis line 418
49. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.coordinateBasis line 419
50. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.tau_hBasis line 422
51. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.tau_firstBasis line 423
52. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.tau_secondBasis line 424
53. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.pair_fst_ite line 426
54. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.pair_snd_ite line 428
55. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.coordinate_decomposition line 431
56. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.linearMap_expansion line 441
57. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.homogeneous line 448
58. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.embed line 468
59. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.embed_mem line 484
60. def OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.equivalence line 494
61. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.finrank_E line 516
62. theorem OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.finrank_homogeneous line 519