Relativizing an alternating prefix along an encoding

The quantifiers of a step formula of the EXPSPACE reduction range over the points of an exponential expansion, but the enumeration a wide machine can run – the binary increment of a register – ranges over all the block values of an address, most of which encode no point at all. This file is the bridge: an alternating prefix over a type is the same prefix over any type it embeds into, provided the matrix is gated – each existentially quantified coordinate is required to be an encoding, each universally quantified one is excused when it is not, and the matrix proper is read at the decoded values.

DescriptiveComplexity.Draw.gateMat is the gated matrix and DescriptiveComplexity.Draw.altQuantFrom_gateMat the equivalence. The two absorption lemmas it rests on say what a valuation with a garbage coordinate is worth: a garbage coordinate under an existential polarity kills its subtree (DescriptiveComplexity.Draw.not_altQuantFrom_gateMat_of_bad_ex), one under a universal polarity satisfies it outright (DescriptiveComplexity.Draw.altQuantFrom_gateMat_of_bad_all) – which is exactly the standard relativization (∃x φ)^G = ∃x (G x ∧ φ^G), (∀x φ)^G = ∀x (G x → φ^G), pushed through a prenex prefix in one pass.

Everything is stated for an arbitrary injection with image G, so the same lemma serves the point encodings of the reduction and the singleton encodings of its element loops.

noncomputable def DescriptiveComplexity.Draw.gateMat {α β : Type} [Nonempty α] (e : α → β) (G : β → Prop) {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → α) → Prop) : (Fin n → β) → Prop

The gated matrix: every existentially quantified coordinate must be an encoding, and provided every universally quantified one is too, the matrix is read at the decoded values. Coordinates that are encodings pass their gates whatever their polarity, so a valuation wholly inside the image satisfies the gated matrix exactly when its decoding satisfies the matrix.

Equations

• DescriptiveComplexity.Draw.gateMat e G pol P w = ((∀ (i : Fin n), pol ↑i = true → G (w i)) ∧ ((∀ (i : Fin n), pol ↑i = false → G (w i)) → P fun (i : Fin n) => Function.invFun e (w i)))

theorem DescriptiveComplexity.Draw.update_encode {α β : Type} {e : α → β} {n : ℕ} (v : Fin n → α) (k : Fin n) (a : α) : Function.update (fun (i : Fin n) => e (v i)) k (e a) = fun (i : Fin n) => e (Function.update v k a i)

Updating an encoded valuation at an encoded value is encoding the updated valuation.

theorem DescriptiveComplexity.Draw.not_altQuantFrom_gateMat_of_bad_ex {α β : Type} [Nonempty α] {e : α → β} {G : β → Prop} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → α) → Prop} {i₀ : Fin n} (hpol : pol ↑i₀ = true) {j : ℕ} (hij : ↑i₀ < j) {w : Fin n → β} (hG : ¬G (w i₀)) : ¬altQuantFrom pol (gateMat e G pol P) j w

A garbage coordinate under an existential polarity kills its subtree: if some coordinate already chosen fails its gate and its polarity is existential, no way of playing the remaining prefix satisfies the gated matrix.

theorem DescriptiveComplexity.Draw.altQuantFrom_gateMat_of_bad_all {α β : Type} [Nonempty α] {e : α → β} {G : β → Prop} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → α) → Prop} (hbij : ∀ (b : β), G b ↔ ∃ (a : α), e a = b) {i₀ : Fin n} (hpol : pol ↑i₀ = false) {j : ℕ} (hij : ↑i₀ < j) {w : Fin n → β} (hG : ¬G (w i₀)) (hval : ∀ (i : Fin n), ↑i < j → pol ↑i = true → G (w i)) : altQuantFrom pol (gateMat e G pol P) j w

A garbage coordinate under a universal polarity satisfies its subtree outright, provided every existentially quantified coordinate already chosen is an encoding: the gated matrix's implication is vacuous at every leaf below this valuation.

theorem DescriptiveComplexity.Draw.altQuantFrom_gateMat {α β : Type} [Nonempty α] {e : α → β} {G : β → Prop} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → α) → Prop} (hinj : Function.Injective e) (hbij : ∀ (b : β), G b ↔ ∃ (a : α), e a = b) {j : ℕ} (v : Fin n → α) : (altQuantFrom pol (gateMat e G pol P) j fun (i : Fin n) => e (v i)) ↔ altQuantFrom pol P j v

Relativization along an encoding: an alternating prefix over a type is the same prefix over the encodings, with the gated matrix. This is what moves a step formula's quantifiers from the points of the expansion to the block values a register enumerates.