Meanings for a whole block

DescriptiveComplexity.SecondOrderNewMeans guesses what an invented value means when a point is a single relation. A point of an exponential expansion is an assignment of a whole block: one relation per variable, of that variable's arity. So the guess is a family – one meaning relation per variable i, of arity B.arity i + 1 – and the conditions on it are the same four, taken variable by variable:

• DescriptiveComplexity.meanShapedB – each relates an invented value to original elements and nothing else;
• DescriptiveComplexity.meanInjB – invented values agreeing on every variable are equal;
• DescriptiveComplexity.meanEmptyB – some invented value means the empty assignment;
• DescriptiveComplexity.meanFlipB – flipping one tuple of one variable, and leaving the other variables alone, lands on an invented value again.

An assignment of a block is a set of Σ i, Fin (B.arity i) → A – a tuple tagged by the variable it belongs to – so the flips of that single sigma type are exactly the flips of one tuple of one variable, and DescriptiveComplexity.bijective_meanAtB reads the four guards as a bijection between the invented values and all assignments of the block, through the counting of DescriptiveComplexity.SecondOrderNewCount.

The block of meanings and its atoms

@[reducible, inline]

abbrev DescriptiveComplexity.meanBlockB (B : SOBlock) : SOBlock

The block guessing the meanings of a whole block: one relation per variable, of one more argument than that variable.

Equations

• DescriptiveComplexity.meanBlockB B = { ι := B.ι, ιFinite := ⋯, arity := fun (i : B.ι) => B.arity i + 1 }

def DescriptiveComplexity.meanSymB (B : SOBlock) (i : B.ι) : (meanBlockB B).lang.Relations (B.arity i + 1)

The meaning relation of one variable, as a symbol.

Equations

• DescriptiveComplexity.meanSymB B i = ⟨i, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.meanHostB (L : FirstOrder.Language) (B : SOBlock) : FirstOrder.Language

The vocabulary a block-meaning guess is written in.

Equations

• DescriptiveComplexity.meanHostB L B = (DescriptiveComplexity.newLang L).sum (DescriptiveComplexity.meanBlockB B).lang

noncomputable def DescriptiveComplexity.oldAtomB (L : FirstOrder.Language) (B : SOBlock) {α : Type} (x : α) : (meanHostB L B).Formula α

The atom old x, over the block-meaning vocabulary.

Equations

• DescriptiveComplexity.oldAtomB L B x = FirstOrder.Language.Relations.formula (Sum.inl (Sum.inr FirstOrder.Language.oldSym)) fun (x_1 : Fin 1) => FirstOrder.Language.var x

noncomputable def DescriptiveComplexity.meanAtomB (L : FirstOrder.Language) (B : SOBlock) (i : B.ι) {α : Type} (v : α) (w : Fin (B.arity i) → α) : (meanHostB L B).Formula α

The atom Mᵢ v x⃗.

Equations

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

The four guards

noncomputable def DescriptiveComplexity.meanShapedB (L : FirstOrder.Language) (B : SOBlock) : (meanHostB L B).Sentence

Each meaning relation is shaped: it relates an invented value to original elements, and nothing else.

Equations

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

noncomputable def DescriptiveComplexity.meanEmptyB (L : FirstOrder.Language) (B : SOBlock) : (meanHostB L B).Sentence

Some invented value means the empty assignment.

Equations

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

noncomputable def DescriptiveComplexity.meanInjB (L : FirstOrder.Language) (B : SOBlock) : (meanHostB L B).Sentence

Invented values agreeing on every variable are equal.

Equations

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

noncomputable def DescriptiveComplexity.meanFlipB (L : FirstOrder.Language) (B : SOBlock) : (meanHostB L B).Sentence

Flipping one tuple of one variable lands on an invented value again, the other variables unchanged. This is what makes the guess onto.

Equations

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

noncomputable def DescriptiveComplexity.meanGuardB (L : FirstOrder.Language) (B : SOBlock) : (meanHostB L B).Sentence

The whole guard: the four conditions together.

Equations

