The sentence a reduction into FINSAT produces

The interpretation σ_A: given the second-order block B and the first-order kernel φ of an ∃SO[new] definition, the encoded sentence

∃x_{a₁} … ∃x_{aₙ} ( ⋀_{a ≠ b} x_a ≠ x_b  ∧  φ* )

defined inside an ordered input structure. Its vocabulary is B.ι and nothing else: neither the symbols of the input nor the marker old occur in it, because each of their atoms is translated into a disjunction over the tuples where it holds, whose defining formula contains the atom – the Tseitin trick, so that the input structure is read by the interpretation and never by the sentence.

What each tag defines

The tags are DescriptiveComplexity.FinSat.Tag (DescriptiveComplexity.Problems.FinSat.Nodes), the positions of the kernel are read by DescriptiveComplexity.FinSat.kernelNode and DescriptiveComplexity.FinSat.kidOf (DescriptiveComplexity.Problems.FinSat.Kernel), and this file adds the accessors those two are consumed through together with one defining formula per relation symbol of DescriptiveComplexity.FINSAT:

• the kinds (andN, orN, allN, exN) are read off the constructor at a position and the polarity – falsity, an implication and a translated atom are a disjunction at polarity true and a conjunction at polarity false, an empty one in the case of falsity; a quantifier is allN at true and exN at false; and the prefix nodes are exN;
• child threads the prefix along the immediate successors of the input order, hands the last of them the top conjunction, gives that conjunction the distinctness literals and the root of the translated kernel, and inside the kernel follows DescriptiveComplexity.FinSat.kidOf. The one place the input structure is read is the child relation between a translated atom and its tuple nodes (DescriptiveComplexity.FinSat.inAtomF);
• bind binds x_a at the prefix node of a and the variable of a de Bruijn level at a quantifier node; eqL/neqL carry the equality literals of the kernel, of the diagram and of the translated atoms; posL/negL, arg and sig carry the atoms of the relation variables, which are the only genuine atoms of the sentence;
• le compares the tags by their key (DescriptiveComplexity.FinSat.Tag.tagKey) and, within one tag, the tuples lexicographically – reversed inside the prefix, whose chain descends as the input order grows;
• root marks the prefix node of the least element.

Every relation but le is guarded by canonicity (DescriptiveComplexity.FinSat.canonG): a tag uses only its first DescriptiveComplexity.FinSat.tagDim coordinates, and a tuple padded otherwise is junk – an element of the encoded sentence that no node binds and no literal reads. le carries no such guard, since it has to be a linear order on the whole universe.

