Reading the encoded sentence off the image

DescriptiveComplexity.FinSat.Interp builds the sentence σ_A and proves it well formed (DescriptiveComplexity.FinSat.image_isWF); this file reads it back as a sentence – what its nodes are, and which of them are children, binders and literals of which – which is what the correctness of the reduction is then stated and proved against.

The elements are points

Every relation of the image but the order demands canonically padded tuples (DescriptiveComplexity.FinSat.canonG), and a canonical tuple is the padding of its own prefix (DescriptiveComplexity.pad_pref_of_canon). So the elements the sentence actually reads are exactly the DescriptiveComplexity.FinSat.ptOf a₀ t w: a tag together with a tuple of the tag's own length, padded with the least element. Elements that are not of that form are junk – variables of the encoded sentence that no node binds and no literal reads – and DescriptiveComplexity.FinSat.eq_ptOf says they are the only ones, so every case analysis may assume a point.

This is the idiom the library uses wherever tagged tuples are compared: a def for the element, an iff lemma for each relation it takes part in, and an inversion lemma putting an arbitrary element in that form. Matching on a pair literal at the type FOInterpretation.Map is ill-typed at the transparency rw and simp work at, so the named constructor is not a convenience but a requirement.

The points of the image

def DescriptiveComplexity.FinSat.ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (finsatInterp B φ).Map A

An element of the encoded sentence: a tag, and a tuple of the tag's own length padded with the least element a₀.

Equations

• DescriptiveComplexity.FinSat.ptOf B φ a₀ t w = (t, DescriptiveComplexity.pad a₀ w)

@[simp]

theorem DescriptiveComplexity.FinSat.ptOf_fst {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).1 = t

@[simp]

theorem DescriptiveComplexity.FinSat.ptOf_snd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).2 = pad a₀ w

theorem DescriptiveComplexity.FinSat.canon_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : Canon (tagDim B φ (ptOf B φ a₀ t w).1) (ptOf B φ a₀ t w).2

theorem DescriptiveComplexity.FinSat.eq_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : (finsatInterp B φ).Map A} (h : Canon (tagDim B φ x.1) x.2) : x = ptOf B φ a₀ x.1 (pref ⋯ x.2)

Junk is the only thing that is not a point: an element whose tuple is canonically padded for its tag is the point of its own prefix.

theorem DescriptiveComplexity.FinSat.ptOf_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {t : FTag B φ} {w w' : Fin (tagDim B φ t) → A} (h : ptOf B φ a₀ t w = ptOf B φ a₀ t w') : w = w'

theorem DescriptiveComplexity.FinSat.ptOf_c0 {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {t : FTag B φ} (hd : 0 < tagDim B φ t) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).2 (c0 B φ) = w ⟨0, hd⟩

The first coordinate of a point, which is where a tag of dimension one – the prefix, its variable, a literal of a translated atom – holds its element.

theorem DescriptiveComplexity.FinSat.ptOf_c1 {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {t : FTag B φ} (hd : 1 < tagDim B φ t) (w : Fin (tagDim B φ t) → A) : (ptOf B φ a₀ t w).2 (c1 B φ) = w ⟨1, hd⟩

The second coordinate of a point: where a distinctness literal of the diagram holds the second of its two elements.

The kinds of a node, at a point

The four kinds are decided by the tag alone (DescriptiveComplexity.FinSat.andTag and its companions), so at a point they are read off the tag and nothing else.

theorem DescriptiveComplexity.FinSat.andG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : AndG (ptOf B φ a₀ t w) ↔ andTag B φ t

theorem DescriptiveComplexity.FinSat.orG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : OrG (ptOf B φ a₀ t w) ↔ orTag B φ t

theorem DescriptiveComplexity.FinSat.allG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : AllG (ptOf B φ a₀ t w) ↔ allTag B φ t

theorem DescriptiveComplexity.FinSat.exG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : ExG (ptOf B φ a₀ t w) ↔ exTag B φ t

The nodes of the encoded sentence, by name

One definition per tag, so that a statement about the sentence never mentions a tuple that has to be reduced to be typed. Each is a DescriptiveComplexity.FinSat.ptOf, definitionally, which is how the lemmas below are proved: the work is done at ptOf – where the tags are literal constructors, so simp can reduce the body of a defining formula – and transported to the named node by exact, which unfolds at the transparency the matching tactics do not.

def DescriptiveComplexity.FinSat.bodyPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) : (finsatInterp B φ).Map A

The top conjunction of the sentence: the diagram and the translated kernel.

Equations

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

def DescriptiveComplexity.FinSat.prePt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ a : A) : (finsatInterp B φ).Map A

The existential of the prefix binding the variable of a.

Equations

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

def DescriptiveComplexity.FinSat.pvarPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ a : A) : (finsatInterp B φ).Map A

The variable that existential binds.

Equations

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

def DescriptiveComplexity.FinSat.neqPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ a b : A) : (finsatInterp B φ).Map A

The distinctness literal x_a ≠ x_b of the diagram.

Equations

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

def DescriptiveComplexity.FinSat.dbvarPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (l : Fin (Tseitin.maxCtx φ)) : (finsatInterp B φ).Map A

The variable naming a de Bruijn level of the kernel.

Equations

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

def DescriptiveComplexity.FinSat.symPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (i : B.ι) : (finsatInterp B φ).Map A

The relation symbol of a relation variable of the block.

Equations

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

def DescriptiveComplexity.FinSat.aposPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (j : Fin (finsatDim B φ)) : (finsatInterp B φ).Map A

An argument position of the relation symbols.

Equations

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

def DescriptiveComplexity.FinSat.ndPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (p : Pos B φ) (pol : Bool) : (finsatInterp B φ).Map A

The translation of the subformula at a position, at a polarity.

Equations

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

def DescriptiveComplexity.FinSat.atupPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) : (finsatInterp B φ).Map A

One tuple of the translation of an atom the sentence may not mention.

Equations

• DescriptiveComplexity.FinSat.atupPt B φ a₀ p pol w = DescriptiveComplexity.FinSat.ptOf B φ a₀ (DescriptiveComplexity.FinSat.Tag.atup p pol) w

