Reading a structure over its subsets: the address expansion

The construction that puts a problem one exponential up without saying anything about resources: an DescriptiveComplexity.ExpExpansion whose block is a single unary relation variable, so that an assignment is a subset of the instance and the expanded universe is its power set.

It is written once here, for an arbitrary relational vocabulary with a designated binary symbol read as the order on the elements, because two problems of this library are drawn on it – the wide machine (DescriptiveComplexity.Problems.Wide.Expansion) and the wide tiling (DescriptiveComplexity.Problems.Wide.Tiling). What a particular problem supplies is only its tags and the choice of sentence at each symbol; what is here is everything else:

• the block and the two vocabularies a defining sentence may be written in – one copy of the block for a unary symbol, two for a binary one;
• the dictionary between an assignment and the address it is (AddrExp.bits, AddrExp.assign);
• the guards of the base vocabulary, and the atoms of the block;
• and the five sentences an expansion of this shape ever needs: a mark of the base (AddrExp.markS), a binary attribute of it (AddrExp.binS), being a singleton (AddrExp.singleS, the domain sentence that keeps the base universe visible), the binary-number order on addresses (AddrExp.addrLeS) and a relation read at the initial segment an element cuts (AddrExp.inpS).

Every quantifier in them ranges over the base – an element, never an address – which is what keeps them first-order there.

The order on addresses is the binary-number order (DescriptiveComplexity.WMSetLe): one subset is below another when, at the least element where they differ, the second contains it and the first does not. That relation and the initial segment an element cuts (DescriptiveComplexity.WMDown) are stated here for an arbitrary relation on an arbitrary type, since both the problems and their expansions read them.

Addresses

The two things said about an address – how it compares with another, and which initial segment it is – stated for an arbitrary order relation, so that they transport along an equivalence without mentioning a structure.

def DescriptiveComplexity.WMSetLe {α : Type} (Le : α → α → Prop) (s t : α → Prop) : Prop

The binary-number order on addresses: the two subsets agree, or, at some element where the first is out and the second in, they agree at every strictly smaller element. Written with the strict order spelled out as Le y x ∧ ¬ Le x y, which is the shape the defining sentence of the expansion realizes to.

Equations

• DescriptiveComplexity.WMSetLe Le s t = ((∀ (x : α), s x ↔ t x) ∨ ∃ (x : α), (∀ (y : α), Le y x ∧ ¬Le x y → (s y ↔ t y)) ∧ ¬s x ∧ t x)

def DescriptiveComplexity.WMDown {α : Type} (Le : α → α → Prop) (s : α → Prop) (x : α) : Prop

The address of an element: the initial segment it cuts, which is where the element's input symbol is written.

Equations

• DescriptiveComplexity.WMDown Le s x = ∀ (y : α), s y ↔ Le y x

def DescriptiveComplexity.WMFileSeg {α : Type} (Le : α → α → Prop) (Has s : α → Prop) (x : α) : Prop

The cell of an element on a file: the initial segment it cuts among the elements the file has a register for. The wide machine's register channel and the wide tiling's bottom row are both described at these addresses – a file of cells rather than the ruler of all the segments.

Equations

• DescriptiveComplexity.WMFileSeg Le Has s x = ∀ (y : α), s y ↔ Le y x ∧ Has y

theorem DescriptiveComplexity.wmSetLe_congr {α β : Type} (u : α ≃ β) {LeA : α → α → Prop} {LeB : β → β → Prop} (hle : ∀ (x y : α), LeA x y ↔ LeB (u x) (u y)) (s t : α → Prop) : WMSetLe LeA s t ↔ WMSetLe LeB (fun (y : β) => s (u.symm y)) fun (y : β) => t (u.symm y)

The order on addresses transports along an equivalence of the index type.