The shape of the reduction

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.Pos {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : Type

The subformula positions of the kernel.

Equations

• DescriptiveComplexity.FinSat.Pos B φ = ((m : ℕ) × DescriptiveComplexity.Tseitin.NodeAt φ m)

def DescriptiveComplexity.FinSat.rootPos {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : Pos B φ

The root position of the kernel.

Equations

• DescriptiveComplexity.FinSat.rootPos B φ = ⟨0, DescriptiveComplexity.Tseitin.rootAt φ⟩

def DescriptiveComplexity.FinSat.finsatDim {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : ℕ

The dimension of the reduction: two coordinates for a distinctness literal of the diagram, and one per argument of an atom of the input vocabulary. Nothing needs a context tuple – the encoded sentence quantifies.

Equations

• DescriptiveComplexity.FinSat.finsatDim B φ = max 2 (DescriptiveComplexity.FinSat.maxArity φ)

theorem DescriptiveComplexity.FinSat.two_le_finsatDim {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : 2 ≤ finsatDim B φ

theorem DescriptiveComplexity.FinSat.maxArity_le_finsatDim {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : maxArity φ ≤ finsatDim B φ

def DescriptiveComplexity.FinSat.c0 {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : Fin (finsatDim B φ)

The first coordinate of a tuple of the reduction.

Equations

• DescriptiveComplexity.FinSat.c0 B φ = ⟨0, ⋯⟩

def DescriptiveComplexity.FinSat.c1 {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : Fin (finsatDim B φ)

The second coordinate of a tuple of the reduction.

Equations

• DescriptiveComplexity.FinSat.c1 B φ = ⟨1, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.FTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : Type

The tags of the reduction.

Equations

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

Reading a position, through the accessors the formulas dispatch on

def DescriptiveComplexity.FinSat.posSize {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : ℕ

The size of the subformula at a position: the layer the translation of that position sits in, and what makes the parse DAG of the image descend.

Equations

• DescriptiveComplexity.FinSat.posSize B φ p = DescriptiveComplexity.FinSat.nodeSize φ p.snd

theorem DescriptiveComplexity.FinSat.posSize_le {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : posSize B φ p ≤ fmlSize φ

theorem DescriptiveComplexity.FinSat.posSize_lt_of_kidOf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {p q : Pos B φ} {b : Bool} (h : kidOf φ p.snd q.snd = some b) : posSize B φ q < posSize B φ p

def DescriptiveComplexity.FinSat.blockSym {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : Option B.ι

The relation variable of a block atom at a position, if it is one.

Equations

• DescriptiveComplexity.FinSat.blockSym B φ p = DescriptiveComplexity.FinSat.symOf φ p.snd

def DescriptiveComplexity.FinSat.blockArg {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) (j : ℕ) : Option ℕ

The de Bruijn level of the j-th argument of a block atom.

Equations

• DescriptiveComplexity.FinSat.blockArg B φ p j = DescriptiveComplexity.FinSat.argOf φ p.snd j

theorem DescriptiveComplexity.FinSat.lt_arity_of_blockArg {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {p : Pos B φ} {i : B.ι} {j l : ℕ} (hs : blockSym B φ p = some i) (ha : blockArg B φ p j = some l) : j < B.arity i

An argument of a block atom sits below the arity of its symbol.

theorem DescriptiveComplexity.FinSat.exists_blockArg {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) [L.IsRelational] {p : Pos B φ} {i : B.ι} {j : ℕ} (hs : blockSym B φ p = some i) (hj : j < B.arity i) : ∃ (l : ℕ), blockArg B φ p j = some l ∧ l < Tseitin.maxCtx φ

A block atom has an argument at every position of its signature, and it is the variable of one of the de Bruijn levels of the kernel. Relational: a function symbol would have no level to give.

def DescriptiveComplexity.FinSat.eqArgs {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : Option (ℕ × ℕ)

The two de Bruijn levels of an equality literal at a position.

Equations

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

def DescriptiveComplexity.FinSat.qLevel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : Option ℕ

The de Bruijn level a quantifier at a position binds.

Equations

• DescriptiveComplexity.FinSat.qLevel B φ p = match DescriptiveComplexity.FinSat.kernelNode φ p.snd with | DescriptiveComplexity.FinSat.KernelNode.quant l => some l | x => none

def DescriptiveComplexity.FinSat.inArity {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : ℕ

The arity of an atom the encoded sentence must not mention: one of the input vocabulary, or the marker old.

Equations

• DescriptiveComplexity.FinSat.inArity B φ p = DescriptiveComplexity.FinSat.inArityOf φ p.snd

theorem DescriptiveComplexity.FinSat.inArity_le {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : inArity B φ p ≤ maxArity φ

def DescriptiveComplexity.FinSat.inArg {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) (j : ℕ) : Option ℕ

The de Bruijn level of the j-th argument of such an atom.

Equations

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

def DescriptiveComplexity.FinSat.isInAtom {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : Prop

Whether the position carries such an atom.

Equations

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

def DescriptiveComplexity.FinSat.isConn {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : Prop

Whether the translation turns the position into an n-ary connective: an implication, falsity – the empty one – or an atom translated away.

Equations

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

def DescriptiveComplexity.FinSat.tagDim {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → ℕ

The number of coordinates a tag uses; a tuple not padded with minima beyond them is junk.

Equations

• DescriptiveComplexity.FinSat.tagDim B φ DescriptiveComplexity.FinSat.Tag.body = 0
• DescriptiveComplexity.FinSat.tagDim B φ DescriptiveComplexity.FinSat.Tag.pre = 1
• DescriptiveComplexity.FinSat.tagDim B φ DescriptiveComplexity.FinSat.Tag.pvar = 1
• DescriptiveComplexity.FinSat.tagDim B φ DescriptiveComplexity.FinSat.Tag.neq = 2
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.dbvar l) = 0
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.sym i) = 0
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.apos j) = 0
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) = 0
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.atup p pol) = DescriptiveComplexity.FinSat.inArity B φ p
• DescriptiveComplexity.FinSat.tagDim B φ (DescriptiveComplexity.FinSat.Tag.alit p pol j) = 1

theorem DescriptiveComplexity.FinSat.tagDim_le_finsatDim {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : FTag B φ) : tagDim B φ t ≤ finsatDim B φ

Every tag fits in the dimension: the widest is a tuple node of a translated atom, whose arity occurs in the kernel.

noncomputable def DescriptiveComplexity.FinSat.fkey {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : FTag B φ) : Lex (ℕ × ℕ)

The sorting key of a tag: its layer, then its place in an arbitrary enumeration.

Equations

• DescriptiveComplexity.FinSat.fkey B φ t = DescriptiveComplexity.FinSat.Tag.tagKey (DescriptiveComplexity.FinSat.posSize B φ) (DescriptiveComplexity.FinSat.fmlSize φ) t

def DescriptiveComplexity.FinSat.frank {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : FTag B φ) : ℕ

The layer of a tag, which is what a child of a node descends by everywhere but inside the existential prefix.

Equations

• DescriptiveComplexity.FinSat.frank B φ t = DescriptiveComplexity.FinSat.Tag.tagRank (DescriptiveComplexity.FinSat.posSize B φ) (DescriptiveComplexity.FinSat.fmlSize φ) t

theorem DescriptiveComplexity.FinSat.fkey_lt_of_frank_lt {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' : FTag B φ} (h : frank B φ t < frank B φ t') : fkey B φ t < fkey B φ t'

The defining formulas

noncomputable def DescriptiveComplexity.FinSat.canonG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {n : ℕ} (t : Fin n → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin n × Fin (finsatDim B φ))

Every argument holds a canonically padded tuple of its tag's own length.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.tupLeF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The comparison of the two tuples inside one tag: lexicographic, and reversed inside the prefix, whose chain descends as the input order grows.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.leFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The order of the syntax: the tags by their key, and within one tag the tuples by DescriptiveComplexity.FinSat.tupLeF. No canonicity guard: this has to be a linear order on the whole universe, junk included.

Equations

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

Every relation but le and the child relation is decided by the tags alone, so its defining formula is DescriptiveComplexity.FinSat.tagF of a named tag predicate – never an inline match, whose realization could only be proved by casing on every tag combination at once.

noncomputable def DescriptiveComplexity.FinSat.tagF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {n : ℕ} (t : Fin n → FTag B φ) (P : Prop) : (L.sum FirstOrder.Language.order).Formula (Fin n × Fin (finsatDim B φ))

A defining formula decided by the tags: canonically padded tuples, and a condition on the tags alone.

Equations

• DescriptiveComplexity.FinSat.tagF B φ t P = DescriptiveComplexity.FinSat.canonG B φ t ⊓ if P then ⊤ else ⊥

def DescriptiveComplexity.FinSat.andTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → Prop

The tags of a conjunction node: the top conjunction of the sentence, a connective at polarity false, and the tuple node of a positively translated atom.

Equations

• DescriptiveComplexity.FinSat.andTag B φ DescriptiveComplexity.FinSat.Tag.body = True
• DescriptiveComplexity.FinSat.andTag B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) = (pol = false ∧ DescriptiveComplexity.FinSat.isConn B φ p)
• DescriptiveComplexity.FinSat.andTag B φ (DescriptiveComplexity.FinSat.Tag.atup p pol) = (pol = true ∧ DescriptiveComplexity.FinSat.isInAtom B φ p)
• DescriptiveComplexity.FinSat.andTag B φ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.andFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 1 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The conjunction nodes.

Equations

• DescriptiveComplexity.FinSat.andFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.andTag B φ (t 0))

def DescriptiveComplexity.FinSat.orTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → Prop

The tags of a disjunction node: a connective at polarity true, and the tuple node of a negatively translated atom.

Equations

• DescriptiveComplexity.FinSat.orTag B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) = (pol = true ∧ DescriptiveComplexity.FinSat.isConn B φ p)
• DescriptiveComplexity.FinSat.orTag B φ (DescriptiveComplexity.FinSat.Tag.atup p pol) = (pol = false ∧ DescriptiveComplexity.FinSat.isInAtom B φ p)
• DescriptiveComplexity.FinSat.orTag B φ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.orFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 1 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The disjunction nodes.

Equations

• DescriptiveComplexity.FinSat.orFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.orTag B φ (t 0))

def DescriptiveComplexity.FinSat.allTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → Prop

The tags of a universal quantifier node: a quantifier of the kernel at polarity true.

Equations

• DescriptiveComplexity.FinSat.allTag B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) = (pol = true ∧ (DescriptiveComplexity.FinSat.qLevel B φ p).isSome = true)
• DescriptiveComplexity.FinSat.allTag B φ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.allFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 1 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The universal quantifier nodes.

Equations

• DescriptiveComplexity.FinSat.allFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.allTag B φ (t 0))

def DescriptiveComplexity.FinSat.exTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → Prop

The tags of an existential quantifier node: the prefix, and a quantifier of the kernel at polarity false.

Equations

• DescriptiveComplexity.FinSat.exTag B φ DescriptiveComplexity.FinSat.Tag.pre = True
• DescriptiveComplexity.FinSat.exTag B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) = (pol = false ∧ (DescriptiveComplexity.FinSat.qLevel B φ p).isSome = true)
• DescriptiveComplexity.FinSat.exTag B φ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.exFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 1 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The existential quantifier nodes.

Equations

• DescriptiveComplexity.FinSat.exFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.exTag B φ (t 0))

noncomputable def DescriptiveComplexity.FinSat.inAtomF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (p : Pos B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The one place the input structure is read: the tuple nodes of a translated atom are those where the atom holds, so the atom itself is a defining formula and never a symbol of the encoded sentence. old holds of every original element, so it filters nothing.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.childBodyF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

What makes one tag a child of another, as a named function of the two tags: the prefix threads along the immediate successors of the input order and hands the top conjunction to its last node, that conjunction takes the distinctness literals and the root of the translated kernel, and inside the kernel the child relation follows DescriptiveComplexity.FinSat.kidOf, with a translated atom taking the tuple nodes where it holds and each of those its equality literals. Named, rather than a match inside DescriptiveComplexity.FinSat.childFml, so that its realization is one lemma and each use cases only on the tags it needs.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.childBodyF B φ DescriptiveComplexity.FinSat.Tag.pre DescriptiveComplexity.FinSat.Tag.body = DescriptiveComplexity.maxF (0, DescriptiveComplexity.FinSat.c0 B φ)
• DescriptiveComplexity.FinSat.childBodyF B φ x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.FinSat.childFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The child relation of the parse DAG.

Equations

• DescriptiveComplexity.FinSat.childFml B φ t = DescriptiveComplexity.FinSat.canonG B φ t ⊓ DescriptiveComplexity.FinSat.childBodyF B φ (t 0) (t 1)

noncomputable def DescriptiveComplexity.FinSat.bindBodyF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

What a quantifier node binds, as a named function of the two tags: x_a at the prefix node of a, and the variable of its de Bruijn level at a quantifier of the kernel.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.bindBodyF B φ x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.FinSat.bindFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The variable a quantifier node binds.

Equations

• DescriptiveComplexity.FinSat.bindFml B φ t = DescriptiveComplexity.FinSat.canonG B φ t ⊓ DescriptiveComplexity.FinSat.bindBodyF B φ (t 0) (t 1)

noncomputable def DescriptiveComplexity.FinSat.eqBodyF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → FTag B φ → (L.sum FirstOrder.Language.order).Formula (Fin 3 × Fin (finsatDim B φ))

The positive equality literals, as a named function of the three tags: those of the kernel, and those of a positively translated atom.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.eqBodyF B φ x✝² x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.FinSat.eqFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 3 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 3 × Fin (finsatDim B φ))

The positive equality literals.

Equations

• DescriptiveComplexity.FinSat.eqFml B φ t = DescriptiveComplexity.FinSat.canonG B φ t ⊓ DescriptiveComplexity.FinSat.eqBodyF B φ (t 0) (t 1) (t 2)

noncomputable def DescriptiveComplexity.FinSat.neqBodyF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → FTag B φ → (L.sum FirstOrder.Language.order).Formula (Fin 3 × Fin (finsatDim B φ))

The negative equality literals, as a named function of the three tags: those of the kernel, those of a negatively translated atom, and the distinctness literals of the diagram.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.neqBodyF B φ x✝² x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.FinSat.neqFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 3 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 3 × Fin (finsatDim B φ))

The negative equality literals.

Equations

• DescriptiveComplexity.FinSat.neqFml B φ t = DescriptiveComplexity.FinSat.canonG B φ t ⊓ DescriptiveComplexity.FinSat.neqBodyF B φ (t 0) (t 1) (t 2)

def DescriptiveComplexity.FinSat.atomTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (pol : Bool) : FTag B φ → FTag B φ → Prop

The tags of an atom of a relation variable at a polarity: a node of the kernel carrying a block atom, and the symbol of its relation variable.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.atomTag B φ pol x✝¹ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.posFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The positive atoms of the relation variables: the only genuine atoms of the encoded sentence.

Equations

• DescriptiveComplexity.FinSat.posFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.atomTag B φ true (t 0) (t 1))

noncomputable def DescriptiveComplexity.FinSat.negFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The negated atoms of the relation variables.

Equations

• DescriptiveComplexity.FinSat.negFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.atomTag B φ false (t 0) (t 1))

def DescriptiveComplexity.FinSat.argTagLevel {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → Option ℕ

The de Bruijn level the argument of an atom at a given position takes, read off the tags of the node and of the argument position.

Equations

• DescriptiveComplexity.FinSat.argTagLevel B φ (DescriptiveComplexity.FinSat.Tag.nd p pol) (DescriptiveComplexity.FinSat.Tag.apos j) = DescriptiveComplexity.FinSat.blockArg B φ p ↑j
• DescriptiveComplexity.FinSat.argTagLevel B φ x✝¹ x✝ = none

def DescriptiveComplexity.FinSat.argTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t t' : FTag B φ) : FTag B φ → Prop

The tags of an argument of an atom: the node, an argument position, and the variable of the de Bruijn level the corresponding term takes there.

Equations

• DescriptiveComplexity.FinSat.argTag B φ t t' (DescriptiveComplexity.FinSat.Tag.dbvar l) = (DescriptiveComplexity.FinSat.argTagLevel B φ t t' = some ↑l)
• DescriptiveComplexity.FinSat.argTag B φ t t' x✝ = False

noncomputable def DescriptiveComplexity.FinSat.argFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 3 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 3 × Fin (finsatDim B φ))

