The guess the forward direction makes

DescriptiveComplexity.SecondOrderNewExpPull reads an assignment of the guessed block as a naming of the points of an exponential expansion. This file goes the other way: given a linear order of the instance and an assignment of the source problem's block over the expansion, it builds the assignment of the guessed block that the sentence asks for, one invented value per assignment of the tagged block, and checks every guard.

The value naming an assignment is fixed by an arbitrary enumeration of the assignments; the meaning variables then say “this tuple of original elements belongs to that value's assignment”, the order variable says “both entries are original and the first is below the second”, and the source problem's variables say “these values name points the certificate relates”. Nothing here is a choice: the guards pin the guess down to exactly this, up to which value gets which assignment.

The guess

noncomputable def DescriptiveComplexity.buildAssign {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) : (pullBlock X C).Assignment (A ⊕ Fin m)

The assignment the forward direction guesses: the order of the instance, one invented value per assignment of the tagged block, and the certificate read at the values naming the points.

Equations

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

What the meaning variables say

theorem DescriptiveComplexity.meaningOfB_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (v : A ⊕ Fin m) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m) : meaningOfB (pullMeanPart (buildAssign σ enum)) i v w ↔ ∃ (k : Fin m) (ts : Fin ((taggedBlock X).arity i) → A), v = Sum.inr k ∧ (∀ (j : Fin ((taggedBlock X).arity i)), w j = Sum.inl (ts j)) ∧ enum k i ts

theorem DescriptiveComplexity.meanAtB_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (k : Fin m) (i : (taggedBlock X).ι) (ts : Fin ((taggedBlock X).arity i) → A) : meanAtB (pullMeanPart (buildAssign σ enum)) k ⟨i, ts⟩ ↔ enum k i ts

theorem DescriptiveComplexity.bijective_meanAtB_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) : Function.Bijective (meanAtB (pullMeanPart (buildAssign σ enum)))

The meaning guards

theorem DescriptiveComplexity.meaningOfB_build_inl {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (k : Fin m) (b : Fin ((taggedBlock X).arity i) → A) : (meaningOfB (pullMeanPart (buildAssign σ enum)) i (Sum.inr k) fun (j : Fin ((taggedBlock X).arity i)) => Sum.inl (b j)) ↔ enum k i b

theorem DescriptiveComplexity.not_meaningOfB_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (v : A ⊕ Fin m) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m) (hnot : ¬∀ (j : Fin ((taggedBlock X).arity i)), IsOld (w j)) : ¬meaningOfB (pullMeanPart (buildAssign σ enum)) i v w

theorem DescriptiveComplexity.build_shaped {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (v : A ⊕ Fin m) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m) (hM : meaningOfB (pullMeanPart (buildAssign σ enum)) i v w) : ¬IsOld v ∧ ∀ (j : Fin ((taggedBlock X).arity i)), IsOld (w j)

A meaning of the built guess relates an invented value to original elements and nothing else.

theorem DescriptiveComplexity.build_empty {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) : ∃ (v : A ⊕ Fin m), ¬IsOld v ∧ ∀ (i : (taggedBlock X).ι) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m), ¬meaningOfB (pullMeanPart (buildAssign σ enum)) i v w

Some invented value of the built guess means the empty assignment.

theorem DescriptiveComplexity.build_inj {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (v u : A ⊕ Fin m) (hv : ¬IsOld v) (hu : ¬IsOld u) (hM : ∀ (i : (taggedBlock X).ι) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m), meaningOfB (pullMeanPart (buildAssign σ enum)) i v w ↔ meaningOfB (pullMeanPart (buildAssign σ enum)) i u w) : v = u

Invented values of the built guess agreeing on every variable are equal.

theorem DescriptiveComplexity.build_flip {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (v : A ⊕ Fin m) (y : Fin ((taggedBlock X).arity i) → A ⊕ Fin m) (hv : ¬IsOld v) (hy : ∀ (j : Fin ((taggedBlock X).arity i)), IsOld (y j)) : ∃ (u : A ⊕ Fin m), ¬IsOld u ∧ (∀ (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m), meaningOfB (pullMeanPart (buildAssign σ enum)) i u w ↔ (meaningOfB (pullMeanPart (buildAssign σ enum)) i v w ↔ ¬∀ (j : Fin ((taggedBlock X).arity i)), w j = y j)) ∧ ∀ (i' : (taggedBlock X).ι), i' ≠ i → ∀ (w : Fin ((taggedBlock X).arity i') → A ⊕ Fin m), meaningOfB (pullMeanPart (buildAssign σ enum)) i' u w ↔ meaningOfB (pullMeanPart (buildAssign σ enum)) i' v w

Flipping one tuple of one variable of the built guess lands on an invented value again, the other variables unchanged.

The order guard

theorem DescriptiveComplexity.build_ord_iff {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (x y : A ⊕ Fin m) : buildAssign σ enum (Sum.inl ()) ![x, y] ↔ ∃ (a : A) (b : A), x = Sum.inl a ∧ y = Sum.inl b ∧ a ≤ b

theorem DescriptiveComplexity.build_le_iff {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) (a b : A) : pullLe (buildAssign σ enum) a b ↔ a ≤ b

theorem DescriptiveComplexity.build_ordGuard {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) : (A ⊕ Fin m) ⊨ extLinearGuard L (guessBlock X C)

The built guess satisfies the order guard.

theorem DescriptiveComplexity.build_meanGuard {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] : (A ⊕ Fin m) ⊨ pullMeanGuard X C

The built guess satisfies the meaning guard.

The naming, the certificate, and the sentence

theorem DescriptiveComplexity.meanAssignEquiv_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] (k : Fin m) : (meanAssignEquiv (pullMeanPart (buildAssign σ enum)) ⋯) k = enum k

theorem DescriptiveComplexity.meanAssignEquiv_symm_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] (α : (taggedBlock X).Assignment A) : (meanAssignEquiv (pullMeanPart (buildAssign σ enum)) ⋯).symm α = enum.symm α

theorem DescriptiveComplexity.pullName_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] (p : X.Map A) : pullName (buildAssign σ enum) ⋯ p = Sum.inr (enum.symm (pointAssign p))

theorem DescriptiveComplexity.pullCert_build {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] : pullCert (buildAssign σ enum) (pullName (buildAssign σ enum) ⋯) = σ

The certificate the built guess carries is the one it was built from.

theorem DescriptiveComplexity.pullSentence_forward {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (σ : C.Assignment (X.Map A)) (enum : Fin m ≃ (taggedBlock X).Assignment A) [Finite A] (φ : (X.E.sum C.lang).Sentence) (hφ : X.Map A ⊨ φ) : (A ⊕ Fin m) ⊨ pullSentence X C φ

The built guess satisfies the sentence: the two guards by construction, and the kernel because the certificate it carries is the given one.

How many values the guess invents

theorem DescriptiveComplexity.card_taggedAssign_le {L : FirstOrder.Language} (X : ExpExpansion L) {A : Type} [Finite A] [Nonempty A] : Nat.card ((taggedBlock X).Assignment A) ≤ 2 ^ (Nat.card (taggedBlock X).ι * Nat.card (Fin (blockArityBound (taggedBlock X)) → A))

The assignments of the tagged block are exponentially many: one variable per index, each a relation of arity at most the block's bound, so an assignment is read off a set of pairs of an index and a tuple of that length.