def DescriptiveComplexity.FinSat.alitPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (a₀ : A) (p : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (a : A) : (finsatInterp B φ).Map A

One equality literal inside such a tuple.

Equations

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

The relations that read the tuples

child, bind and the two equality literals are not decided by the tags alone: their bodies compare the elements the tuples hold. Each is bridged to its named body (DescriptiveComplexity.FinSat.childBodyF and its companions) read at the valuation the interpretation supplies, and then computed at the tags it is defined for.

The bridge is stated at points, not at two arbitrary elements projected with .1: a projection out of FOInterpretation.Map is ill-typed at the transparency simp matches at, so childBodyF B φ g.1 c.1 would never reduce even with both tags known. At a point the tag is syntactically there.

def DescriptiveComplexity.FinSat.val₁ {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (x : (finsatInterp B φ).Map A) : Fin 1 × Fin (finsatDim B φ) → A

The valuation a unary defining formula of the image is read at.

Equations

• DescriptiveComplexity.FinSat.val₁ B φ x q = (![x] q.1).2 q.2

def DescriptiveComplexity.FinSat.val₂ {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (x y : (finsatInterp B φ).Map A) : Fin 2 × Fin (finsatDim B φ) → A

The valuation a binary defining formula of the image is read at.

Equations

• DescriptiveComplexity.FinSat.val₂ B φ x y q = (![x, y] q.1).2 q.2

def DescriptiveComplexity.FinSat.val₃ {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (x y z : (finsatInterp B φ).Map A) : Fin 3 × Fin (finsatDim B φ) → A

The valuation a ternary defining formula of the image is read at.

Equations

• DescriptiveComplexity.FinSat.val₃ B φ x y z q = (![x, y, z] q.1).2 q.2

theorem DescriptiveComplexity.FinSat.childG_ptOf_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : ChildG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') ↔ (childBodyF B φ t t').Realize (val₂ B φ (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w'))

The child relation at a pair of points: canonicity is automatic, so only the body is left.

The child relation, node by node

theorem DescriptiveComplexity.FinSat.childG_pre_pre {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a b : A) : ChildG (prePt B φ a₀ a) (prePt B φ a₀ b) ↔ a < b ∧ ∀ (x : A), ¬(a < x ∧ x < b)

The existential prefix is a chain: the node of a has the node of the next element of the input order as its child.

theorem DescriptiveComplexity.FinSat.childG_pre_body {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a : A) : ChildG (prePt B φ a₀ a) (bodyPt B φ a₀) ↔ ∀ (x : A), x ≤ a

The last node of the prefix hands over the top conjunction: the node of the greatest element of the input order.

theorem DescriptiveComplexity.FinSat.childG_body_neq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a b : A) : ChildG (bodyPt B φ a₀) (neqPt B φ a₀ a b) ↔ a ≠ b

The top conjunction takes the distinctness literals of the diagram – and only those of distinct pairs: the literal of (a, a) says x_a ≠ x_a, which no environment satisfies, so it must not be a conjunct.

theorem DescriptiveComplexity.FinSat.childG_body_nd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) : ChildG (bodyPt B φ a₀) (ndPt B φ a₀ p pol) ↔ pol = true ∧ p = rootPos B φ

The top conjunction takes the root of the translated kernel, and nothing else of the kernel.

theorem DescriptiveComplexity.FinSat.childG_nd_nd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p q : Pos B φ) (pol pol' : Bool) : ChildG (ndPt B φ a₀ p pol) (ndPt B φ a₀ q pol') ↔ kidOf φ p.snd q.snd = some (pol ^^ pol')

Inside the translated kernel the child relation follows DescriptiveComplexity.FinSat.kidOf, the polarity flipping exactly at the premise of an implication.

theorem DescriptiveComplexity.FinSat.childG_nd_atup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) : ChildG (ndPt B φ a₀ p pol) (atupPt B φ a₀ p pol w) ↔ (inAtomF B φ p).Realize (val₂ B φ (ptOf B φ a₀ (Tag.nd p pol) fun (x : Fin (tagDim B φ (Tag.nd p pol))) => a₀) (ptOf B φ a₀ (Tag.atup p pol) w))

A translated atom takes the tuple nodes where it holds: the one place the reduction reads the input structure, and the reason the encoded sentence never mentions a symbol of the input vocabulary.

theorem DescriptiveComplexity.FinSat.childG_atup_alit {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) (j : Fin (finsatDim B φ)) (a : A) : ChildG (atupPt B φ a₀ p pol w) (alitPt B φ a₀ p pol j a) ↔ ↑j < inArity B φ p ∧ pad a₀ w j = a

Each tuple node takes one equality literal per argument position, binding that argument to the variable of the corresponding element.

The binders, the literals and the root

theorem DescriptiveComplexity.FinSat.bindG_ptOf_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : BindG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') ↔ (bindBodyF B φ t t').Realize (val₂ B φ (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w'))

theorem DescriptiveComplexity.FinSat.bindG_pre_pvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a b : A) : BindG (prePt B φ a₀ a) (pvarPt B φ a₀ b) ↔ a = b

Each node of the prefix binds its own variable.

theorem DescriptiveComplexity.FinSat.bindG_nd_dbvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (l : Fin (Tseitin.maxCtx φ)) : BindG (ndPt B φ a₀ p pol) (dbvarPt B φ a₀ l) ↔ qLevel B φ p = some ↑l

A quantifier of the kernel binds the variable of the de Bruijn level it introduces.

theorem DescriptiveComplexity.FinSat.neqG_ptOf_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' t'' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) (w'' : Fin (tagDim B φ t'') → A) : NeqG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w'') ↔ (neqBodyF B φ t t' t'').Realize (val₃ B φ (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w''))

theorem DescriptiveComplexity.FinSat.neqG_neq_pvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a b x y : A) : NeqG (neqPt B φ a₀ a b) (pvarPt B φ a₀ x) (pvarPt B φ a₀ y) ↔ a = x ∧ b = y ∧ a ≠ b

The diagram: the literal of the pair (a, b) says that the variables of a and of b are distinct, and it exists only for a ≠ b.

theorem DescriptiveComplexity.FinSat.rootG_ptOf_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) : RootG (ptOf B φ a₀ t w) ↔ (rootBodyF B φ t).Realize (val₁ B φ (ptOf B φ a₀ t w))

theorem DescriptiveComplexity.FinSat.rootG_pre {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a : A) : RootG (prePt B φ a₀ a) ↔ ∀ (x : A), a ≤ x

The root of the encoded sentence is the node of the prefix binding the least element of the input order: the outermost existential.

Inversion: these are the only children

The truth definition quantifies over all the children of a node, so reading σ_A needs the converse of the lemmas above: which elements of the image are children of a given node, and no others. Everything rests on canonicity – a relation of the image holds only of canonically padded tuples, and those are the points – so an arbitrary element can always be replaced by a point, after which the tag alone decides.

theorem DescriptiveComplexity.FinSat.exists_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : (finsatInterp B φ).Map A} (h : Canon (tagDim B φ x.1) x.2) : ∃ (t : FTag B φ) (w : Fin (tagDim B φ t) → A), x = ptOf B φ a₀ t w

Every canonically padded element is a point.

theorem DescriptiveComplexity.FinSat.canon_of_childG_right {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {g c : (finsatInterp B φ).Map A} (h : ChildG g c) : Canon (tagDim B φ c.1) c.2

theorem DescriptiveComplexity.FinSat.canon_of_bindG_right {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {g x : (finsatInterp B φ).Map A} (h : BindG g x) : Canon (tagDim B φ x.1) x.2

theorem DescriptiveComplexity.FinSat.childG_iff_pt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) (c : (finsatInterp B φ).Map A) : ChildG (ptOf B φ a₀ t w) c ↔ ∃ (t' : FTag B φ) (w' : Fin (tagDim B φ t') → A), c = ptOf B φ a₀ t' w' ∧ ChildG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w')

A child is a point: the child relation of the image never leaves the elements the sentence reads.

theorem DescriptiveComplexity.FinSat.not_childG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (hb : childBodyF B φ t t' = ⊥) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : ¬ChildG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w')

A tag pair the child relation is not defined at has no edge.

The tuples of the tags of dimension zero, one and two, read out: what the inversion lemmas put an arbitrary tuple back into.

theorem DescriptiveComplexity.FinSat.tup_zero_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 0) (w w' : Fin (tagDim B φ t) → A) : w = w'

theorem DescriptiveComplexity.FinSat.tup_one_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 1) (w : Fin (tagDim B φ t) → A) (h0 : 0 < tagDim B φ t) : w = fun (x : Fin (tagDim B φ t)) => w ⟨0, h0⟩

theorem DescriptiveComplexity.FinSat.tup_two_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {t : FTag B φ} (h : tagDim B φ t = 2) (w : Fin (tagDim B φ t) → A) (h0 : 0 < tagDim B φ t) (h1 : 1 < tagDim B φ t) : w = fun (j : Fin (tagDim B φ t)) => if ↑j = 0 then w ⟨0, h0⟩ else w ⟨1, h1⟩

theorem DescriptiveComplexity.FinSat.childG_body_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (c : (finsatInterp B φ).Map A) : ChildG (bodyPt B φ a₀) c ↔ (∃ (a : A) (b : A), a ≠ b ∧ c = neqPt B φ a₀ a b) ∨ c = ndPt B φ a₀ (rootPos B φ) true

The children of the top conjunction: every distinctness literal of the diagram, and the root of the translated kernel at polarity true.

theorem DescriptiveComplexity.FinSat.childG_pre_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (a : A) (c : (finsatInterp B φ).Map A) : ChildG (prePt B φ a₀ a) c ↔ (∃ (b : A), c = prePt B φ a₀ b ∧ a < b ∧ ∀ (x : A), ¬(a < x ∧ x < b)) ∨ c = bodyPt B φ a₀ ∧ ∀ (x : A), x ≤ a

The children of a node of the existential prefix: the node of the next element of the input order, and – at the greatest element – the top conjunction.

The literals and the atoms, node by node

The remaining clauses of the truth definition: the equality literals of the kernel and of the translated atoms, and the atoms of the relation variables – the only genuine atoms of the encoded sentence – with their symbols, their argument positions and their signature. All but the literals of a translated atom are decided by the tags.

theorem DescriptiveComplexity.FinSat.eqG_ptOf_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' t'' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) (w'' : Fin (tagDim B φ t'') → A) : EqG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w'') ↔ (eqBodyF B φ t t' t'').Realize (val₃ B φ (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w''))