The arguments of such an atom: at each argument position, the variable of the de Bruijn level of the corresponding term.

Equations

• DescriptiveComplexity.FinSat.argFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.argTag B φ (t 0) (t 1) (t 2))

def DescriptiveComplexity.FinSat.sigTag {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → FTag B φ → Prop

The tags of an argument position of a relation symbol: the symbol of a relation variable, and a position below its arity.

Equations

• DescriptiveComplexity.FinSat.sigTag B φ (DescriptiveComplexity.FinSat.Tag.sym i) (DescriptiveComplexity.FinSat.Tag.apos j) = (↑j < B.arity i)
• DescriptiveComplexity.FinSat.sigTag B φ x✝¹ x✝ = False

noncomputable def DescriptiveComplexity.FinSat.sigFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 2 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (finsatDim B φ))

The signature of the relation symbols: one argument position per argument of the relation variable.

Equations

• DescriptiveComplexity.FinSat.sigFml B φ t = DescriptiveComplexity.FinSat.tagF B φ t (DescriptiveComplexity.FinSat.sigTag B φ (t 0) (t 1))

noncomputable def DescriptiveComplexity.FinSat.rootBodyF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FTag B φ → (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The root of the encoded sentence, as a named function of the tag: the prefix node of the least element of the instance, the outermost existential.

Equations

• DescriptiveComplexity.FinSat.rootBodyF B φ DescriptiveComplexity.FinSat.Tag.pre = DescriptiveComplexity.minF (0, DescriptiveComplexity.FinSat.c0 B φ)
• DescriptiveComplexity.FinSat.rootBodyF B φ x✝ = ⊥

noncomputable def DescriptiveComplexity.FinSat.rootFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) (t : Fin 1 → FTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (finsatDim B φ))