• DescriptiveComplexity.meanGuardB L B = DescriptiveComplexity.meanShapedB L B ⊓ DescriptiveComplexity.meanEmptyB L B ⊓ DescriptiveComplexity.meanInjB L B ⊓ DescriptiveComplexity.meanFlipB L B

Assignments, as sets of tagged tuples

def DescriptiveComplexity.SOBlock.assignEquivSigma (B : SOBlock) (A : Type) : B.Assignment A ≃ ((i : B.ι) × (Fin (B.arity i) → A) → Prop)

An assignment of a block is a set of tagged tuples: one tuple of the right arity per variable, tagged by the variable it belongs to. This is the shape the flips of DescriptiveComplexity.SecondOrderNewCount are stated at, and it is what makes flipping one tuple of one variable a flip of a single element.

Equations

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

def DescriptiveComplexity.consAssignEquiv (B C : SOBlock) (A : Type) : (B.cons C).Assignment A ≃ B.Assignment A × C.Assignment A

Splitting an assignment of a merged block.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.tagBits (T : Type) [Finite T] : SOBlock

The block of tag bits: one nullary variable per tag, so that an assignment of it is a set of tags. Adding it to a block is how an invented value carries a tag without any machinery of its own – a nullary variable's meaning relation is unary, M v, read as “the value v carries this tag”.

Equations

• DescriptiveComplexity.tagBits T = { ι := T, ιFinite := inst✝, arity := fun (x : T) => 0 }

def DescriptiveComplexity.tagBitsEquiv (T : Type) [Finite T] (A : Type) : (tagBits T).Assignment A ≃ (T → Prop)

An assignment of the tag bits is a set of tags.

Equations

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

def DescriptiveComplexity.consTagAssignEquiv (B : SOBlock) (T : Type) [Finite T] (A : Type) : (B.cons (tagBits T)).Assignment A ≃ B.Assignment A × (T → Prop)

With tag bits added, an assignment is a point's data: the block's own assignment paired with a set of tags. An invented value stands for a point of the expansion exactly when its tag set is a singleton and its assignment satisfies that tag's domain sentence – both conditions the kernel can state, so neither needs a guard of its own.

Equations

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

The guards, realized

def DescriptiveComplexity.meaningOfB {B : SOBlock} {A : Type} {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) (i : B.ι) (v : A ⊕ Fin m) (w : Fin (B.arity i) → A ⊕ Fin m) : Prop

What an element means at one variable, read off the guess.

Equations

• DescriptiveComplexity.meaningOfB ρ i v w = ρ i fun (i_1 : Fin (B.arity i + 1)) => Fin.cases v w i_1

def DescriptiveComplexity.meanAtB {B : SOBlock} {A : Type} {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) (k : Fin m) : (i : B.ι) × (Fin (B.arity i) → A) → Prop

The assignment an invented value means, as a set of tuples tagged by the variable they belong to.

Equations

• DescriptiveComplexity.meanAtB ρ k p = DescriptiveComplexity.meaningOfB ρ p.fst (Sum.inr k) fun (j : Fin (B.arity p.fst)) => Sum.inl (p.snd j)

@[instance_reducible]

noncomputable def DescriptiveComplexity.meanStrucB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) : (meanHostB L B).Structure (A ⊕ Fin m)

The host structure: the extended structure expanded by the guess.

Equations

• DescriptiveComplexity.meanStrucB ρ = (DescriptiveComplexity.newLang L).sumStructure (DescriptiveComplexity.meanBlockB B).lang (A ⊕ Fin m)

theorem DescriptiveComplexity.realize_oldAtomB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) {α : Type} (x : α) (v : α → A ⊕ Fin m) : (oldAtomB L B x).Realize v ↔ IsOld (v x)

theorem DescriptiveComplexity.realize_meanAtomB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) (i : B.ι) {α : Type} (x : α) (w : Fin (B.arity i) → α) (v : α → A ⊕ Fin m) : (meanAtomB L B i x w).Realize v ↔ meaningOfB ρ i (v x) fun (j : Fin (B.arity i)) => v (w j)