theorem DescriptiveComplexity.FinSat.eqG_nd_dbvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (l₁ l₂ : Fin (Tseitin.maxCtx φ)) : EqG (ndPt B φ a₀ p pol) (dbvarPt B φ a₀ l₁) (dbvarPt B φ a₀ l₂) ↔ pol = true ∧ eqArgs B φ p = some (↑l₁, ↑l₂)

A positive equality of the kernel, between the variables of two de Bruijn levels.

theorem DescriptiveComplexity.FinSat.neqG_nd_dbvar {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (l₁ l₂ : Fin (Tseitin.maxCtx φ)) : NeqG (ndPt B φ a₀ p pol) (dbvarPt B φ a₀ l₁) (dbvarPt B φ a₀ l₂) ↔ pol = false ∧ eqArgs B φ p = some (↑l₁, ↑l₂)

A negated equality of the kernel.

theorem DescriptiveComplexity.FinSat.eqG_alit {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (a b : A) (l : Fin (Tseitin.maxCtx φ)) : EqG (alitPt B φ a₀ p pol j a) (dbvarPt B φ a₀ l) (pvarPt B φ a₀ b) ↔ (pol = true ∧ inArg B φ p ↑j = some ↑l) ∧ a = b

A literal of a translated atom: the argument of the atom at one position is the variable of the element that tuple holds there.

theorem DescriptiveComplexity.FinSat.neqG_alit {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (a b : A) (l : Fin (Tseitin.maxCtx φ)) : NeqG (alitPt B φ a₀ p pol j a) (dbvarPt B φ a₀ l) (pvarPt B φ a₀ b) ↔ (pol = false ∧ inArg B φ p ↑j = some ↑l) ∧ a = b

The same, negated: what a tuple of a negatively translated atom asks.

The atoms of the relation variables, which the encoded sentence does name: all four relations are decided by the tags.

theorem DescriptiveComplexity.FinSat.posG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : PosG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') ↔ atomTag B φ true t t'

theorem DescriptiveComplexity.FinSat.negG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : NegG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') ↔ atomTag B φ false t t'

theorem DescriptiveComplexity.FinSat.argG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' t'' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) (w'' : Fin (tagDim B φ t'') → A) : ArgG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w'') ↔ argTag B φ t t' t''

theorem DescriptiveComplexity.FinSat.sigG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : SigG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') ↔ sigTag B φ t t'

The children of the translated kernel

Inside the kernel a node takes the nodes of its children positions – the polarity flipping exactly at the premise of an implication – and, where the kernel carries an atom the sentence may not mention, the tuple nodes of that atom, each of which takes one equality literal per argument. A tuple node of another position is never a child, which is what makes the translation of two atoms independent.

theorem DescriptiveComplexity.FinSat.eq_of_childG_nd_atup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {p q : Pos B φ} {pol pol' : Bool} (w : Fin (tagDim B φ (Tag.atup q pol')) → A) (h : ChildG (ptOf B φ a₀ (Tag.nd p pol) fun (x : Fin (tagDim B φ (Tag.nd p pol))) => a₀) (ptOf B φ a₀ (Tag.atup q pol') w)) : p = q ∧ pol = pol'

A kernel node only takes tuple nodes of its own position and polarity.

theorem DescriptiveComplexity.FinSat.eq_of_childG_atup_alit {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {p q : Pos B φ} {pol pol' : Bool} {j : Fin (finsatDim B φ)} (w : Fin (tagDim B φ (Tag.atup p pol)) → A) (w' : Fin (tagDim B φ (Tag.alit q pol' j)) → A) (h : ChildG (ptOf B φ a₀ (Tag.atup p pol) w) (ptOf B φ a₀ (Tag.alit q pol' j) w')) : p = q ∧ pol = pol'

A tuple node only takes literals of its own position and polarity.

theorem DescriptiveComplexity.FinSat.childG_nd_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (c : (finsatInterp B φ).Map A) : ChildG (ndPt B φ a₀ p pol) c ↔ (∃ (q : Pos B φ) (pol' : Bool), kidOf φ p.snd q.snd = some (pol ^^ pol') ∧ c = ndPt B φ a₀ q pol') ∨ ∃ (w : Fin (tagDim B φ (Tag.atup p pol)) → A), ChildG (ndPt B φ a₀ p pol) (atupPt B φ a₀ p pol w) ∧ c = atupPt B φ a₀ p pol w

The children of a node of the translated kernel.

theorem DescriptiveComplexity.FinSat.childG_atup_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) (c : (finsatInterp B φ).Map A) : ChildG (atupPt B φ a₀ p pol w) c ↔ ∃ (j : Fin (finsatDim B φ)), ↑j < inArity B φ p ∧ c = alitPt B φ a₀ p pol j (pad a₀ w j)

The children of a tuple node: one equality literal per argument position, binding that argument to the variable of the element the tuple holds there.

The binders of a quantifier node

The quantifier clauses of the truth definition quantify over the variables a node binds, so they need the converse of DescriptiveComplexity.FinSat.bindG_nd_dbvar: a quantifier of the kernel binds the variable of the de Bruijn level it introduces, and nothing else.

theorem DescriptiveComplexity.FinSat.bindG_iff_pt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (w : Fin (tagDim B φ t) → A) (x : (finsatInterp B φ).Map A) : BindG (ptOf B φ a₀ t w) x ↔ ∃ (t' : FTag B φ) (w' : Fin (tagDim B φ t') → A), x = ptOf B φ a₀ t' w' ∧ BindG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w')

A binder is a point.

theorem DescriptiveComplexity.FinSat.not_bindG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' : FTag B φ) (hb : bindBodyF B φ t t' = ⊥) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) : ¬BindG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w')

A tag pair the binding relation is not defined at binds nothing.

theorem DescriptiveComplexity.FinSat.bindG_nd_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (x : (finsatInterp B φ).Map A) : BindG (ndPt B φ a₀ p pol) x ↔ ∃ (l : Fin (Tseitin.maxCtx φ)), qLevel B φ p = some ↑l ∧ x = dbvarPt B φ a₀ l

What a quantifier of the kernel binds: the variable of the de Bruijn level it introduces, and nothing else.

The environment, as a de Bruijn context

An environment of the encoded sentence assigns a model element to every element of the image; what the kernel's own recursion reads is only its restriction to the variables of the de Bruijn levels. Passing under a quantifier updates the environment at one variable, and that is exactly Fin.snoc on the context tuple – the one calculation the quantifier case of the kernel recursion needs.

theorem DescriptiveComplexity.FinSat.dbvarPt_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {l l' : Fin (Tseitin.maxCtx φ)} (h : dbvarPt B φ a₀ l = dbvarPt B φ a₀ l') : l = l'

The variables of two distinct de Bruijn levels are distinct elements.

def DescriptiveComplexity.FinSat.envOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (v : (finsatInterp B φ).Map A → M) : Fin (Tseitin.maxCtx φ) → M

The de Bruijn context an environment carries.

Equations

• DescriptiveComplexity.FinSat.envOf B φ a₀ v l = v (DescriptiveComplexity.FinSat.dbvarPt B φ a₀ l)

theorem DescriptiveComplexity.FinSat.pref_envOf_upd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {M : Type} (v : (finsatInterp B φ).Map A → M) {n : ℕ} (hn : n < Tseitin.maxCtx φ) (d : M) : pref ⋯ (envOf B φ a₀ (upd v (dbvarPt B φ a₀ ⟨n, hn⟩) d)) = Fin.snoc (pref ⋯ (envOf B φ a₀ v)) d

Passing under a quantifier is Fin.snoc: updating the environment at the variable of level n extends the context tuple of length n by the value bound there.

The equality literals of the kernel, inverted

The truth definition's literal clauses quantify over the two elements an equality relates, so, as with the children, an arbitrary pair has to be put back into points and the tags then decide.

theorem DescriptiveComplexity.FinSat.canon_of_eqG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {g x y : (finsatInterp B φ).Map A} (h : EqG g x y) : Canon (tagDim B φ x.1) x.2 ∧ Canon (tagDim B φ y.1) y.2

theorem DescriptiveComplexity.FinSat.canon_of_neqG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {g x y : (finsatInterp B φ).Map A} (h : NeqG g x y) : Canon (tagDim B φ x.1) x.2 ∧ Canon (tagDim B φ y.1) y.2

theorem DescriptiveComplexity.FinSat.not_eqG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' t'' : FTag B φ) (hb : eqBodyF B φ t t' t'' = ⊥) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) (w'' : Fin (tagDim B φ t'') → A) : ¬EqG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w'')

theorem DescriptiveComplexity.FinSat.not_neqG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t t' t'' : FTag B φ) (hb : neqBodyF B φ t t' t'' = ⊥) (w : Fin (tagDim B φ t) → A) (w' : Fin (tagDim B φ t') → A) (w'' : Fin (tagDim B φ t'') → A) : ¬NeqG (ptOf B φ a₀ t w) (ptOf B φ a₀ t' w') (ptOf B φ a₀ t'' w'')

theorem DescriptiveComplexity.FinSat.eqG_nd_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (x y : (finsatInterp B φ).Map A) : EqG (ndPt B φ a₀ p pol) x y ↔ ∃ (l₁ : Fin (Tseitin.maxCtx φ)) (l₂ : Fin (Tseitin.maxCtx φ)), (pol = true ∧ eqArgs B φ p = some (↑l₁, ↑l₂)) ∧ x = dbvarPt B φ a₀ l₁ ∧ y = dbvarPt B φ a₀ l₂

The positive equality literals of a kernel node: the variables of the two de Bruijn levels the kernel compares there, at polarity true.

theorem DescriptiveComplexity.FinSat.neqG_nd_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (x y : (finsatInterp B φ).Map A) : NeqG (ndPt B φ a₀ p pol) x y ↔ ∃ (l₁ : Fin (Tseitin.maxCtx φ)) (l₂ : Fin (Tseitin.maxCtx φ)), (pol = false ∧ eqArgs B φ p = some (↑l₁, ↑l₂)) ∧ x = dbvarPt B φ a₀ l₁ ∧ y = dbvarPt B φ a₀ l₂

The same for the negated equalities.

The existential prefix, evaluated

The prefix is the one chain of the encoded sentence, and the one place the proof walks the input order. Its evaluation needs nothing about the kernel: given that the top conjunction holds under the environment sending each variable x_b to its intended value, every node of the prefix holds – by downward induction, from the greatest element of the input order, where the child is the top conjunction, to the least, which is the root of the sentence.

theorem DescriptiveComplexity.FinSat.pvarPt_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ b c : A} (h : pvarPt B φ a₀ b = pvarPt B φ a₀ c) : b = c