The root of the encoded sentence.

Equations

• DescriptiveComplexity.FinSat.rootFml B φ t = DescriptiveComplexity.FinSat.canonG B φ t ⊓ DescriptiveComplexity.FinSat.rootBodyF B φ (t 0)

noncomputable def DescriptiveComplexity.FinSat.finsatInterp {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.finsat (FTag B φ) (finsatDim B φ)

The interpretation: the encoded sentence σ_A, defined inside an ordered input structure.

Equations

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

The order of the image

The four order axioms of DescriptiveComplexity.FinSat.IsWF, which is what the image has to satisfy before it is an encoded sentence at all. Nothing else in this section depends on the shape of the kernel: the order is the lexicographic product of the tag key with the tuples, and is linear because both are.

def DescriptiveComplexity.FinSat.tupLe {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] (t : FTag B φ) (u v : Fin (finsatDim B φ) → A) : Prop

The tuple comparison the order uses inside one tag, as a relation: the lexicographic order, reversed inside the prefix.

Equations

• DescriptiveComplexity.FinSat.tupLe B φ DescriptiveComplexity.FinSat.Tag.pre u v = (toLex v ≤ toLex u)
• DescriptiveComplexity.FinSat.tupLe B φ t u v = (toLex u ≤ toLex v)

theorem DescriptiveComplexity.FinSat.tupLe_refl {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] (t : FTag B φ) (u : Fin (finsatDim B φ) → A) : tupLe B φ t u u

theorem DescriptiveComplexity.FinSat.tupLe_total {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] (t : FTag B φ) (u v : Fin (finsatDim B φ) → A) : tupLe B φ t u v ∨ tupLe B φ t v u

theorem DescriptiveComplexity.FinSat.tupLe_antisymm {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {t : FTag B φ} {u v : Fin (finsatDim B φ) → A} (h₁ : tupLe B φ t u v) (h₂ : tupLe B φ t v u) : u = v

theorem DescriptiveComplexity.FinSat.tupLe_trans {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {t : FTag B φ} {u v w : Fin (finsatDim B φ) → A} (h₁ : tupLe B φ t u v) (h₂ : tupLe B φ t v w) : tupLe B φ t u w

theorem DescriptiveComplexity.FinSat.realize_tupLeF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (tupLeF B φ t).Realize v ↔ tupLe B φ t (fun (j : Fin (finsatDim B φ)) => v (0, j)) fun (j : Fin (finsatDim B φ)) => v (1, j)

theorem DescriptiveComplexity.FinSat.tag_eq_of_fkey_eq {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' : FTag B φ} (h : fkey B φ t = fkey B φ t') : t = t'

Tags are determined by their key.

theorem DescriptiveComplexity.FinSat.realize_leFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (leFml B φ t).Realize v ↔ fkey B φ (t 0) < fkey B φ (t 1) ∨ fkey B φ (t 0) = fkey B φ (t 1) ∧ tupLe B φ (t 0) (fun (j : Fin (finsatDim B φ)) => v (0, j)) fun (j : Fin (finsatDim B φ)) => v (1, j)

Reading the order formula: the tags by their key, and within one tag the tuples by DescriptiveComplexity.FinSat.tupLe. Stated at the raw type of tagged tuples – FOInterpretation.Map is a non-reducible definition, so a rewrite inside it is ill-typed at matching transparency.

theorem DescriptiveComplexity.FinSat.ord_map_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x y : (finsatInterp B φ).Map A) : Ord x y ↔ fkey B φ x.1 < fkey B φ y.1 ∨ fkey B φ x.1 = fkey B φ y.1 ∧ tupLe B φ x.1 x.2 y.2

The order of the syntax on the image.

The first four fields of DescriptiveComplexity.FinSat.IsWF: the image is linearly ordered, being the lexicographic product of the tag key with the tuples.

theorem DescriptiveComplexity.FinSat.ord_map_refl {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x : (finsatInterp B φ).Map A) : Ord x x

theorem DescriptiveComplexity.FinSat.ord_map_total {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x y : (finsatInterp B φ).Map A) : Ord x y ∨ Ord y x

theorem DescriptiveComplexity.FinSat.ord_map_antisymm {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x y : (finsatInterp B φ).Map A) (h₁ : Ord x y) (h₂ : Ord y x) : x = y

theorem DescriptiveComplexity.FinSat.ord_map_trans {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x y z : (finsatInterp B φ).Map A) (h₁ : Ord x y) (h₂ : Ord y z) : Ord x z

Canonicity, and the shape of an atom

A tag uses only its first DescriptiveComplexity.FinSat.tagDim coordinates, so the tuple of a tag of dimension zero – a node, a symbol, an argument position, a de Bruijn variable – is forced to be all minima, hence unique. That is what makes the shape conditions of DescriptiveComplexity.FinSat.IsWF hold on the image: the objects those conditions compare are determined by their tags.

theorem DescriptiveComplexity.FinSat.eq_of_canon_zero {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [LinearOrder A] {u v : Fin (finsatDim B φ) → A} (hu : Canon 0 u) (hv : Canon 0 v) : u = v

Two tuples all of whose coordinates are minima are equal.

theorem DescriptiveComplexity.FinSat.realize_canonG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (t : Fin n → FTag B φ) (v : Fin n × Fin (finsatDim B φ) → A) : (canonG B φ t).Realize v ↔ ∀ (i : Fin n), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)

theorem DescriptiveComplexity.FinSat.realize_canonInf {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (t : Fin n → FTag B φ) (F : (L.sum FirstOrder.Language.order).Formula (Fin n × Fin (finsatDim B φ))) (v : Fin n × Fin (finsatDim B φ) → A) : (canonG B φ t ⊓ F).Realize v ↔ (∀ (i : Fin n), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ F.Realize v

The realization of a defining formula that carries a formula of the input structure: canonicity, and that formula.

theorem DescriptiveComplexity.FinSat.realize_tagF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (t : Fin n → FTag B φ) (P : Prop) (v : Fin n × Fin (finsatDim B φ) → A) : (tagF B φ t P).Realize v ↔ (∀ (i : Fin n), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ P

The realization of a defining formula decided by the tags – one lemma for the eight relations that are, each of whose uses then cases only on the tags it needs.

theorem DescriptiveComplexity.FinSat.realize_andFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 1 → FTag B φ) (v : Fin 1 × Fin (finsatDim B φ) → A) : (andFml B φ t).Realize v ↔ (∀ (i : Fin 1), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ andTag B φ (t 0)

theorem DescriptiveComplexity.FinSat.realize_orFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 1 → FTag B φ) (v : Fin 1 × Fin (finsatDim B φ) → A) : (orFml B φ t).Realize v ↔ (∀ (i : Fin 1), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ orTag B φ (t 0)

theorem DescriptiveComplexity.FinSat.realize_allFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 1 → FTag B φ) (v : Fin 1 × Fin (finsatDim B φ) → A) : (allFml B φ t).Realize v ↔ (∀ (i : Fin 1), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ allTag B φ (t 0)

theorem DescriptiveComplexity.FinSat.realize_exFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 1 → FTag B φ) (v : Fin 1 × Fin (finsatDim B φ) → A) : (exFml B φ t).Realize v ↔ (∀ (i : Fin 1), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ exTag B φ (t 0)

theorem DescriptiveComplexity.FinSat.realize_bindFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (bindFml B φ t).Realize v ↔ (∀ (i : Fin 2), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ (bindBodyF B φ (t 0) (t 1)).Realize v

theorem DescriptiveComplexity.FinSat.realize_eqFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 3 → FTag B φ) (v : Fin 3 × Fin (finsatDim B φ) → A) : (eqFml B φ t).Realize v ↔ (∀ (i : Fin 3), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ (eqBodyF B φ (t 0) (t 1) (t 2)).Realize v

theorem DescriptiveComplexity.FinSat.realize_neqFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 3 → FTag B φ) (v : Fin 3 × Fin (finsatDim B φ) → A) : (neqFml B φ t).Realize v ↔ (∀ (i : Fin 3), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ (neqBodyF B φ (t 0) (t 1) (t 2)).Realize v

theorem DescriptiveComplexity.FinSat.realize_rootFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 1 → FTag B φ) (v : Fin 1 × Fin (finsatDim B φ) → A) : (rootFml B φ t).Realize v ↔ (∀ (i : Fin 1), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ (rootBodyF B φ (t 0)).Realize v

theorem DescriptiveComplexity.FinSat.realize_posFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (posFml B φ t).Realize v ↔ (∀ (i : Fin 2), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ atomTag B φ true (t 0) (t 1)

theorem DescriptiveComplexity.FinSat.realize_negFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (negFml B φ t).Realize v ↔ (∀ (i : Fin 2), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ atomTag B φ false (t 0) (t 1)

theorem DescriptiveComplexity.FinSat.atomTag_unique {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {pol pol' : Bool} {t t₁ t₂ : FTag B φ} (h₁ : atomTag B φ pol t t₁) (h₂ : atomTag B φ pol' t t₂) : t₁ = t₂ ∧ tagDim B φ t₁ = 0

An atom's symbol tag is determined by its node tag – so an atom of the image carries at most one relation symbol.

theorem DescriptiveComplexity.FinSat.atomTag_cases {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {pol : Bool} {t t' : FTag B φ} (h : atomTag B φ pol t t') : ∃ (p : Pos B φ) (i : B.ι), t = Tag.nd p pol ∧ t' = Tag.sym i ∧ blockSym B φ p = some i

The tags of an atom of a relation variable, read out: a node carrying a block atom of the kernel, and the symbol of that block variable.

theorem DescriptiveComplexity.FinSat.atomTag_dims {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {pol : Bool} {t t' : FTag B φ} (h : atomTag B φ pol t t') : tagDim B φ t = 0 ∧ tagDim B φ t' = 0

Both tags of an atom use no coordinate: their tuples are all minima.

theorem DescriptiveComplexity.FinSat.realize_argFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 3 → FTag B φ) (v : Fin 3 × Fin (finsatDim B φ) → A) : (argFml B φ t).Realize v ↔ (∀ (i : Fin 3), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ argTag B φ (t 0) (t 1) (t 2)

theorem DescriptiveComplexity.FinSat.argTag_unique {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' t₁ t₂ : FTag B φ} (h₁ : argTag B φ t t' t₁) (h₂ : argTag B φ t t' t₂) : t₁ = t₂ ∧ tagDim B φ t₁ = 0

An argument of an atom of the image is determined by the node and the argument position – so an atom has at most one argument at each position.

theorem DescriptiveComplexity.FinSat.argTag_cases {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' t₁ : FTag B φ} (h : argTag B φ t t' t₁) : ∃ (pos : Pos B φ) (pol : Bool) (j : Fin (finsatDim B φ)) (l : Fin (Tseitin.maxCtx φ)), t = Tag.nd pos pol ∧ t' = Tag.apos j ∧ t₁ = Tag.dbvar l ∧ blockArg B φ pos ↑j = some ↑l

The tags of an argument of an atom, read out: the node, the argument position and the variable are each of their own kind, and the de Bruijn level is the one the term at that position takes.

theorem DescriptiveComplexity.FinSat.argTag_dims {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' t₁ : FTag B φ} (h : argTag B φ t t' t₁) : tagDim B φ t = 0 ∧ tagDim B φ t' = 0 ∧ tagDim B φ t₁ = 0

All three tags of an argument use no coordinate.

theorem DescriptiveComplexity.FinSat.sigTag_cases {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' : FTag B φ} (h : sigTag B φ t t') : ∃ (i : B.ι) (j : Fin (finsatDim B φ)), t = Tag.sym i ∧ t' = Tag.apos j ∧ ↑j < B.arity i

The tags of an argument position of a relation symbol, read out.

theorem DescriptiveComplexity.FinSat.sigTag_dims {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {t t' : FTag B φ} (h : sigTag B φ t t') : tagDim B φ t = 0 ∧ tagDim B φ t' = 0

Both tags of a signature entry use no coordinate.

The shape conditions, read on the image

The bridge from DescriptiveComplexity.FinSat.PosG and its companions to the tag predicates: FOInterpretation.Map is not reducible, so the arguments of the realization lemma have to be supplied explicitly – unification will not find them – and the tuple of a tag of dimension zero is extracted at the index it sits at.

theorem DescriptiveComplexity.FinSat.shape_of_posG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g s : (finsatInterp B φ).Map A) (h : PosG g s) : Canon 0 g.2 ∧ Canon 0 s.2 ∧ atomTag B φ true g.1 s.1

theorem DescriptiveComplexity.FinSat.shape_of_negG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g s : (finsatInterp B φ).Map A) (h : NegG g s) : Canon 0 g.2 ∧ Canon 0 s.2 ∧ atomTag B φ false g.1 s.1

theorem DescriptiveComplexity.FinSat.shape_of_posOrNeg {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g s : (finsatInterp B φ).Map A) (h : PosG g s ∨ NegG g s) : ∃ (pol : Bool), Canon 0 g.2 ∧ Canon 0 s.2 ∧ atomTag B φ pol g.1 s.1

theorem DescriptiveComplexity.FinSat.shape_of_argG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g p x : (finsatInterp B φ).Map A) (h : ArgG g p x) : Canon 0 g.2 ∧ Canon 0 p.2 ∧ Canon 0 x.2 ∧ argTag B φ g.1 p.1 x.1

theorem DescriptiveComplexity.FinSat.argG_of {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g p x : (finsatInterp B φ).Map A) (hg : Canon (tagDim B φ g.1) g.2) (hp : Canon (tagDim B φ p.1) p.2) (hx : Canon (tagDim B φ x.1) x.2) (h : argTag B φ g.1 p.1 x.1) : ArgG g p x

Building an argument relation of the image: the tags say what the argument is, and the tuples only have to be canonically padded.

theorem DescriptiveComplexity.FinSat.realize_sigFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (sigFml B φ t).Realize v ↔ (∀ (i : Fin 2), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ sigTag B φ (t 0) (t 1)

theorem DescriptiveComplexity.FinSat.shape_of_sigG {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (s p : (finsatInterp B φ).Map A) (h : SigG s p) : Canon 0 s.2 ∧ Canon 0 p.2 ∧ sigTag B φ s.1 p.1

Building a relation of the image, rather than reading one: the tags say what holds, and the tuples only have to be canonically padded. This is the direction DescriptiveComplexity.FinSat.IsWF.arg_sig and DescriptiveComplexity.FinSat.IsWF.arg_tot need.

theorem DescriptiveComplexity.FinSat.sigG_of {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (s p : (finsatInterp B φ).Map A) (hs : Canon (tagDim B φ s.1) s.2) (hp : Canon (tagDim B φ p.1) p.2) (h : sigTag B φ s.1 p.1) : SigG s p

theorem DescriptiveComplexity.FinSat.atom_sym_map {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g s s' : (finsatInterp B φ).Map A) (h : PosG g s ∨ NegG g s) (h' : PosG g s' ∨ NegG g s') : s = s'

An atom of the image carries at most one relation symbol (DescriptiveComplexity.FinSat.IsWF.atom_sym).

theorem DescriptiveComplexity.FinSat.arg_fun_map {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g p x x' : (finsatInterp B φ).Map A) (h : ArgG g p x) (h' : ArgG g p x') : x = x'

An atom of the image has at most one argument at each position (DescriptiveComplexity.FinSat.IsWF.arg_fun).

theorem DescriptiveComplexity.FinSat.arg_sig_map {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (g s p x : (finsatInterp B φ).Map A) (h : PosG g s ∨ NegG g s) (h' : ArgG g p x) : SigG s p

An atom of the image only has arguments at the positions of its symbol's signature (DescriptiveComplexity.FinSat.IsWF.arg_sig): an argument of a block atom sits below the arity of its relation variable.

theorem DescriptiveComplexity.FinSat.arg_tot_map {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] (g s p : (finsatInterp B φ).Map A) (h : PosG g s ∨ NegG g s) (hsig : SigG s p) : ∃ (x : (finsatInterp B φ).Map A), ArgG g p x

An atom of the image has an argument at every position of its symbol's signature (DescriptiveComplexity.FinSat.IsWF.arg_tot): the variable of the de Bruijn level the corresponding term takes, which exists because the source vocabulary is relational – a function symbol would have no level to give (the junk-value hazard).

The parse DAG descends along the order

The last field of DescriptiveComplexity.FinSat.IsWF. Everywhere but inside the existential prefix a child sits in a strictly lower layer of the tag order, so its key is smaller; inside the prefix the two tags are equal and the chain descends because the tuple order is reversed there – which is what the prefix case of DescriptiveComplexity.FinSat.tupLeF is for.

theorem DescriptiveComplexity.FinSat.realize_childFml {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 2 → FTag B φ) (v : Fin 2 × Fin (finsatDim B φ) → A) : (childFml B φ t).Realize v ↔ (∀ (i : Fin 2), Canon (tagDim B φ (t i)) fun (j : Fin (finsatDim B φ)) => v (i, j)) ∧ (childBodyF B φ (t 0) (t 1)).Realize v

theorem DescriptiveComplexity.FinSat.childBody_tags {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] {t t' : FTag B φ} {v : Fin 2 × Fin (finsatDim B φ) → A} (h : (childBodyF B φ t t').Realize v) : v (0, c0 B φ) < v (1, c0 B φ) ∧ t = Tag.pre ∧ t' = Tag.pre ∨ frank B φ t' < frank B φ t

Every child edge descends: a child either sits in a strictly lower layer of the tag order, or the edge is one step of the existential prefix.

theorem DescriptiveComplexity.FinSat.child_lt_map {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) : OrdLt c g

Children come strictly earlier in the order of the syntax (DescriptiveComplexity.FinSat.IsWF.child_lt), so the parse DAG of the image is acyclic.

The kinds of a node of the image

Each of the four kinds, read as a condition on the tag and the tuple: the interface the correctness proof of the reduction works against, and the reason the defining formulas dispatch on named predicates. A junk tuple – one not canonically padded – is a node of no kind at all, so it is read by nothing.

theorem DescriptiveComplexity.FinSat.andG_map_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x : (finsatInterp B φ).Map A) : AndG x ↔ Canon (tagDim B φ x.1) x.2 ∧ andTag B φ x.1

theorem DescriptiveComplexity.FinSat.orG_map_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x : (finsatInterp B φ).Map A) : OrG x ↔ Canon (tagDim B φ x.1) x.2 ∧ orTag B φ x.1

theorem DescriptiveComplexity.FinSat.allG_map_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x : (finsatInterp B φ).Map A) : AllG x ↔ Canon (tagDim B φ x.1) x.2 ∧ allTag B φ x.1

theorem DescriptiveComplexity.FinSat.exG_map_iff {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] (x : (finsatInterp B φ).Map A) : ExG x ↔ Canon (tagDim B φ x.1) x.2 ∧ exTag B φ x.1

theorem DescriptiveComplexity.FinSat.image_isWF {L : FirstOrder.Language} (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [L.IsRelational] [Finite A] [Nonempty A] : IsWF ((finsatInterp B φ).Map A)

The image of the reduction is a well-formed encoded sentence: the order of its syntax is linear, its parse DAG descends along that order, and its atoms carry one relation symbol and exactly one argument at each position of that symbol's signature. This is what makes σ_A an instance of DescriptiveComplexity.FINSAT at all – junk tags are elements no node reads, and well-formedness asks nothing of them.