theorem DescriptiveComplexity.realize_meanShapedB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanShapedB L B ↔ ∀ (i : B.ι) (v : A ⊕ Fin m) (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i v w → ¬IsOld v ∧ ∀ (j : Fin (B.arity i)), IsOld (w j)

theorem DescriptiveComplexity.realize_meanEmptyB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanEmptyB L B ↔ ∃ (v : A ⊕ Fin m), ¬IsOld v ∧ ∀ (i : B.ι) (w : Fin (B.arity i) → A ⊕ Fin m), ¬meaningOfB ρ i v w

theorem DescriptiveComplexity.realize_meanInjB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanInjB L B ↔ ∀ (v u : A ⊕ Fin m), ¬IsOld v → ¬IsOld u → (∀ (i : B.ι) (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i v w ↔ meaningOfB ρ i u w) → v = u

theorem DescriptiveComplexity.realize_meanFlipB {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ meanFlipB L B ↔ ∀ (i : B.ι) (v : A ⊕ Fin m) (y : Fin (B.arity i) → A ⊕ Fin m), ¬IsOld v → (∀ (j : Fin (B.arity i)), IsOld (y j)) → ∃ (u : A ⊕ Fin m), ¬IsOld u ∧ (∀ (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i u w ↔ (meaningOfB ρ i v w ↔ ¬∀ (j : Fin (B.arity i)), w j = y j)) ∧ ∀ (i' : B.ι), i' ≠ i → ∀ (w : Fin (B.arity i') → A ⊕ Fin m), meaningOfB ρ i' u w ↔ meaningOfB ρ i' v w

theorem DescriptiveComplexity.bijective_meanAtB {B : SOBlock} {A : Type} {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) [Finite A] (hshaped : ∀ (i : B.ι) (v : A ⊕ Fin m) (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i v w → ¬IsOld v ∧ ∀ (j : Fin (B.arity i)), IsOld (w j)) (hempty : ∃ (v : A ⊕ Fin m), ¬IsOld v ∧ ∀ (i : B.ι) (w : Fin (B.arity i) → A ⊕ Fin m), ¬meaningOfB ρ i v w) (hinj : ∀ (v u : A ⊕ Fin m), ¬IsOld v → ¬IsOld u → (∀ (i : B.ι) (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i v w ↔ meaningOfB ρ i u w) → v = u) (hflip : ∀ (i : B.ι) (v : A ⊕ Fin m) (y : Fin (B.arity i) → A ⊕ Fin m), ¬IsOld v → (∀ (j : Fin (B.arity i)), IsOld (y j)) → ∃ (u : A ⊕ Fin m), ¬IsOld u ∧ (∀ (w : Fin (B.arity i) → A ⊕ Fin m), meaningOfB ρ i u w ↔ (meaningOfB ρ i v w ↔ ¬∀ (j : Fin (B.arity i)), w j = y j)) ∧ ∀ (i' : B.ι), i' ≠ i → ∀ (w : Fin (B.arity i') → A ⊕ Fin m), meaningOfB ρ i' u w ↔ meaningOfB ρ i' v w) : Function.Bijective (meanAtB ρ)

The four guards make the meanings a bijection: the invented values name every assignment of the block, each exactly once.

theorem DescriptiveComplexity.bijective_meanAtB_of_guard {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) [Finite A] : (A ⊕ Fin m) ⊨ meanGuardB L B → Function.Bijective (meanAtB ρ)

The whole guard, and what it buys: the invented values name every assignment of the block, each exactly once.

noncomputable def DescriptiveComplexity.meanAssignEquiv {B : SOBlock} {A : Type} {m : ℕ} (ρ : (meanBlockB B).Assignment (A ⊕ Fin m)) [Finite A] (hbij : Function.Bijective (meanAtB ρ)) : Fin m ≃ B.Assignment A

The invented values enumerate the assignments of the block: the guard's bijection, read at assignments rather than at sets of tagged tuples.

Equations

• DescriptiveComplexity.meanAssignEquiv ρ hbij = (Equiv.ofBijective (DescriptiveComplexity.meanAtB ρ) hbij).trans (B.assignEquivSigma A).symm