The variables of the prefix are pairwise distinct: they are the elements the sentence's diagram forces apart.

theorem DescriptiveComplexity.FinSat.gval_prePt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (ι : A → M) (hbody : ∀ (v : (finsatInterp B φ).Map A → M), (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → Gval I v (bodyPt B φ a₀)) (a : A) (v : (finsatInterp B φ).Map A → M) : (∀ b < a, v (pvarPt B φ a₀ b) = ι b) → Gval I v (prePt B φ a₀ a)

The prefix holds: at every element of the input order, provided the top conjunction holds once every variable has been given its intended value.

theorem DescriptiveComplexity.FinSat.not_rootG_ptOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (t : FTag B φ) (hb : rootBodyF B φ t = ⊥) (w : Fin (tagDim B φ t) → A) : ¬RootG (ptOf B φ a₀ t w)

A tag the root marker is not defined at marks nothing.

theorem DescriptiveComplexity.FinSat.gval_rootG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (ι : A → M) (hbody : ∀ (v : (finsatInterp B φ).Map A → M), (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → Gval I v (bodyPt B φ a₀)) (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) (hg : RootG g) : Gval I v g

The root of the encoded sentence holds, which is what finite satisfiability asks: the root is the prefix node of the least element, and no variable is bound outside it.

The diagram, evaluated

What is left of the ⟹ direction, once the prefix is walked: the top conjunction. Its children are the distinctness literals and the root of the translated kernel, so it holds as soon as the environment separates the variables of distinct elements – which the intended assignment does, being injective – and the kernel holds.

theorem DescriptiveComplexity.FinSat.gval_bodyPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (hdiag : ∀ (a b : A), a ≠ b → v (pvarPt B φ a₀ a) ≠ v (pvarPt B φ a₀ b)) (hker : Gval I v (ndPt B φ a₀ (rootPos B φ) true)) : Gval I v (bodyPt B φ a₀)

The top conjunction holds when the environment separates the variables of distinct elements and the root of the translated kernel holds.

theorem DescriptiveComplexity.FinSat.gval_of_kernel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (ι : A → M) (hinj : Function.Injective ι) (hker : ∀ (v : (finsatInterp B φ).Map A → M), (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → Gval I v (ndPt B φ a₀ (rootPos B φ) true)) (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) (hg : RootG g) : Gval I v g

The encoded sentence holds, modulo its kernel: the whole of the ⟹ direction that does not depend on φ. An injective intended assignment ι of the prefix variables satisfies the diagram, the prefix chain carries it to the root, and what is left to prove of σ_A is that the root of the translated kernel holds under every environment giving the prefix variables their intended values.

The model side: an interpretation from an assignment of the block

DescriptiveComplexity.FinSat.FinSatOn asks for a model together with a local interpretation – one that reads a symbol only at the argument positions of its own signature. The relation variables of the block give one: the symbol of a variable is interpreted by that variable's relation, read at the argument positions. Locality is what makes it a relation of the symbol's own arity rather than of the whole universe, and it is the condition the truth definition's atom clauses are stated against.

theorem DescriptiveComplexity.FinSat.symPt_inj {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {i i' : B.ι} (h : symPt B φ a₀ i = symPt B φ a₀ i') : i = i'

Distinct relation variables get distinct symbols.

noncomputable def DescriptiveComplexity.FinSat.argTup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (i : B.ι) (w : (finsatInterp B φ).Map A → M) : Fin (B.arity i) → M

The arguments an assignment of the argument positions gives to a relation variable. A variable of the block whose arity exceeds the dimension cannot occur in the kernel, so the sentence never reads it; the value taken there is immaterial, and reading it at the first position keeps the whole tuple inside the symbol's signature, which is what locality asks.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.blockI {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (μ : B.Assignment M) : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop

The interpretation determined by an assignment of the block.

Equations

• DescriptiveComplexity.FinSat.blockI B φ a₀ μ s w = ∃ (i : B.ι), s = DescriptiveComplexity.FinSat.symPt B φ a₀ i ∧ μ i (DescriptiveComplexity.FinSat.argTup B φ a₀ i w)

theorem DescriptiveComplexity.FinSat.argTup_congr {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (i : B.ι) {w w' : (finsatInterp B φ).Map A → M} (hag : ∀ (p : (finsatInterp B φ).Map A), SigG (symPt B φ a₀ i) p → w p = w' p) : argTup B φ a₀ i w = argTup B φ a₀ i w'

The arguments of a relation variable are read inside its signature.

theorem DescriptiveComplexity.FinSat.local_blockI {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (μ : B.Assignment M) : Local (blockI B φ a₀ μ)

The interpretation is local, so it is a genuine interpretation of the encoded sentence's vocabulary.

theorem DescriptiveComplexity.FinSat.blockI_symPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A M : Type} (a₀ : A) (μ : B.Assignment M) (i : B.ι) (w : (finsatInterp B φ).Map A → M) : blockI B φ a₀ μ (symPt B φ a₀ i) w ↔ μ i (argTup B φ a₀ i w)

The atom of a relation variable, read on the image: at a node carrying a block atom of the kernel, the interpretation holds of an assignment exactly when the variable's relation holds of the arguments that assignment gives.

The atom clause does not depend on the assignment it is read at

The truth definition reads an atom at some assignment of the argument positions matching the environment on the atom's arguments. Two such assignments agree on every position of the symbol's signature – that is what DescriptiveComplexity.FinSat.IsWF.arg_tot gives – so a local interpretation cannot tell them apart, and the clause may always be read at the canonical assignment below. This is the one place the shape conditions of well-formedness are used for something other than being proved.

noncomputable def DescriptiveComplexity.FinSat.argAssign {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {M : Type} (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) (junk : M) : (finsatInterp B φ).Map A → M

The canonical assignment of the argument positions of a node: the value of the argument sitting there, and anything at all elsewhere.

Equations

• DescriptiveComplexity.FinSat.argAssign B φ v g junk q = if h : ∃ (x : (DescriptiveComplexity.FinSat.finsatInterp B φ).Map A), DescriptiveComplexity.FinSat.ArgG g q x then v h.choose else junk

theorem DescriptiveComplexity.FinSat.argAssign_spec {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {M : Type} (v : (finsatInterp B φ).Map A → M) (g : (finsatInterp B φ).Map A) (junk : M) (q x : (finsatInterp B φ).Map A) (hx : ArgG g q x) : argAssign B φ v g junk q = v x

It does match the environment on the arguments – the atom of the image has at most one argument at each position.

theorem DescriptiveComplexity.FinSat.interp_matching_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {M : Type} [L.IsRelational] [Finite A] [Nonempty A] {I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop} (hloc : Local I) (v : (finsatInterp B φ).Map A → M) (g s : (finsatInterp B φ).Map A) (hs : PosG g s ∨ NegG g s) (w : (finsatInterp B φ).Map A → M) (junk : M) (hw : ∀ (p x : (finsatInterp B φ).Map A), ArgG g p x → w p = v x) : I s w ↔ I s (argAssign B φ v g junk)

Any matching assignment gives the atom the same value as the canonical one: they agree on the signature of the symbol, and the interpretation is local.

The atoms of the relation variables, evaluated

Putting the last three pieces together: at a node of the kernel carrying an atom of a relation variable, the atom clause of the truth definition says exactly that the variable's relation holds of the values its arguments take. This is the one clause of the kernel recursion that mentions the model at all.

theorem DescriptiveComplexity.FinSat.eq_symPt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : (finsatInterp B φ).Map A} {i : B.ι} (ht : x.1 = Tag.sym i) (h : Canon 0 x.2) : x = symPt B φ a₀ i

An element canonical at dimension zero carrying the tag of a symbol is that symbol.

theorem DescriptiveComplexity.FinSat.posG_ndPt_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (s : (finsatInterp B φ).Map A) : PosG (ndPt B φ a₀ p pol) s ↔ ∃ (i : B.ι), pol = true ∧ blockSym B φ p = some i ∧ s = symPt B φ a₀ i

The symbol of an atom of the image: a node of the kernel carries a positive atom exactly when it sits at polarity true on a block atom, and then the symbol is that of its relation variable.

theorem DescriptiveComplexity.FinSat.negG_ndPt_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (s : (finsatInterp B φ).Map A) : NegG (ndPt B φ a₀ p pol) s ↔ ∃ (i : B.ι), pol = false ∧ blockSym B φ p = some i ∧ s = symPt B φ a₀ i

The same at polarity false: a negated atom.

theorem DescriptiveComplexity.FinSat.posAtom_clause_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (μ : B.Assignment M) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (i : B.ι) (hi : blockSym B φ p = some i) (junk : M) : (∃ (s : (finsatInterp B φ).Map A), PosG (ndPt B φ a₀ p true) s ∧ ∃ (w : (finsatInterp B φ).Map A → M), (∀ (q x : (finsatInterp B φ).Map A), ArgG (ndPt B φ a₀ p true) q x → w q = v x) ∧ blockI B φ a₀ μ s w) ↔ μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p true) junk))

The positive-atom clause of the truth definition, evaluated.

theorem DescriptiveComplexity.FinSat.negAtom_clause_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (μ : B.Assignment M) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (i : B.ι) (hi : blockSym B φ p = some i) (junk : M) : (∃ (s : (finsatInterp B φ).Map A), NegG (ndPt B φ a₀ p false) s ∧ ∃ (w : (finsatInterp B φ).Map A → M), (∀ (q x : (finsatInterp B φ).Map A), ArgG (ndPt B φ a₀ p false) q x → w q = v x) ∧ ¬blockI B φ a₀ μ s w) ↔ ¬μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p false) junk))

