The formulas of the reduction of #1-in-SAT to #Cycle Cover

The reduction draws, over the ordered expansion of a CNF formula, the ladder expansion (DescriptiveComplexity.ladder) of the base graph with Valiant's gadgets attached (DescriptiveComplexity.Site.flatAttach). This file names the tags and writes the first-order formulas the drawing is made of, each with its realization lemma; the drawing itself is in DescriptiveComplexity.Problems.CycleCover.Drawing.

• A node of the attached graph is a tagged pair (c, x): a track node, a spoke or a gadget node of the occurrence of the literal (x, s) in the clause c (the dummy occurrence of x being written (x, x)), or the hub of the clause c or of the variable x (written (c, c) and (x, x)). DescriptiveComplexity.SatCover.vDomF says which pairs are nodes of which tag, DescriptiveComplexity.SatCover.flatEntryF which entries the attached matrix has between them.
• A level of the ladders is a tagged pair too: one level per occurrence and index in Fin 3, and one more, the pair of least elements. The levels are ordered lexicographically (DescriptiveComplexity.SatCover.levelLeF), and the least level, the greatest and the cover relation are first-order.
• A rung is a node, a node, a level and an index below the width (DescriptiveComplexity.SatCover.widthF).

Tags

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.OccTag : Type

The tag of an occurrence: whether it is the dummy one, and its sign.

Equations

• DescriptiveComplexity.SatCover.OccTag = (Bool × Bool)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.NodeTag : Type

The tags of the nodes of the base graph: track nodes and spokes of an occurrence, and hubs, of a clause (true) or of a variable (false).

Equations

• DescriptiveComplexity.SatCover.NodeTag = (DescriptiveComplexity.SatCover.OccTag ⊕ DescriptiveComplexity.SatCover.OccTag ⊕ Bool)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.VTag : Type

The tags of the nodes of the attached graph: base nodes, and the four gadget nodes of an occurrence.

Equations

• DescriptiveComplexity.SatCover.VTag = (DescriptiveComplexity.SatCover.NodeTag ⊕ DescriptiveComplexity.SatCover.OccTag × Fin 4)

def DescriptiveComplexity.SatCover.LevelTag : Type

The tags of the levels: one per occurrence and index, and one more. A definition rather than an abbreviation, so that the only order on it is the one declared here.

Equations

• DescriptiveComplexity.SatCover.LevelTag = Option (DescriptiveComplexity.SatCover.OccTag × Fin 3)

instance DescriptiveComplexity.SatCover.instFiniteLevelTag : Finite LevelTag

@[instance_reducible]

instance DescriptiveComplexity.SatCover.instDecidableEqLevelTag : DecidableEq LevelTag

Equations

• DescriptiveComplexity.SatCover.instDecidableEqLevelTag = DescriptiveComplexity.SatCover.instDecidableEqLevelTag._aux_1

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instLinearOrderLevelTag : LinearOrder LevelTag

Equations

• DescriptiveComplexity.SatCover.instLinearOrderLevelTag = DescriptiveComplexity.finiteLinearOrder DescriptiveComplexity.SatCover.LevelTag

def DescriptiveComplexity.SatCover.LevelTag.extra : LevelTag

The extra level.

Equations

• DescriptiveComplexity.SatCover.LevelTag.extra = none

def DescriptiveComplexity.SatCover.LevelTag.pos (o : OccTag) (k : Fin 3) : LevelTag

The level of an occurrence tag and an index.

Equations

• DescriptiveComplexity.SatCover.LevelTag.pos o k = some (o, k)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.DrawTag : Type

The tags of the drawing: the nodes of the attached graph, and the rungs, tagged by their two nodes, their level and their index.

Equations

• One or more equations did not get rendered due to their size.

Occurrences and nodes

noncomputable def DescriptiveComplexity.SatCover.satOccF {α : Type} (x : α) : SatOcc.satOrd.Formula α

x is a variable of the formula, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.occDomF {α : Type} (d s : Bool) (c x : α) : SatOcc.satOrd.Formula α

(c, x) is an occurrence of tag (d, s): the dummy occurrence (x, x) of a variable x when d, the occurrence of (x, s) in the clause c otherwise.

Equations

• DescriptiveComplexity.SatCover.occDomF d s c x = if d = true then DescriptiveComplexity.SatOcc.eqF c x ⊓ DescriptiveComplexity.SatCover.satOccF x else DescriptiveComplexity.SatOcc.occF s c x