theorem DescriptiveComplexity.wmDown_congr {α β : Type} (u : α ≃ β) {LeA : α → α → Prop} {LeB : β → β → Prop} (hle : ∀ (x y : α), LeA x y ↔ LeB (u x) (u y)) (s : α → Prop) (x : α) : WMDown LeA s x ↔ WMDown LeB (fun (y : β) => s (u.symm y)) (u x)

The initial segment of an element transports along an equivalence.

The vocabularies

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.aeOrd (L : FirstOrder.Language) : FirstOrder.Language

The ordered vocabulary of wide-machine instances: what an expansion's sentences may read besides the block.

Equations

• DescriptiveComplexity.AddrExp.aeOrd L = L.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.addrBlock : SOBlock

The block whose assignments are the addresses: a single unary relation variable, so an assignment is a subset of the instance.

Equations

• DescriptiveComplexity.AddrExp.addrBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.aeLang1 (L : FirstOrder.Language) : FirstOrder.Language

The base vocabulary expanded by one copy of the block.

Equations

• DescriptiveComplexity.AddrExp.aeLang1 L = (DescriptiveComplexity.AddrExp.aeOrd L).sum DescriptiveComplexity.AddrExp.addrBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.aeLang2 (L : FirstOrder.Language) : FirstOrder.Language

The base vocabulary expanded by two copies of the block.

Equations

• DescriptiveComplexity.AddrExp.aeLang2 L = (DescriptiveComplexity.AddrExp.aeLang1 L).sum DescriptiveComplexity.AddrExp.addrBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.aeSym₁ {L : FirstOrder.Language} (r : L.Relations 1) : (aeOrd L).Relations 1

A unary symbol of the instance, in the ordered vocabulary: a raw Sum.inl does not elaborate at that type.

Equations

• DescriptiveComplexity.AddrExp.aeSym₁ r = Sum.inl r

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.aeSym₂ {L : FirstOrder.Language} (r : L.Relations 2) : (aeOrd L).Relations 2

A binary symbol of the instance, in the ordered vocabulary.

Equations

• DescriptiveComplexity.AddrExp.aeSym₂ r = Sum.inl r

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.bit1 {L : FirstOrder.Language} : (aeLang1 L).Relations 1

The relation variable of the block, at one copy.

Equations

• DescriptiveComplexity.AddrExp.bit1 = Sum.inr ⟨(), DescriptiveComplexity.AddrExp.bit1._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.bitA {L : FirstOrder.Language} : (aeLang2 L).Relations 1

The relation variable of the first of two copies.

Equations