The negated-atom clause, the same at polarity false.

The nodes of a translated atom

An atom the sentence may not mention becomes a disjunction over the tuples where it holds, each tuple a conjunction of equality literals pinning one argument to a prefix variable. Those two node kinds need the same treatment as the kernel's: which clause of the truth definition fires, and which elements it relates.

theorem DescriptiveComplexity.FinSat.not_posG_of_ne_nd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (t : FTag B φ) (ht : ∀ (q : Pos B φ) (pol : Bool), t ≠ Tag.nd q pol) (w : Fin (tagDim B φ t) → A) (s : (finsatInterp B φ).Map A) : ¬PosG (ptOf B φ a₀ t w) s

A node that is not a translation of a kernel position carries no atom.

theorem DescriptiveComplexity.FinSat.not_negG_of_ne_nd {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (t : FTag B φ) (ht : ∀ (q : Pos B φ) (pol : Bool), t ≠ Tag.nd q pol) (w : Fin (tagDim B φ t) → A) (s : (finsatInterp B φ).Map A) : ¬NegG (ptOf B φ a₀ t w) s

theorem DescriptiveComplexity.FinSat.not_eqG_atup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) (x y : (finsatInterp B φ).Map A) : ¬EqG (atupPt B φ a₀ p pol w) x y

