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

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

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))

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.