noncomputable def DescriptiveComplexity.SatCover.nodeDomF {α : Type} (t : NodeTag) (c x : α) : SatOcc.satOrd.Formula α

(c, x) is a node of the base graph of tag t.

Equations

• DescriptiveComplexity.SatCover.nodeDomF (Sum.inl (d, s)) c x = DescriptiveComplexity.SatCover.occDomF d s c x
• DescriptiveComplexity.SatCover.nodeDomF (Sum.inr (Sum.inl (d, s))) c x = DescriptiveComplexity.SatCover.occDomF d s c x
• DescriptiveComplexity.SatCover.nodeDomF (Sum.inr (Sum.inr true)) c x = DescriptiveComplexity.SatOcc.clF c ⊓ DescriptiveComplexity.SatOcc.eqF x c
• DescriptiveComplexity.SatCover.nodeDomF (Sum.inr (Sum.inr false)) c x = DescriptiveComplexity.SatCover.satOccF c ⊓ DescriptiveComplexity.SatOcc.eqF x c

noncomputable def DescriptiveComplexity.SatCover.vDomF {α : Type} (t : VTag) (c x : α) : SatOcc.satOrd.Formula α

(c, x) is a node of the attached graph of tag t.

Equations

• DescriptiveComplexity.SatCover.vDomF (Sum.inl t_2) c x = DescriptiveComplexity.SatCover.nodeDomF t_2 c x
• DescriptiveComplexity.SatCover.vDomF (Sum.inr ((d, s), snd)) c x = DescriptiveComplexity.SatCover.occDomF d s c x

noncomputable def DescriptiveComplexity.SatCover.isMinF {α : Type} (c : α) : SatOcc.satOrd.Formula α

c is the least element, as a formula.

Equations

• DescriptiveComplexity.SatCover.isMinF c = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.leF (Sum.inl c) (Sum.inr 0))

noncomputable def DescriptiveComplexity.SatCover.levelDomF {α : Type} (t : LevelTag) (c x : α) : SatOcc.satOrd.Formula α

(c, x) is a level of tag t: an occurrence, or the pair of least elements.

Equations

• DescriptiveComplexity.SatCover.levelDomF none c x = DescriptiveComplexity.SatCover.isMinF c ⊓ DescriptiveComplexity.SatOcc.eqF x c
• DescriptiveComplexity.SatCover.levelDomF (some ((d, s), snd)) c x = DescriptiveComplexity.SatCover.occDomF d s c x

The base edges and the entries of the attached matrix

noncomputable def DescriptiveComplexity.SatCover.nextF {α : Type} (d d' s : Bool) (c x c' : α) : SatOcc.satOrd.Formula α

(c', x) is the occurrence of the literal (x, s) next after (c, x), cyclically, the dummy occurrence first: the four cases according to whether each is the dummy one.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.baseEdgeF {α : Type} (t t' : NodeTag) (c x c' x' : α) : SatOcc.satOrd.Formula α

The base edge from the node (c, x) of tag t to the node (c', x') of tag t'.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatCover.baseEdgeF t t' c x c' x' = ⊥

noncomputable def DescriptiveComplexity.SatCover.flatEntryF {α : Type} (v : ℤ) (t t' : VTag) (c x c' x' : α) : SatOcc.satOrd.Formula α

The entry of the attached matrix between the node (c, x) of tag t and the node (c', x') of tag t' is v, for v ≠ 0.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SatCover.flatEntryF v (Sum.inl t_2) (Sum.inl t'_2) c x c' x' = if v = 1 then DescriptiveComplexity.SatCover.baseEdgeF t_2 t'_2 c x c' x' else ⊥

The order of the levels

noncomputable def DescriptiveComplexity.SatCover.levelLeF {α : Type} (t t' : LevelTag) (c x c' x' : α) : SatOcc.satOrd.Formula α

The level (c, x) of tag t is at most the level (c', x') of tag t', in the lexicographic order: the tags are compared statically.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.levelLtF {α : Type} (t t' : LevelTag) (c x c' x' : α) : SatOcc.satOrd.Formula α

Strictly below, among the levels.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.levelMinF {α : Type} (t : LevelTag) (c x : α) : SatOcc.satOrd.Formula α