A tuple node of a translated atom carries no equality literal: it is a conjunction of them, not one itself.

theorem DescriptiveComplexity.FinSat.not_neqG_atup {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A) (x y : (finsatInterp B φ).Map A) : ¬NeqG (atupPt B φ a₀ p pol w) x y

theorem DescriptiveComplexity.FinSat.eqG_alit_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (a : A) (x y : (finsatInterp B φ).Map A) : EqG (alitPt B φ a₀ p pol j a) x y ↔ ∃ (l : Fin (Tseitin.maxCtx φ)) (b : A), (pol = true ∧ inArg B φ p ↑j = some ↑l) ∧ a = b ∧ x = dbvarPt B φ a₀ l ∧ y = pvarPt B φ a₀ b

The equality literal of a translated atom, inverted: it relates the variable of the argument's de Bruijn level to the prefix variable of the element its tuple holds there.

theorem DescriptiveComplexity.FinSat.neqG_alit_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (p : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (a : A) (x y : (finsatInterp B φ).Map A) : NeqG (alitPt B φ a₀ p pol j a) x y ↔ ∃ (l : Fin (Tseitin.maxCtx φ)) (b : A), (pol = false ∧ inArg B φ p ↑j = some ↑l) ∧ a = b ∧ x = dbvarPt B φ a₀ l ∧ y = pvarPt B φ a₀ b

The same for a negatively translated atom.

The one place the input structure is read

The tuple nodes of a translated atom are selected by a defining formula, so reading them off the image means realizing that formula: for an atom of the input vocabulary it is the atom itself, at the tuple the node holds; for the marker old it is ⊤, since every original element is old. The kernelNode equation is a hypothesis to rewrite with – its arity is an implicit argument, so destructing it would land in HEq.

theorem DescriptiveComplexity.FinSat.realize_inAtomF_input {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {p : Pos B φ} {k : ℕ} {r : L.Relations k} {args : Fin k → Option ℕ} (hk : kernelNode φ p.snd = KernelNode.inputAtom r args) (h : k ≤ finsatDim B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (inAtomF B φ p).Realize v ↔ FirstOrder.Language.Structure.RelMap r fun (j : Fin k) => v (1, Fin.castLE h j)

theorem DescriptiveComplexity.FinSat.realize_inAtomF_old {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {p : Pos B φ} {x : Option ℕ} (hk : kernelNode φ p.snd = KernelNode.oldAtom x) (v : Fin 2 × Fin (finsatDim B φ) → A) : (inAtomF B φ p).Realize v

The truth definition at a node of the kernel

What the kernel says at a position decides which clause of the truth definition can fire there, and the other seven are then vacuous. These two lemmas do that bookkeeping once: at a node translating an n-ary connective – falsity, an implication or an atom the sentence may not mention – the value is the disjunction of the children's at polarity true and their conjunction at polarity false.

theorem DescriptiveComplexity.FinSat.gstep_conn_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : isConn B φ p) : gstep I rec v (ndPt B φ a₀ p true) ↔ ∃ (c : (finsatInterp B φ).Map A), ChildG (ndPt B φ a₀ p true) c ∧ rec v c

theorem DescriptiveComplexity.FinSat.gstep_conn_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : isConn B φ p) : gstep I rec v (ndPt B φ a₀ p false) ↔ ∀ (c : (finsatInterp B φ).Map A), ChildG (ndPt B φ a₀ p false) c → rec v c

At a quantifier node the value is the conjunction (respectively the disjunction) over the model of the child's, the bound variable of the level the quantifier introduces taking each value in turn.

theorem DescriptiveComplexity.FinSat.gstep_quant_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (l : Fin (Tseitin.maxCtx φ)) (hq : qLevel B φ p = some ↑l) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : ¬isConn B φ p) : gstep I rec v (ndPt B φ a₀ p true) ↔ ∀ (d : M) (c : (finsatInterp B φ).Map A), ChildG (ndPt B φ a₀ p true) c → rec (upd v (dbvarPt B φ a₀ l) d) c

theorem DescriptiveComplexity.FinSat.gstep_quant_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (l : Fin (Tseitin.maxCtx φ)) (hq : qLevel B φ p = some ↑l) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : ¬isConn B φ p) : gstep I rec v (ndPt B φ a₀ p false) ↔ ∃ (d : M) (c : (finsatInterp B φ).Map A), ChildG (ndPt B φ a₀ p false) c ∧ rec (upd v (dbvarPt B φ a₀ l) d) c

At a node translating an equality of the kernel the value is that equality, read at the variables of the two de Bruijn levels.

theorem DescriptiveComplexity.FinSat.gstep_eqLit_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (l₁ l₂ : Fin (Tseitin.maxCtx φ)) (hq : qLevel B φ p = none) (he : eqArgs B φ p = some (↑l₁, ↑l₂)) (hs : blockSym B φ p = none) (hcn : ¬isConn B φ p) : gstep I rec v (ndPt B φ a₀ p true) ↔ v (dbvarPt B φ a₀ l₁) = v (dbvarPt B φ a₀ l₂)

theorem DescriptiveComplexity.FinSat.gstep_eqLit_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (l₁ l₂ : Fin (Tseitin.maxCtx φ)) (hq : qLevel B φ p = none) (he : eqArgs B φ p = some (↑l₁, ↑l₂)) (hs : blockSym B φ p = none) (hcn : ¬isConn B φ p) : gstep I rec v (ndPt B φ a₀ p false) ↔ v (dbvarPt B φ a₀ l₁) ≠ v (dbvarPt B φ a₀ l₂)

At a node translating an atom of a relation variable – the only genuine atoms of the encoded sentence – the value is that relation, read at the values of the atom's arguments.

theorem DescriptiveComplexity.FinSat.gstep_blockAtom_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (μ : B.Assignment M) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (i : B.ι) (junk : M) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = some i) (hcn : ¬isConn B φ p) : gstep (blockI B φ a₀ μ) rec v (ndPt B φ a₀ p true) ↔ μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p true) junk))

theorem DescriptiveComplexity.FinSat.gstep_blockAtom_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (μ : B.Assignment M) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (i : B.ι) (junk : M) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = some i) (hcn : ¬isConn B φ p) : gstep (blockI B φ a₀ μ) rec v (ndPt B φ a₀ p false) ↔ ¬μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p false) junk))

The kernel, position by position

The cases of the induction, each stated for a subformula of the kernel embedded by a DescriptiveComplexity.FinSat.SubEmb: the shape facts come from SubEmb.node, the children from SubEmb.kid and SubEmb.kid_range through DescriptiveComplexity.FinSat.childG_nd_iff.

theorem DescriptiveComplexity.FinSat.gval_nd_falsum {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) {n : ℕ} (E : SubEmb φ FirstOrder.Language.BoundedFormula.falsum) : ¬Gval I v (ndPt B φ a₀ ⟨n, E.emb (Tseitin.rootAt FirstOrder.Language.BoundedFormula.falsum)⟩ true) ∧ Gval I v (ndPt B φ a₀ ⟨n, E.emb (Tseitin.rootAt FirstOrder.Language.BoundedFormula.falsum)⟩ false)

A node translating falsity has no children at all: at polarity true it is the empty disjunction, which is false, and at false the empty conjunction, which is true.

