GraphDecidability.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Decidability of fixed-size graph witnesses

Connectivity is characterized by containment in every Boolean equivalence relation containing the marked edges. On a finite carrier this gives an executable decision procedure, and hence a decision procedure for the existence of a graph witness at each fixed size. The size of a witness in HasGraphWitness is not bounded by these results.

def OAI.FiniteCongruence.ClosedMarking line 18

Source documentation

A Boolean relation is closed if it is an equivalence containing every marked edge.

def ClosedMarking {Lat Carrier : Type} [LE Lat] (color : Carrier → Carrier → Lat)
    (seeds : Finset (Carrier × Carrier)) (rel : Carrier → Carrier → Bool) : Prop :=
…

theorem OAI.FiniteCongruence.connected_iff_closedMarkings line 27
Source documentation
Connectivity is the intersection of the Boolean equivalence relations containing all marked edges. This characterization uses classical logic but allows finite enumeration.
```
theorem connected_iff_closedMarkings {Lat Carrier : Type} [LE Lat]
    (color : Carrier → Carrier → Lat) (seeds : Finset (Carrier × Carrier)) (left right : Carrier) :
    Connected color seeds left right ↔
      ∀ rel : Carrier → Carrier → Bool, ClosedMarking color seeds rel → rel left right = true := by
…
```
Mentions: OAI.FiniteCongruence.Connected, OAI.FiniteCongruence.ClosedMarking
instance OAI.FiniteCongruence.decidableAdmissible line 56
instance OAI.FiniteCongruence.decidableMarked line 62
instance OAI.FiniteCongruence.decidableClosedMarking line 70
instance OAI.FiniteCongruence.decidableConnected line 80

def OAI.FiniteCongruence.graphWitnessDecidable line 89

Source documentation

An executable fixed-size test, with no classical choice in its computational content.

def graphWitnessDecidable (Lat Carrier : Type) [Fintype Lat] [Lattice Lat] [OrderBot Lat]
    [DecidableEq Lat] [DecidableLE Lat] [Fintype Carrier] [DecidableEq Carrier]
    (color : Carrier → Carrier → Lat) : Decidable (IsGraphWitness color) :=
…

Mentions: OAI.FiniteCongruence.IsGraphWitness

def OAI.FiniteCongruence.graphSizeDecidable line 103

Source documentation

Existence of a colored-graph witness at a fixed candidate size is decidable.

def graphSizeDecidable (Lat : Type) [Fintype Lat] [Lattice Lat] [OrderBot Lat]
    [DecidableEq Lat] [DecidableLE Lat] (size : ℕ) :
    Decidable (0 < size ∧ ∃ color : Fin size → Fin size → Lat, IsGraphWitness color) := by
…

Mentions: OAI.FiniteCongruence.IsGraphWitness