OAI/Combinatorics/IndependentSets/Model.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LargeIndependentSets.Literal line 7

   Also declared: ComparatorChallenges/IndependentSets.lean:7 (same declaration text).

2. structure OAI.LargeIndependentSets.Formula line 12

   Also declared: ComparatorChallenges/IndependentSets.lean:12 (same declaration text).

3. def OAI.LargeIndependentSets.Formula.Satisfiable line 16

   Also declared: ComparatorChallenges/IndependentSets.lean:16 (same declaration text).

4. def OAI.LargeIndependentSets.frame line 21

   Source documentation

   Binary framing: true,b for a payload bit and false as terminator.

   Also declared: ComparatorChallenges/IndependentSets.lean:21 (same declaration text).

   def frame : List Bool → List Bool
     | [] => [false]
     | b :: bs => true :: b :: frame bs

5. def OAI.LargeIndependentSets.nameBits line 25

   Also declared: ComparatorChallenges/IndependentSets.lean:25 (same declaration text).

6. def OAI.LargeIndependentSets.literalBits line 27

   Also declared: ComparatorChallenges/IndependentSets.lean:27 (same declaration text).

7. def OAI.LargeIndependentSets.clauseBits line 29

   Also declared: ComparatorChallenges/IndependentSets.lean:29 (same declaration text).

8. def OAI.LargeIndependentSets.formulaBits line 32

   Also declared: ComparatorChallenges/IndependentSets.lean:32 (same declaration text).

9. structure OAI.LargeIndependentSets.Graph line 36

   Source documentation

   A nonempty, finite, simple, undirected, unweighted graph.

   Also declared: ComparatorChallenges/IndependentSets.lean:36 (same declaration text).

   structure Graph where
   …

10. def OAI.LargeIndependentSets.Graph.Independent line 43

    Also declared: ComparatorChallenges/IndependentSets.lean:43 (same declaration text).

11. instance OAI.LargeIndependentSets.(instance at line 46) line 46
12. def OAI.LargeIndependentSets.Graph.independenceNumber line 49

    Also declared: ComparatorChallenges/IndependentSets.lean:49 (same declaration text).

13. def OAI.LargeIndependentSets.Graph.ThreeColorable line 52

    Also declared: ComparatorChallenges/IndependentSets.lean:52 (same declaration text).

14. def OAI.LargeIndependentSets.graphBits line 57

    Source documentation

    Full explicit adjacency matrix, row-major, with binary vertex count.

    Also declared: ComparatorChallenges/IndependentSets.lean:57 (same declaration text).

    def graphBits (G : Graph) : List Bool :=
    …

    Mentions: OAI.LargeIndependentSets.Graph

15. structure OAI.LargeIndependentSets.RealGraphReduction line 65

    Source documentation

    Polynomial-time graph reduction with a real independence-ratio threshold.

    Also declared: ComparatorChallenges/IndependentSets.lean:65 (same declaration text).

    structure RealGraphReduction (δ : ℝ) where
    …