theorem DescriptiveComplexity.FinSat.gval_nd_impl {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p p₁ p₂ : Pos B φ) (hk : kernelNode φ p.snd = KernelNode.impl) (h1 : kidOf φ p.snd p₁.snd = some true) (h2 : kidOf φ p.snd p₂.snd = some false) (henum : ∀ (q : Pos B φ) (b : Bool), kidOf φ p.snd q.snd = some b → b = true ∧ q = p₁ ∨ b = false ∧ q = p₂) : (Gval I v (ndPt B φ a₀ p true) ↔ Gval I v (ndPt B φ a₀ p₁ false) ∨ Gval I v (ndPt B φ a₀ p₂ true)) ∧ (Gval I v (ndPt B φ a₀ p false) ↔ Gval I v (ndPt B φ a₀ p₁ true) ∧ Gval I v (ndPt B φ a₀ p₂ false))

A node translating an implication: at polarity true it is the disjunction of the negated premise and the conclusion, at false the conjunction of the premise and the negated conclusion – negation normal form, as a polarity flag on the premise.

theorem DescriptiveComplexity.FinSat.gval_nd_quant {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p p' : Pos B φ) (l : Fin (Tseitin.maxCtx φ)) (hk : kernelNode φ p.snd = KernelNode.quant ↑l) (h1 : kidOf φ p.snd p'.snd = some false) (henum : ∀ (q : Pos B φ) (b : Bool), kidOf φ p.snd q.snd = some b → b = false ∧ q = p') : (Gval I v (ndPt B φ a₀ p true) ↔ ∀ (d : M), Gval I (upd v (dbvarPt B φ a₀ l) d) (ndPt B φ a₀ p' true)) ∧ (Gval I v (ndPt B φ a₀ p false) ↔ ∃ (d : M), Gval I (upd v (dbvarPt B φ a₀ l) d) (ndPt B φ a₀ p' false))

A node translating a quantifier: at polarity true it is the conjunction over the model of the body's values, at false the disjunction – the variable of the de Bruijn level the quantifier introduces taking each value of the model in turn.

theorem DescriptiveComplexity.FinSat.gval_nd_eqLit {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (l₁ l₂ : Fin (Tseitin.maxCtx φ)) (hk : kernelNode φ p.snd = KernelNode.eqLit (some ↑l₁) (some ↑l₂)) : (Gval I v (ndPt B φ a₀ p true) ↔ v (dbvarPt B φ a₀ l₁) = v (dbvarPt B φ a₀ l₂)) ∧ (Gval I v (ndPt B φ a₀ p false) ↔ v (dbvarPt B φ a₀ l₁) ≠ v (dbvarPt B φ a₀ l₂))

A node translating an equality of the kernel: the equality of the values of the two variables, negated at polarity false.

theorem DescriptiveComplexity.FinSat.gval_nd_blockAtom {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (μ : B.Assignment M) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (i : B.ι) (junk : M) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = some i) (hcn : ¬isConn B φ p) : (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ p true) ↔ μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p true) junk))) ∧ (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ p false) ↔ ¬μ i (argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p false) junk)))

A node translating an atom of a relation variable: the relation the assignment gives that variable, read at the values of the atom's arguments.

The truth definition at the two node kinds of a translated atom: a tuple node is the conjunction of its literals (the disjunction, at a negatively translated atom), and a literal is the equality it carries.

theorem DescriptiveComplexity.FinSat.gstep_atup_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (w : Fin (tagDim B φ (Tag.atup p true)) → A) (hin : isInAtom B φ p) : gstep I rec v (atupPt B φ a₀ p true w) ↔ ∀ (c : (finsatInterp B φ).Map A), ChildG (atupPt B φ a₀ p true w) c → rec v c

theorem DescriptiveComplexity.FinSat.gstep_atup_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (w : Fin (tagDim B φ (Tag.atup p false)) → A) (hin : isInAtom B φ p) : gstep I rec v (atupPt B φ a₀ p false w) ↔ ∃ (c : (finsatInterp B φ).Map A), ChildG (atupPt B φ a₀ p false w) c ∧ rec v c

theorem DescriptiveComplexity.FinSat.gstep_alit_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (j : Fin (finsatDim B φ)) (a : A) (l : Fin (Tseitin.maxCtx φ)) (hl : inArg B φ p ↑j = some ↑l) : gstep I rec v (alitPt B φ a₀ p true j a) ↔ v (dbvarPt B φ a₀ l) = v (pvarPt B φ a₀ a)