• DescriptiveComplexity.AddrExp.bitA = Sum.inl (Sum.inr ⟨(), DescriptiveComplexity.AddrExp.bit1._proof_1⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.bitB {L : FirstOrder.Language} : (aeLang2 L).Relations 1

The relation variable of the second of two copies.

Equations

• DescriptiveComplexity.AddrExp.bitB = Sum.inr ⟨(), DescriptiveComplexity.AddrExp.bit1._proof_1⟩

Addresses, as assignments of the block

def DescriptiveComplexity.AddrExp.aeBits {A : Type} (ρ : addrBlock.Assignment A) : A → Prop

The address an assignment is: the elements its relation variable holds of.

Equations

• DescriptiveComplexity.AddrExp.aeBits ρ x = ρ () fun (x_1 : Fin (DescriptiveComplexity.AddrExp.addrBlock.arity ())) => x

def DescriptiveComplexity.AddrExp.aeAssign {A : Type} (s : A → Prop) : addrBlock.Assignment A

The assignment an address is, the inverse of DescriptiveComplexity.AddrExp.aeBits.

Equations

• DescriptiveComplexity.AddrExp.aeAssign s x✝ v = s (v 0)

@[simp]

theorem DescriptiveComplexity.AddrExp.aeBits_aeAssign {A : Type} (s : A → Prop) : aeBits (aeAssign s) = s

theorem DescriptiveComplexity.AddrExp.apply₁ {A : Type} (f : (Fin 1 → A) → Prop) (v : Fin 1 → A) : f v ↔ f fun (x : Fin 1) => v 0

A unary relation variable is read at its only argument.

@[simp]

theorem DescriptiveComplexity.AddrExp.aeAssign_aeBits {A : Type} (ρ : addrBlock.Assignment A) : aeAssign (aeBits ρ) = ρ

An assignment of the block is the assignment of its address: the single variable being unary, nothing else is stored.

theorem DescriptiveComplexity.AddrExp.aeAssign_injective {A : Type} : Function.Injective aeBits

Two assignments of the block holding the same address are equal.

The base's own relations, read semantically

def DescriptiveComplexity.AddrExp.aeRel₁ {L : FirstOrder.Language} {A : Type} [L.Structure A] (r : L.Relations 1) (x : A) : Prop

A unary relation of the base, at an element.

Equations

• DescriptiveComplexity.AddrExp.aeRel₁ r x = FirstOrder.Language.Structure.RelMap r ![x]

def DescriptiveComplexity.AddrExp.aeRel₂ {L : FirstOrder.Language} {A : Type} [L.Structure A] (r : L.Relations 2) (x y : A) : Prop

A binary relation of the base, at two elements.

Equations

• DescriptiveComplexity.AddrExp.aeRel₂ r x y = FirstOrder.Language.Structure.RelMap r ![x, y]

The guards of the base vocabulary

noncomputable def DescriptiveComplexity.AddrExp.markG {L : FirstOrder.Language} {γ : Type} (r : L.Relations 1) (x : γ) : (aeOrd L).Formula γ

A unary mark of the instance.

Equations

• DescriptiveComplexity.AddrExp.markG r x = (DescriptiveComplexity.AddrExp.aeSym₁ r).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.AddrExp.attrG {L : FirstOrder.Language} {γ : Type} (r : L.Relations 2) (x y : γ) : (aeOrd L).Formula γ

A binary attribute of the instance.

Equations

• DescriptiveComplexity.AddrExp.attrG r x y = (DescriptiveComplexity.AddrExp.aeSym₂ r).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.AddrExp.eqG {L : FirstOrder.Language} {γ : Type} (x y : γ) : (aeOrd L).Formula γ

x and y are the same element.

Equations

• DescriptiveComplexity.AddrExp.eqG x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.AddrExp.ltG {L : FirstOrder.Language} {γ : Type} (leSym : L.Relations 2) (x y : γ) : (aeOrd L).Formula γ

x is strictly below y in the order the instance carries.

Equations

• DescriptiveComplexity.AddrExp.ltG leSym x y = DescriptiveComplexity.AddrExp.attrG leSym x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.AddrExp.attrG leSym y x)

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_markG {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (r : L.Relations 1) (x : γ) : (markG r x).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x]

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_attrG {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (r : L.Relations 2) (x y : γ) : (attrG r x y).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x, v y]

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_eqG {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (eqG x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_ltG {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (leSym : L.Relations 2) (x y : γ) : (ltG leSym x y).Realize v ↔ aeRel₂ leSym (v x) (v y) ∧ ¬aeRel₂ leSym (v y) (v x)

The atoms of the block, and the lifts

noncomputable def DescriptiveComplexity.AddrExp.bit1F {L : FirstOrder.Language} {γ : Type} (x : γ) : (aeLang1 L).Formula γ

The address of the single copy holds x.

Equations

• DescriptiveComplexity.AddrExp.bit1F x = DescriptiveComplexity.AddrExp.bit1.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.AddrExp.bitAF {L : FirstOrder.Language} {γ : Type} (x : γ) : (aeLang2 L).Formula γ

The address of the first of two copies holds x.

Equations

• DescriptiveComplexity.AddrExp.bitAF x = DescriptiveComplexity.AddrExp.bitA.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.AddrExp.bitBF {L : FirstOrder.Language} {γ : Type} (x : γ) : (aeLang2 L).Formula γ

The address of the second of two copies holds x.

Equations

• DescriptiveComplexity.AddrExp.bitBF x = DescriptiveComplexity.AddrExp.bitB.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.AddrExp.lift1 {L : FirstOrder.Language} {γ : Type} (φ : (aeOrd L).Formula γ) : (aeLang1 L).Formula γ

A base guard, read at one copy of the block.

Equations

• DescriptiveComplexity.AddrExp.lift1 φ = FirstOrder.Language.LHom.sumInl.onFormula φ

noncomputable def DescriptiveComplexity.AddrExp.lift2 {L : FirstOrder.Language} {γ : Type} (φ : (aeOrd L).Formula γ) : (aeLang2 L).Formula γ

A base guard, read at two copies of the block.

Equations

• DescriptiveComplexity.AddrExp.lift2 φ = FirstOrder.Language.LHom.sumInl.onFormula (FirstOrder.Language.LHom.sumInl.onFormula φ)

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_bit1F {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (ρ : addrBlock.Assignment A) (x : γ) : (bit1F x).Realize v ↔ aeBits ρ (v x)

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_bitAF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : addrBlock.Assignment A) (x : γ) : (bitAF x).Realize v ↔ aeBits ρ (v x)

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_bitBF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : addrBlock.Assignment A) (x : γ) : (bitBF x).Realize v ↔ aeBits σ (v x)

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_lift1 {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (ρ : addrBlock.Assignment A) (φ : (aeOrd L).Formula γ) : (lift1 φ).Realize v ↔ φ.Realize v

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_lift2 {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : addrBlock.Assignment A) (φ : (aeOrd L).Formula γ) : (lift2 φ).Realize v ↔ φ.Realize v

The five sentences

Everything an expansion of FirstOrder.L has to say, once each.

noncomputable def DescriptiveComplexity.AddrExp.markS {L : FirstOrder.Language} (r : L.Relations 1) : (aeLang1 L).Sentence

A mark of the control: the point is the element x, and x carries the mark r.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.binS {L : FirstOrder.Language} (r : L.Relations 2) : (aeLang2 L).Sentence

A binary attribute of the control: the two points are the elements x and y, and r holds of them.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.singleS {L : FirstOrder.Language} : (aeLang1 L).Sentence

The domain sentence of the control tag: the address is a singleton, so the point is an element of the instance.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.addrLeS {L : FirstOrder.Language} (leSym : L.Relations 2) : (aeLang2 L).Sentence

The order on addresses: the two addresses agree, or, at some element the first is out of and the second in, they agree at every strictly smaller element.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.inpS {L : FirstOrder.Language} (leSym inpSym : L.Relations 2) : (aeLang2 L).Sentence

The initial tape: the first address is the initial segment cut by some element x, the second point is a symbol y, and y is the input at x.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.subsetS {L : FirstOrder.Language} (r : L.Relations 1) : (aeLang1 L).Sentence

The address lies inside a marked part of the instance: every element it holds carries the mark. This is what makes a sub-power-set the universe a problem's grid is indexed by, when the expansion's own universe has to be bigger than the instance to hold the problem's other objects.

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.hasRelG {L : FirstOrder.Language} {γ : Type} (r : L.Relations 2) (x : γ) : (aeOrd L).Formula γ

An element the file has a register for, as a guard: it carries the relation the file is described by.

Equations

• DescriptiveComplexity.AddrExp.hasRelG r x = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.AddrExp.attrG r (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.AddrExp.regS {L : FirstOrder.Language} (leSym inpSym : L.Relations 2) : (aeLang2 L).Sentence

A relation read at the cells of a file: the first address is the segment some element x cuts among the elements carrying inpSym, the second point is a y, and inpSym holds of x and y. This is AddrExp.inpS with the ruler of all the segments replaced by the file.

Equations

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

What the five sentences say

def DescriptiveComplexity.AddrExp.WMSingle {A : Type} (s : A → Prop) : Prop

An address is a singleton: it holds something, and at most one thing.

Equations

• DescriptiveComplexity.AddrExp.WMSingle s = ((∃ (x : A), s x) ∧ ∀ (x y : A), s x → s y → x = y)

theorem DescriptiveComplexity.AddrExp.exists_eq_of_wmSingle {A : Type} {s : A → Prop} (h : WMSingle s) : ∃ (x : A), ∀ (y : A), s y ↔ y = x

A singleton address is the address of an element.

theorem DescriptiveComplexity.AddrExp.wmSingle_eq {A : Type} (x : A) : WMSingle fun (y : A) => y = x

The address of an element is a singleton.

theorem DescriptiveComplexity.AddrExp.realize_topS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (ρ : addrBlock.Assignment A) : A ⊨ ⊤

The trivially true sentence, at one copy of the block.

theorem DescriptiveComplexity.AddrExp.not_realize_botS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (ρ : addrBlock.Assignment A) : ¬A ⊨ ⊥

The trivially false sentence, at one copy of the block.

theorem DescriptiveComplexity.AddrExp.realize_topS₂ {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (ρ σ : addrBlock.Assignment A) : A ⊨ ⊤

The trivially true sentence, at two copies of the block.

theorem DescriptiveComplexity.AddrExp.not_realize_botS₂ {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (ρ σ : addrBlock.Assignment A) : ¬A ⊨ ⊥

The trivially false sentence, at two copies of the block.

theorem DescriptiveComplexity.AddrExp.realize_markS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (r : L.Relations 1) (ρ : addrBlock.Assignment A) : A ⊨ markS r ↔ ∃ (x : A), aeBits ρ x ∧ FirstOrder.Language.Structure.RelMap r ![x]

theorem DescriptiveComplexity.AddrExp.realize_binS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (r : L.Relations 2) (ρ σ : addrBlock.Assignment A) : A ⊨ binS r ↔ ∃ (x : A) (y : A), aeBits ρ x ∧ aeBits σ y ∧ FirstOrder.Language.Structure.RelMap r ![x, y]

theorem DescriptiveComplexity.AddrExp.realize_singleS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (ρ : addrBlock.Assignment A) : A ⊨ singleS ↔ WMSingle (aeBits ρ)

theorem DescriptiveComplexity.AddrExp.realize_addrLeS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (leSym : L.Relations 2) (ρ σ : addrBlock.Assignment A) : A ⊨ addrLeS leSym ↔ WMSetLe (aeRel₂ leSym) (aeBits ρ) (aeBits σ)

theorem DescriptiveComplexity.AddrExp.realize_inpS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (leSym inpSym : L.Relations 2) (ρ σ : addrBlock.Assignment A) : A ⊨ inpS leSym inpSym ↔ ∃ (x : A) (y : A), WMDown (aeRel₂ leSym) (aeBits ρ) x ∧ aeBits σ y ∧ aeRel₂ inpSym x y

@[simp]

theorem DescriptiveComplexity.AddrExp.realize_hasRelG {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (r : L.Relations 2) (x : γ) : (hasRelG r x).Realize v ↔ ∃ (z : A), aeRel₂ r (v x) z

theorem DescriptiveComplexity.AddrExp.realize_subsetS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (r : L.Relations 1) (ρ : addrBlock.Assignment A) : A ⊨ subsetS r ↔ ∀ (x : A), aeBits ρ x → aeRel₁ r x

theorem DescriptiveComplexity.AddrExp.realize_regS {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] (leSym inpSym : L.Relations 2) (ρ σ : addrBlock.Assignment A) : A ⊨ regS leSym inpSym ↔ ∃ (x : A) (y : A), WMFileSeg (aeRel₂ leSym) (fun (z : A) => ∃ (w : A), aeRel₂ inpSym z w) (aeBits ρ) x ∧ aeBits σ y ∧ aeRel₂ inpSym x y

The universe, the tags and the expansion skeleton

@[reducible, inline]

abbrev DescriptiveComplexity.AddrExp.WPoint (A : Type) : Type

The universe a problem at this expansion runs over: the addresses – the subsets of the instance – together with the elements of the instance. An abbrev, so that the sum structure stays visible to rw and to the elaborator.

Equations

• DescriptiveComplexity.AddrExp.WPoint A = ((A → Prop) ⊕ A)

inductive DescriptiveComplexity.AddrExp.WTag : Type

The two tags of the expansion: the addresses, and the elements of the instance.

• addr : WTag

  An address: any assignment of the block.

• ctrl : WTag

  A control element: a singleton assignment of the block.

@[instance_reducible]

instance DescriptiveComplexity.AddrExp.instDecidableEqWTag : DecidableEq WTag

Equations

• DescriptiveComplexity.AddrExp.instDecidableEqWTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.AddrExp.instFintypeWTag : Fintype WTag

Equations

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

noncomputable def DescriptiveComplexity.AddrExp.domT {L : FirstOrder.Language} : WTag → (aeLang1 L).Sentence

The domain sentence of each tag: an address is unrestricted, a control element is a singleton.

Equations

• DescriptiveComplexity.AddrExp.domT DescriptiveComplexity.AddrExp.WTag.addr = ⊤
• DescriptiveComplexity.AddrExp.domT DescriptiveComplexity.AddrExp.WTag.ctrl = DescriptiveComplexity.AddrExp.singleS

noncomputable def DescriptiveComplexity.AddrExp.onS1 {L : FirstOrder.Language} (φ : (aeLang1 L).Sentence) : ((aeOrd L).sum (addrBlock.replicate 1).lang).Sentence

Reading a one-copy sentence inside the block replicated once.

Equations

• DescriptiveComplexity.AddrExp.onS1 φ = (DescriptiveComplexity.SOBlock.oneLHom (DescriptiveComplexity.AddrExp.aeOrd L) DescriptiveComplexity.AddrExp.addrBlock).onSentence φ

noncomputable def DescriptiveComplexity.AddrExp.onS2 {L : FirstOrder.Language} (φ : (aeLang2 L).Sentence) : ((aeOrd L).sum (addrBlock.replicate 2).lang).Sentence

Reading a two-copy sentence inside the block replicated twice.

Equations

• DescriptiveComplexity.AddrExp.onS2 φ = (DescriptiveComplexity.SOBlock.twoLHom (DescriptiveComplexity.AddrExp.aeOrd L) DescriptiveComplexity.AddrExp.addrBlock).onSentence φ

noncomputable def DescriptiveComplexity.AddrExp.addrExp (L E : FirstOrder.Language) [E.IsRelational] (relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence) : ExpExpansion L

The expansion whose points are the subsets of the instance: two tags, the one-variable block, and whatever defining sentences the problem supplies. Everything below is proved of this expansion, so a problem drawn on it has only to say what each of its symbols means.

Equations

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

The universe of the problem is the universe of the expansion

theorem DescriptiveComplexity.AddrExp.domHolds_addr {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : A → Prop) : ExpExpansion.DomHolds (WTag.addr, aeAssign s)

An address satisfies the domain sentence of its tag, which is ⊤.

theorem DescriptiveComplexity.AddrExp.domHolds_ctrl {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (x : A) : ExpExpansion.DomHolds (WTag.ctrl, aeAssign fun (y : A) => y = x)

The singleton address of an element satisfies the domain sentence of the control tag.

noncomputable def DescriptiveComplexity.AddrExp.addrEmbed {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] : WPoint A → (addrExp L E fun {n : ℕ} => relS).Map A

The universe of the problem sits inside the expansion: an address becomes the point tagged addr carrying it, a control element the point tagged ctrl carrying its singleton.

Equations

• DescriptiveComplexity.AddrExp.addrEmbed (Sum.inl s) = ⟨(DescriptiveComplexity.AddrExp.WTag.addr, DescriptiveComplexity.AddrExp.aeAssign s), ⋯⟩
• DescriptiveComplexity.AddrExp.addrEmbed (Sum.inr x_1) = ⟨(DescriptiveComplexity.AddrExp.WTag.ctrl, DescriptiveComplexity.AddrExp.aeAssign fun (y : A) => y = x_1), ⋯⟩

@[simp]

theorem DescriptiveComplexity.AddrExp.addrEmbed_addr_tag {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (s : A → Prop) : (↑(addrEmbed (Sum.inl s))).1 = WTag.addr

@[simp]

theorem DescriptiveComplexity.AddrExp.addrEmbed_ctrl_tag {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (x : A) : (↑(addrEmbed (Sum.inr x))).1 = WTag.ctrl

theorem DescriptiveComplexity.AddrExp.addrEmbed_bijective {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] : Function.Bijective addrEmbed

The embedding is onto the whole expanded universe: every point tagged addr is an address, and every point tagged ctrl is a control element, because its domain sentence made its assignment a singleton.

noncomputable def DescriptiveComplexity.AddrExp.addrEquiv {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] : WPoint A ≃ (addrExp L E fun {n : ℕ} => relS).Map A

The points of the expansion are the universe of the problem.

Equations

• DescriptiveComplexity.AddrExp.addrEquiv = Equiv.ofBijective DescriptiveComplexity.AddrExp.addrEmbed ⋯

@[simp]

theorem DescriptiveComplexity.AddrExp.addrEquiv_apply {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (p : WPoint A) : addrEquiv p = addrEmbed p

Reading a defining sentence at the points

theorem DescriptiveComplexity.AddrExp.realize_onS1 {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (φ : (aeLang1 L).Sentence) (x : (addrExp L E fun {n : ℕ} => relS).Map A) : A ⊨ onS1 φ ↔ A ⊨ φ

Reading a one-copy sentence at a point: the replicated assignment holds the point's address in its single copy.

theorem DescriptiveComplexity.AddrExp.realize_onS2 {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (φ : (aeLang2 L).Sentence) (x y : (addrExp L E fun {n : ℕ} => relS).Map A) : A ⊨ onS2 φ ↔ A ⊨ φ

Reading a two-copy sentence at two points: the replicated assignment holds the first point's address in copy 0 and the second's in copy 1.

@[instance_reducible]

noncomputable def DescriptiveComplexity.AddrExp.addrStructure {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} (A : Type) [L.Structure A] [LinearOrder A] : E.Structure ((addrExp L E fun {n : ℕ} => relS).Map A)

The expanded structure, at the vocabulary the problem is written in – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• DescriptiveComplexity.AddrExp.addrStructure A = (DescriptiveComplexity.AddrExp.addrExp L E fun {n : ℕ} => relS).mapStructure A

theorem DescriptiveComplexity.AddrExp.realize_one {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (rt : E.Relations 1) (φ : WTag → (aeLang1 L).Sentence) (h : ∀ (τ : Fin 1 → WTag), relS rt τ = onS1 (φ (τ 0))) (x : (addrExp L E fun {n : ℕ} => relS).Map A) : FirstOrder.Language.Structure.RelMap rt ![x] ↔ A ⊨ φ (↑x).1

Reading a unary symbol of the expanded vocabulary at one point.

theorem DescriptiveComplexity.AddrExp.realize_two {L E : FirstOrder.Language} [E.IsRelational] {relS : {n : ℕ} → E.Relations n → (Fin n → WTag) → ((aeOrd L).sum (addrBlock.replicate n).lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (rt : E.Relations 2) (φ : WTag → WTag → (aeLang2 L).Sentence) (h : ∀ (τ : Fin 2 → WTag), relS rt τ = onS2 (φ (τ 0) (τ 1))) (x y : (addrExp L E fun {n : ℕ} => relS).Map A) : FirstOrder.Language.Structure.RelMap rt ![x, y] ↔ A ⊨ φ (↑x).1 (↑y).1

Reading a binary symbol of the expanded vocabulary at two points.