OAI/Computability/MaxCut/Games/Target.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MaxCutGames.Foundations.Target.Literal line 8
  2. def OAI.MaxCutGames.Foundations.Target.Literal.eval line 13
  3. abbrev OAI.MaxCutGames.Foundations.Target.Clause line 16
  4. def OAI.MaxCutGames.Foundations.Target.Clause.eval line 18
  5. structure OAI.MaxCutGames.Foundations.Target.Formula line 23

    Source documentation

    A finite conjunction of clauses with exactly three literal slots each. Repeated «variables» and repeated literals are allowed.

    structure Formula where
…
  6. def OAI.MaxCutGames.Foundations.Target.Formula.Satisfiable line 27
  7. structure OAI.MaxCutGames.Foundations.Target.PermutationTable line 33

    Source documentation

    Finite forward and inverse tables make totality and invertibility explicit. An eventual external encoding only needs to serialize the forward table.

    structure PermutationTable (alphabet : Nat) where
…
  8. theorem OAI.MaxCutGames.Foundations.Target.PermutationTable.images_injective line 39
  9. theorem OAI.MaxCutGames.Foundations.Target.PermutationTable.images_surjective line 44
  10. structure OAI.MaxCutGames.Foundations.Target.Constraint line 48
  11. def OAI.MaxCutGames.Foundations.Target.Constraint.satisfied line 53
  12. structure OAI.MaxCutGames.Foundations.Target.Instance line 59

    Source documentation

    Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation.

    structure Instance (alphabet : Nat) where
…
  13. def OAI.MaxCutGames.Foundations.Target.countSatisfied line 64
  14. theorem OAI.MaxCutGames.Foundations.Target.countSatisfied_le_length line 70
  15. theorem OAI.MaxCutGames.Foundations.Target.Instance.constraintCount_positive line 79
  16. structure OAI.MaxCutGames.Foundations.Target.RationalError line 87

    Source documentation

    The rational number numerator / denominator lies strictly between 0 and 1/2. No normalization to lowest terms is needed for the gap predicates.

    structure RationalError where
…
  17. def OAI.MaxCutGames.Foundations.Target.CompleteAt line 95

    Source documentation

    At least one labeling satisfies a fraction at least 1 - error.

    def CompleteAt {q : Nat} (error : RationalError) (game : Instance q) : Prop :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.RationalError, OAI.MaxCutGames.Foundations.Target.Instance

  18. def OAI.MaxCutGames.Foundations.Target.SoundAt line 102

    Source documentation

    Every labeling satisfies a fraction at most error.

    def SoundAt {q : Nat} (error : RationalError) (game : Instance q) : Prop :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.RationalError, OAI.MaxCutGames.Foundations.Target.Instance

  19. structure OAI.MaxCutGames.Foundations.Target.SemanticGapReduction line 109

    Source documentation

    Only the semantic part of a reduction. This is not a definition of an efficient reduction or an NP-hardness certificate.

    structure SemanticGapReduction (completenessError soundnessError : RationalError) where
…

    Mentions: OAI.MaxCutGames.Foundations.Target.RationalError