theorem DescriptiveComplexity.FinSat.gstep_alit_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (rec : ((finsatInterp B φ).Map A → M) → (finsatInterp B φ).Map A → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (j : Fin (finsatDim B φ)) (a : A) (l : Fin (Tseitin.maxCtx φ)) (hl : inArg B φ p ↑j = some ↑l) : gstep I rec v (alitPt B φ a₀ p false j a) ↔ v (dbvarPt B φ a₀ l) ≠ v (pvarPt B φ a₀ a)

theorem DescriptiveComplexity.FinSat.gval_atup_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (w : Fin (tagDim B φ (Tag.atup p true)) → A) (hin : isInAtom B φ p) : Gval I v (atupPt B φ a₀ p true w) ↔ ∀ (j : Fin (finsatDim B φ)), ↑j < inArity B φ p → Gval I v (alitPt B φ a₀ p true j (pad a₀ w j))

A tuple node of a translated atom is the conjunction of its literals, one per argument position.

theorem DescriptiveComplexity.FinSat.gval_atup_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (w : Fin (tagDim B φ (Tag.atup p false)) → A) (hin : isInAtom B φ p) : Gval I v (atupPt B φ a₀ p false w) ↔ ∃ (j : Fin (finsatDim B φ)), ↑j < inArity B φ p ∧ Gval I v (alitPt B φ a₀ p false j (pad a₀ w j))

At a negatively translated atom the tuple node is the disjunction of its literals: negation normal form has pushed the negation to the leaves.

theorem DescriptiveComplexity.FinSat.gval_nd_inAtom {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : isConn B φ p) (hnokid : ∀ (q : Pos B φ) (b : Bool), kidOf φ p.snd q.snd ≠ some b) : (Gval I v (ndPt B φ a₀ p true) ↔ ∃ (w : Fin (tagDim B φ (Tag.atup p true)) → A), (inAtomF B φ p).Realize (val₂ B φ (ptOf B φ a₀ (Tag.nd p true) fun (x : Fin (tagDim B φ (Tag.nd p true))) => a₀) (ptOf B φ a₀ (Tag.atup p true) w)) ∧ Gval I v (atupPt B φ a₀ p true w)) ∧ (Gval I v (ndPt B φ a₀ p false) ↔ ∀ (w : Fin (tagDim B φ (Tag.atup p false)) → A), (inAtomF B φ p).Realize (val₂ B φ (ptOf B φ a₀ (Tag.nd p false) fun (x : Fin (tagDim B φ (Tag.nd p false))) => a₀) (ptOf B φ a₀ (Tag.atup p false) w)) → Gval I v (atupPt B φ a₀ p false w))

A node translating an atom the sentence may not mention: the disjunction, over the tuples where the atom holds, of the conjunctions of its literals – and dually at polarity false. This is the Tseitin trick: the tuples are selected by a defining formula, so the input structure is read by the interpretation and never by the encoded sentence.

theorem DescriptiveComplexity.FinSat.gval_alit_true {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (j : Fin (finsatDim B φ)) (a : A) (l : Fin (Tseitin.maxCtx φ)) (hl : inArg B φ p ↑j = some ↑l) : Gval I v (alitPt B φ a₀ p true j a) ↔ v (dbvarPt B φ a₀ l) = v (pvarPt B φ a₀ a)

A literal of a translated atom, evaluated: it pins the argument at its position to the prefix variable of the element the tuple holds there.

theorem DescriptiveComplexity.FinSat.gval_alit_false {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (j : Fin (finsatDim B φ)) (a : A) (l : Fin (Tseitin.maxCtx φ)) (hl : inArg B φ p ↑j = some ↑l) : Gval I v (alitPt B φ a₀ p false j a) ↔ v (dbvarPt B φ a₀ l) ≠ v (pvarPt B φ a₀ a)

The kernel, by induction on the formula

The node lemmas above are stated about a position; tying them together is an induction on the kernel itself, carried by a DescriptiveComplexity.FinSat.SubEmb – a subformula together with an embedding of its positions into the kernel's – so that the clause of a node, which quantifies over all the children it has in the kernel, collapses to the subformula (SubEmb.no_children, SubEmb.imp_children, SubEmb.all_children).

Two things fall out of the same induction rather than being assumed: negation normal form, as the second half of each statement, and the quantifier step, where updating the environment at the variable of the level bound there is Fin.snoc on the context tuple (pref_envOf_upd).

The model is any structure over DescriptiveComplexity.newLang L whose relations are read through an injection ι of the instance – the shape an extended universe A ⊕ Fin m has (DescriptiveComplexity.relMap_ext_iff), and the only thing about it the translation uses.

theorem DescriptiveComplexity.FinSat.argTup_argAssign {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} (ha₀ : IsBot a₀) (v : (finsatInterp B φ).Map A → M) (p : Pos B φ) (pol : Bool) (i : B.ι) (hs : blockSym B φ p = some i) (junk : M) (j : Fin (B.arity i)) (l : Fin (Tseitin.maxCtx φ)) (hl : blockArg B φ p ↑j = some ↑l) : argTup B φ a₀ i (argAssign B φ v (ndPt B φ a₀ p pol) junk) j = v (dbvarPt B φ a₀ l)

The arguments of an atom of a relation variable: the canonical assignment of the argument positions gives, at each of them, the value of the variable of that argument's de Bruijn level.

theorem DescriptiveComplexity.FinSat.val₂_one {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} (x y : (finsatInterp B φ).Map A) (c : Fin (finsatDim B φ)) : val₂ B φ x y (1, c) = y.2 c

The second point a binary defining formula of the image is read at.

theorem DescriptiveComplexity.FinSat.inAtom_levels {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} {a₀ : A} {M : Type} [L.IsRelational] [(newLang L).Structure M] {n k : ℕ} (hn : n ≤ Tseitin.maxCtx φ) (v : (finsatInterp B φ).Map A → M) (ts : Fin k → ((newLang L).sum B.lang).Term (Empty ⊕ Fin n)) {p : Pos B φ} (hia : ∀ (j : ℕ) (h : j < k), inArg B φ p j = termLevel (ts ⟨j, h⟩)) : ∃ (lev : Fin k → Fin (Tseitin.maxCtx φ)), (∀ (j : Fin k), inArg B φ p ↑j = some ↑(lev j)) ∧ ∀ (j : Fin k), FirstOrder.Language.Term.realize (Sum.elim (fun (a : Empty) => isEmptyElim a) (pref hn (envOf B φ a₀ v))) (Tseitin.termToL (ts j)) = v (dbvarPt B φ a₀ (lev j))

The de Bruijn levels of the arguments of a translated atom, and the values its terms take: in a relational vocabulary every argument is a variable, so it has a level, and the value of the term is the context tuple there.

theorem DescriptiveComplexity.FinSat.atom_translation {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) (I : (finsatInterp B φ).Map A → ((finsatInterp B φ).Map A → M) → Prop) (v : (finsatInterp B φ).Map A → M) (ι : A → M) (hv : ∀ (b : A), v (pvarPt B φ a₀ b) = ι b) (p : Pos B φ) (hq : qLevel B φ p = none) (he : eqArgs B φ p = none) (hs : blockSym B φ p = none) (hcn : isConn B φ p) (hin : isInAtom B φ p) (hnokid : ∀ (q : Pos B φ) (b : Bool), kidOf φ p.snd q.snd ≠ some b) {k : ℕ} (hdim : inArity B φ p = k) (hkd : k ≤ finsatDim B φ) (lev : Fin k → Fin (Tseitin.maxCtx φ)) (hlev : ∀ (j : Fin k), inArg B φ p ↑j = some ↑(lev j)) (Filt : (Fin k → A) → Prop) {Q : Prop} (hRW : Q ↔ ∃ (y : Fin k → A), Filt y ∧ ∀ (j : Fin k), v (dbvarPt B φ a₀ (lev j)) = ι (y j)) (hfilt : ∀ (pol : Bool) (w : Fin (tagDim B φ (Tag.atup p pol)) → A), (inAtomF B φ p).Realize (val₂ B φ (ptOf B φ a₀ (Tag.nd p pol) fun (x : Fin (tagDim B φ (Tag.nd p pol))) => a₀) (ptOf B φ a₀ (Tag.atup p pol) w)) ↔ Filt fun (j : Fin k) => pad a₀ w ⟨↑j, ⋯⟩) : (Gval I v (ndPt B φ a₀ p true) ↔ Q) ∧ (Gval I v (ndPt B φ a₀ p false) ↔ ¬Q)

A node translating an atom the sentence may not mention, evaluated: the disjunction over the tuples the defining formula selects, of the conjunctions of the literals pinning each argument to a prefix variable, is the atom – read at the values the environment gives the arguments' de Bruijn levels, through the intended assignment ι of the prefix variables.

Stated once for the two shapes it serves: an atom of the input vocabulary, where the filter Filt is the atom itself, and the marker old, where it is ⊤.

theorem DescriptiveComplexity.FinSat.gval_kernel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {M : Type} [L.IsRelational] [Finite A] [Nonempty A] (ha₀ : IsBot a₀) [(newLang L).Structure M] [Nonempty M] (μ : B.Assignment M) (ι : A → M) (hrel : ∀ {k : ℕ} (r : L.Relations k) (u : Fin k → M), FirstOrder.Language.Structure.RelMap (Sum.inl r) u ↔ ∃ (y : Fin k → A), FirstOrder.Language.Structure.RelMap r y ∧ ∀ (j : Fin k), u j = ι (y j)) (hold : ∀ (u : Fin 1 → M), FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) u ↔ ∃ (a : A), u 0 = ι a) {n : ℕ} (f : ((newLang L).sum B.lang).BoundedFormula Empty n) (x✝ : SubEmb φ f) (hn : n ≤ Tseitin.maxCtx φ) (v : (finsatInterp B φ).Map A → M) : (∀ (b : A), v (pvarPt B φ a₀ b) = ι b) → (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ ⟨n, x✝.emb (Tseitin.rootAt f)⟩ true) ↔ Tseitin.RealizeWith μ f (pref hn (envOf B φ a₀ v))) ∧ (Gval (blockI B φ a₀ μ) v (ndPt B φ a₀ ⟨n, x✝.emb (Tseitin.rootAt f)⟩ false) ↔ ¬Tseitin.RealizeWith μ f (pref hn (envOf B φ a₀ v)))

The translated kernel computes the kernel: at every position of the kernel the node of the encoded sentence at polarity true holds exactly when the subformula there does, and the node at polarity false exactly when it does not.

The environment gives the prefix variables their intended values ι and the variables of the de Bruijn levels the context tuple; the model reads the relations of the instance through ι, which is what an extended universe does.