The level (c, x) of tag t is the least level.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.levelMaxF {α : Type} (t : LevelTag) (c x : α) : SatOcc.satOrd.Formula α

The level (c, x) of tag t is the greatest level.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SatCover.levelCovF {α : Type} (t t' : LevelTag) (c x c' x' : α) : SatOcc.satOrd.Formula α

The level (c', x') of tag t' is the one next after the level (c, x) of tag t.

Equations

• One or more equations did not get rendered due to their size.

The widths

noncomputable def DescriptiveComplexity.SatCover.widthF {α : Type} (t t' : VTag) (l : LevelTag) (j : Fin 3) (c x c' x' c'' x'' : α) : SatOcc.satOrd.Formula α

The index j is below the width, at the level (c'', x'') of tag l, of the ladder from the node (c, x) of tag t to the node (c', x') of tag t': two rungs at every level for an entry -1, the entry at the least level and one rung elsewhere otherwise.

Equations

• One or more equations did not get rendered due to their size.

Semantics of the tags

def DescriptiveComplexity.SatCover.OccDom {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) : Prop

The pair (c, x) is an occurrence of tag (d, s).

Equations

• DescriptiveComplexity.SatCover.OccDom d s c x = if d = true then c = x ∧ DescriptiveComplexity.SatOccurs A x else DescriptiveComplexity.SatOcc.OccIn c x s

def DescriptiveComplexity.SatCover.occC {A : Type} (d : Bool) (c : A) : WithBot A

The clause of an occurrence of tag d: ⊥ for the dummy one.

Equations

• DescriptiveComplexity.SatCover.occC d c = if d = true then ⊥ else ↑c

def DescriptiveComplexity.SatCover.occOf {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : Occ A

The occurrence a tagged pair denotes.

Equations

• DescriptiveComplexity.SatCover.occOf d s c x h = ⟨(DescriptiveComplexity.SatCover.occC d c, x, s), ⋯⟩

@[simp]

theorem DescriptiveComplexity.SatCover.occOf_c {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : (occOf d s c x h).c = occC d c

@[simp]

theorem DescriptiveComplexity.SatCover.occOf_x {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : (occOf d s c x h).x = x

@[simp]

theorem DescriptiveComplexity.SatCover.occOf_s {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : (occOf d s c x h).s = s

def DescriptiveComplexity.SatCover.occTag {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : OccTag

The tag of an occurrence.

Equations

• DescriptiveComplexity.SatCover.occTag o = (WithBot.recBotCoe true (fun (x : A) => false) o.c, o.s)

def DescriptiveComplexity.SatCover.occPair {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : A × A

The pair an occurrence is drawn as: (x, x) for a dummy one.

Equations

• DescriptiveComplexity.SatCover.occPair o = (WithBot.unbotD o.x o.c, o.x)

theorem DescriptiveComplexity.SatCover.occDom_occTag {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : OccDom (occTag o).1 (occTag o).2 (occPair o).1 (occPair o).2

theorem DescriptiveComplexity.SatCover.occOf_occTag {A : Type} [FirstOrder.Language.sat.Structure A] (o : Occ A) : occOf (occTag o).1 (occTag o).2 (occPair o).1 (occPair o).2 ⋯ = o

theorem DescriptiveComplexity.SatCover.occTag_occOf {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : occTag (occOf d s c x h) = (d, s)

theorem DescriptiveComplexity.SatCover.occPair_occOf {A : Type} [FirstOrder.Language.sat.Structure A] (d s : Bool) (c x : A) (h : OccDom d s c x) : occPair (occOf d s c x h) = (c, x)

def DescriptiveComplexity.SatCover.NodeDom {A : Type} [FirstOrder.Language.sat.Structure A] (t : NodeTag) (c x : A) : Prop

The pair (c, x) is a node of the base graph of tag t.

Equations

• DescriptiveComplexity.SatCover.NodeDom (Sum.inl (d, s)) c x = DescriptiveComplexity.SatCover.OccDom d s c x
• DescriptiveComplexity.SatCover.NodeDom (Sum.inr (Sum.inl (d, s))) c x = DescriptiveComplexity.SatCover.OccDom d s c x
• DescriptiveComplexity.SatCover.NodeDom (Sum.inr (Sum.inr true)) c x = (DescriptiveComplexity.SatOcc.IsCl c ∧ x = c)
• DescriptiveComplexity.SatCover.NodeDom (Sum.inr (Sum.inr false)) c x = (DescriptiveComplexity.SatOccurs A c ∧ x = c)

def DescriptiveComplexity.SatCover.nodeOf {A : Type} [FirstOrder.Language.sat.Structure A] (t : NodeTag) (c x : A) (h : NodeDom t c x) : Node A

The node a tagged pair denotes.

Equations

• DescriptiveComplexity.SatCover.nodeOf (Sum.inl (d, s)) c x h_2 = DescriptiveComplexity.SatCover.trk (DescriptiveComplexity.SatCover.occOf d s c x h_2)
• DescriptiveComplexity.SatCover.nodeOf (Sum.inr (Sum.inl (d, s))) c x h_2 = DescriptiveComplexity.SatCover.spk (DescriptiveComplexity.SatCover.occOf d s c x h_2)
• DescriptiveComplexity.SatCover.nodeOf (Sum.inr (Sum.inr true)) c x h_2 = DescriptiveComplexity.SatCover.hub (Sum.inl ⟨c, ⋯⟩)
• DescriptiveComplexity.SatCover.nodeOf (Sum.inr (Sum.inr false)) c x h_2 = DescriptiveComplexity.SatCover.hub (Sum.inr ⟨c, ⋯⟩)

def DescriptiveComplexity.SatCover.nodeTag {A : Type} [FirstOrder.Language.sat.Structure A] (n : Node A) : NodeTag

The tag of a node.

Equations

• DescriptiveComplexity.SatCover.nodeTag (Sum.inl o) = Sum.inl (DescriptiveComplexity.SatCover.occTag o)
• DescriptiveComplexity.SatCover.nodeTag (Sum.inr (Sum.inl o)) = Sum.inr (Sum.inl (DescriptiveComplexity.SatCover.occTag o))
• DescriptiveComplexity.SatCover.nodeTag (Sum.inr (Sum.inr (Sum.inl val))) = Sum.inr (Sum.inr true)
• DescriptiveComplexity.SatCover.nodeTag (Sum.inr (Sum.inr (Sum.inr val))) = Sum.inr (Sum.inr false)

def DescriptiveComplexity.SatCover.nodePair {A : Type} [FirstOrder.Language.sat.Structure A] (n : Node A) : A × A

The pair a node is drawn as.

Equations

• DescriptiveComplexity.SatCover.nodePair (Sum.inl o) = DescriptiveComplexity.SatCover.occPair o
• DescriptiveComplexity.SatCover.nodePair (Sum.inr (Sum.inl o)) = DescriptiveComplexity.SatCover.occPair o
• DescriptiveComplexity.SatCover.nodePair (Sum.inr (Sum.inr (Sum.inl val))) = (↑val, ↑val)
• DescriptiveComplexity.SatCover.nodePair (Sum.inr (Sum.inr (Sum.inr val))) = (↑val, ↑val)

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.V (A : Type) [FirstOrder.Language.sat.Structure A] : Type

The nodes of the attached graph.

Equations

• DescriptiveComplexity.SatCover.V A = (DescriptiveComplexity.SatCover.Node A ⊕ DescriptiveComplexity.SatCover.Occ A × Fin 4)

def DescriptiveComplexity.SatCover.VDom {A : Type} [FirstOrder.Language.sat.Structure A] (t : VTag) (c x : A) : Prop

The pair (c, x) is a node of the attached graph of tag t.

Equations

• DescriptiveComplexity.SatCover.VDom (Sum.inl t_2) c x = DescriptiveComplexity.SatCover.NodeDom t_2 c x
• DescriptiveComplexity.SatCover.VDom (Sum.inr ((d, s), snd)) c x = DescriptiveComplexity.SatCover.OccDom d s c x

def DescriptiveComplexity.SatCover.vOf {A : Type} [FirstOrder.Language.sat.Structure A] (t : VTag) (c x : A) (h : VDom t c x) : V A

The node of the attached graph a tagged pair denotes.

Equations

• DescriptiveComplexity.SatCover.vOf (Sum.inl t_2) c x h_2 = Sum.inl (DescriptiveComplexity.SatCover.nodeOf t_2 c x h_2)
• DescriptiveComplexity.SatCover.vOf (Sum.inr ((d, s), j)) c x h_2 = Sum.inr (DescriptiveComplexity.SatCover.occOf d s c x h_2, j)

def DescriptiveComplexity.SatCover.vTag {A : Type} [FirstOrder.Language.sat.Structure A] (n : V A) : VTag

The tag of a node of the attached graph.

Equations

• DescriptiveComplexity.SatCover.vTag (Sum.inl n_2) = Sum.inl (DescriptiveComplexity.SatCover.nodeTag n_2)
• DescriptiveComplexity.SatCover.vTag (Sum.inr (o, j)) = Sum.inr (DescriptiveComplexity.SatCover.occTag o, j)

def DescriptiveComplexity.SatCover.vPair {A : Type} [FirstOrder.Language.sat.Structure A] (n : V A) : A × A

The pair a node of the attached graph is drawn as.

Equations

• DescriptiveComplexity.SatCover.vPair (Sum.inl n_2) = DescriptiveComplexity.SatCover.nodePair n_2
• DescriptiveComplexity.SatCover.vPair (Sum.inr (o, j)) = DescriptiveComplexity.SatCover.occPair o

theorem DescriptiveComplexity.SatCover.vDom_vTag {A : Type} [FirstOrder.Language.sat.Structure A] (n : V A) : VDom (vTag n) (vPair n).1 (vPair n).2

theorem DescriptiveComplexity.SatCover.vOf_vTag {A : Type} [FirstOrder.Language.sat.Structure A] (n : V A) : vOf (vTag n) (vPair n).1 (vPair n).2 ⋯ = n

theorem DescriptiveComplexity.SatCover.vTag_vOf {A : Type} [FirstOrder.Language.sat.Structure A] (t : VTag) (c x : A) (h : VDom t c x) : vTag (vOf t c x h) = t

theorem DescriptiveComplexity.SatCover.vPair_vOf {A : Type} [FirstOrder.Language.sat.Structure A] (t : VTag) (c x : A) (h : VDom t c x) : vPair (vOf t c x h) = (c, x)

def DescriptiveComplexity.SatCover.LevelDom {A : Type} [FirstOrder.Language.sat.Structure A] [LE A] (t : LevelTag) (c x : A) : Prop

The pair (c, x) is a level of tag t.

Equations

• DescriptiveComplexity.SatCover.LevelDom none c x = ((∀ (y : A), c ≤ y) ∧ x = c)
• DescriptiveComplexity.SatCover.LevelDom (some ((d, s), snd)) c x = DescriptiveComplexity.SatCover.OccDom d s c x

Realization

theorem DescriptiveComplexity.SatCover.realize_occDomF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {d s : Bool} {c x : α} : (occDomF d s c x).Realize v ↔ OccDom d s (v c) (v x)

theorem DescriptiveComplexity.SatCover.realize_levelDomF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {t : LevelTag} {c x : α} : (levelDomF t c x).Realize v ↔ LevelDom t (v c) (v x)

The next occurrence

The base edges

def DescriptiveComplexity.SatCover.nodeKind {A : Type} [FirstOrder.Language.sat.Structure A] (n : Node A) : Fin 3

The kind of a node: track node, spoke or hub.

Equations

• DescriptiveComplexity.SatCover.nodeKind (Sum.inl val) = 0
• DescriptiveComplexity.SatCover.nodeKind (Sum.inr (Sum.inl val)) = 1
• DescriptiveComplexity.SatCover.nodeKind (Sum.inr (Sum.inr val)) = 2

def DescriptiveComplexity.SatCover.tagKind (t : NodeTag) : Fin 3

The kind of a node tag.

Equations

• DescriptiveComplexity.SatCover.tagKind (Sum.inl val) = 0
• DescriptiveComplexity.SatCover.tagKind (Sum.inr (Sum.inl val)) = 1
• DescriptiveComplexity.SatCover.tagKind (Sum.inr (Sum.inr val)) = 2

theorem DescriptiveComplexity.SatCover.nodeKind_nodeOf {A : Type} [FirstOrder.Language.sat.Structure A] (t : NodeTag) (c x : A) (h : NodeDom t c x) : nodeKind (nodeOf t c x h) = tagKind t

The entries of the attached matrix

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.SatCover.attachedM {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] : V A → V A → ℤ

The attached matrix: the base matrix with Valiant's gadget attached at every site, on the flat node type.

Equations

• DescriptiveComplexity.SatCover.attachedM = DescriptiveComplexity.Site.flatAttach DescriptiveComplexity.SatCover.baseM DescriptiveComplexity.SatCover.site

theorem DescriptiveComplexity.SatCover.attachedM_bounds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Fintype A] (a b : V A) : -1 ≤ attachedM a b ∧ attachedM a b ≤ 3

The entries of the attached matrix are between -1 and 3.

theorem DescriptiveComplexity.SatCover.realize_ite_bot {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {β : Type} {w : β → A} (p : Prop) [Decidable p] (φ : SatOcc.satOrd.Formula β) : (if p then φ else ⊥).Realize w ↔ p ∧ φ.Realize w

theorem DescriptiveComplexity.SatCover.ite_one_eq_iff {k : ℤ} (_hk : k ≠ 0) (P : Prop) [Decidable P] : (if P then 1 else 0) = k ↔ k = 1 ∧ P

theorem DescriptiveComplexity.SatCover.ite_add_ite_eq_iff {k : ℤ} (_hk : k ≠ 0) (P Q : Prop) [Decidable P] [Decidable Q] (hPQ : ¬(P ∧ Q)) : ((if P then 1 else 0) + if Q then 1 else 0) = k ↔ k = 1 ∧ (P ∨ Q)

theorem DescriptiveComplexity.SatCover.ite_eq_iff_of_ne {k z : ℤ} (_hk : k ≠ 0) (P : Prop) [Decidable P] : (if P then z else 0) = k ↔ P ∧ z = k

The levels

noncomputable def DescriptiveComplexity.SatCover.levelsInterp : RelFOInterpretation SatOcc.satOrd FirstOrder.Language.empty LevelTag 2

The levels of the ladders, as a relativized interpretation into the empty vocabulary: the number of levels is then a definable cardinality.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.SatCover.Level (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Type

The levels: the universe of the interpretation of the levels, ordered lexicographically.

Equations

• DescriptiveComplexity.SatCover.Level A = DescriptiveComplexity.SatCover.levelsInterp.MapRel A

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instLinearOrderLevel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : LinearOrder (Level A)

Equations

• DescriptiveComplexity.SatCover.instLinearOrderLevel = DescriptiveComplexity.SatCover.levelsInterp.mapRelLinearOrder A

instance DescriptiveComplexity.SatCover.instFiniteLevel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : Finite (Level A)

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instFintypeLevelOfFinite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : Fintype (Level A)

Equations

• DescriptiveComplexity.SatCover.instFintypeLevelOfFinite = Fintype.ofFinite (DescriptiveComplexity.SatCover.Level A)

theorem DescriptiveComplexity.SatCover.levelDom_of {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ℓ : Level A) : LevelDom (↑ℓ).1 ((↑ℓ).2 0) ((↑ℓ).2 1)

def DescriptiveComplexity.SatCover.mkLevel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : LevelTag) (c x : A) (h : LevelDom t c x) : Level A

A level, from its tag and its pair.

Equations

• DescriptiveComplexity.SatCover.mkLevel t c x h = ⟨(t, ![c, x]), ⋯⟩

theorem DescriptiveComplexity.SatCover.mkLevel_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ℓ : Level A) : mkLevel (↑ℓ).1 ((↑ℓ).2 0) ((↑ℓ).2 1) ⋯ = ℓ

instance DescriptiveComplexity.SatCover.instNonemptyLevelOfFinite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty (Level A)

@[instance_reducible]

noncomputable instance DescriptiveComplexity.SatCover.instBoundedOrderLevelOfFiniteOfNonempty {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : BoundedOrder (Level A)

Equations

• DescriptiveComplexity.SatCover.instBoundedOrderLevelOfFiniteOfNonempty = Fintype.toBoundedOrder (DescriptiveComplexity.SatCover.Level A)

theorem DescriptiveComplexity.SatCover.tupLeLex_two {A : Type} [LinearOrder A] (c x c' x' : A) : tupLeLex ![c, x] ![c', x'] ↔ c < c' ∨ c = c' ∧ x ≤ x'

Realization of the level formulas and of the widths

theorem DescriptiveComplexity.SatCover.realize_levelCovF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {t t' : LevelTag} {c x c' x' : α} (h : LevelDom t (v c) (v x)) (h' : LevelDom t' (v c') (v x')) : (levelCovF t t' c x c' x').Realize v ↔ mkLevel t (v c) (v x) h ⋖ mkLevel t' (v c') (v x') h'