OAI/Computability/MaxCut/Games/GapSemantics.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Exact bridges between the integer-encoded target gaps and acceptance rates. Repeated constraint entries retain their multiplicity in every definition.

  1. def OAI.MaxCutGames.Integration.GapSemantics.errorValue line 13
  2. def OAI.MaxCutGames.Integration.GapSemantics.satisfactionRate line 15
  3. theorem OAI.MaxCutGames.Integration.GapSemantics.countSatisfied_eq_sum line 18
  4. theorem OAI.MaxCutGames.Integration.GapSemantics.countSatisfied_ofFn line 26
  5. def OAI.MaxCutGames.Integration.GapSemantics.uniformConstraintAcceptance line 33
  6. theorem OAI.MaxCutGames.Integration.GapSemantics.uniformConstraintAcceptance_eq_rate line 40

    Source documentation

    Uniform sampling is over occurrence indices, so equal constraints are counted with exactly their stored multiplicity.

    theorem uniformConstraintAcceptance_eq_rate {q : Nat} (g : Instance q)
    (labeling : Fin g.vertices → Fin q) :
    uniformConstraintAcceptance g labeling = satisfactionRate g labeling := by
…

    Mentions: OAI.MaxCutGames.Integration.GapSemantics.uniformConstraintAcceptance, OAI.MaxCutGames.Integration.GapSemantics.satisfactionRate

  7. theorem OAI.MaxCutGames.Integration.GapSemantics.errorValue_pos line 51
  8. theorem OAI.MaxCutGames.Integration.GapSemantics.errorValue_lt_half line 56
  9. theorem OAI.MaxCutGames.Integration.GapSemantics.satisfactionRate_nonneg line 63
  10. theorem OAI.MaxCutGames.Integration.GapSemantics.satisfactionRate_le_one line 67
  11. theorem OAI.MaxCutGames.Integration.GapSemantics.completeAt_iff line 75
  12. theorem OAI.MaxCutGames.Integration.GapSemantics.soundAt_iff line 100
  13. theorem OAI.MaxCutGames.Integration.GapSemantics.completeAt_mono line 121

    Source documentation

    Strengthening either error threshold implies the requested weaker gap.

    theorem completeAt_mono {q : Nat} {e e' : RationalError} {g : Instance q}
    (hee : errorValue e ≤ errorValue e') (hg : CompleteAt e g) : CompleteAt e' g := by
…

    Mentions: OAI.MaxCutGames.Integration.GapSemantics.errorValue

  14. theorem OAI.MaxCutGames.Integration.GapSemantics.soundAt_mono line 127
  15. theorem OAI.MaxCutGames.Integration.GapSemantics.completeAt_iff_real line 134

    Source documentation

    The same target gap is obtained when the analysis uses real expectations.

    theorem completeAt_iff_real {q : Nat} (e : RationalError) (g : Instance q) :
    CompleteAt e g ↔ ∃ labeling,
      1 - (errorValue e : ℝ) ≤
        (countSatisfied labeling g.constraints : ℝ) / g.constraints.length := by
…

    Mentions: OAI.MaxCutGames.Integration.GapSemantics.errorValue

  16. theorem OAI.MaxCutGames.Integration.GapSemantics.soundAt_iff_real line 145
  17. def OAI.MaxCutGames.Integration.InstanceEquivalences.renameConstraint line 165
  18. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.renameConstraint_satisfied line 171
  19. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.rename_count line 175
  20. def OAI.MaxCutGames.Integration.InstanceEquivalences.renameInstance line 184
  21. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.countSatisfied_perm line 192
  22. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.satisfactionRate_eq_of_rename_perm line 201

    Source documentation

    This statement is directly usable by an executable adapter: only its vertex equivalence and its permutation of the explicit edge list are needed.

    theorem satisfactionRate_eq_of_rename_perm {q : Nat} (g h : Instance q)
    (e : Fin g.vertices ≃ Fin h.vertices)
    (hp : h.constraints.Perm (g.constraints.map (renameConstraint e)))
    (labeling : Fin h.vertices → Fin q) :
    satisfactionRate h labeling = satisfactionRate g (labeling ∘ e) := by
…

    Mentions: OAI.MaxCutGames.Integration.InstanceEquivalences.renameConstraint

  23. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.completeAt_iff_of_rename_perm line 213
  24. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.soundAt_iff_of_rename_perm line 227
  25. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.rename_rate line 241
  26. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.completeAt_rename_iff line 246
  27. theorem OAI.MaxCutGames.Integration.InstanceEquivalences.soundAt_rename_iff line 251