Padding a prefix normal form

DescriptiveComplexity.Draw.exists_prenexPack puts every formula into the prefix normal form the program's control is built from, but it puts it in the shortest one: a quantifier-free sentence gets a pack with no levels at all. The reduction cannot live with that – its address blocks are Fin ko ⊕ₗ Fin ki, and a step definition all of whose variables are nullary and all of whose packs are quantifier-free leaves that type empty, which is exactly the hypothesis reaches_mainB spends. So the packs are padded rather than cased on.

Padding is one vacuous innermost level: the matrix is lifted past a new bound variable it does not mention, and the prefix walks one step further. The whole content is DescriptiveComplexity.Draw.altQuantFrom_liftLast – a prefix over a predicate that ignores its last coordinate is the prefix without it – whose Nonempty hypothesis is what makes the new level vacuous in both polarities.

A vacuous innermost level

theorem DescriptiveComplexity.Draw.altQuantFrom_liftLast {A : Type} [Nonempty A] {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} (r j : ℕ) : n ≤ j + r → ∀ (v : Fin (n + 1) → A), altQuantFrom pol (fun (w : Fin (n + 1) → A) => P (w ∘ Fin.castSucc)) j v ↔ altQuantFrom pol P j (v ∘ Fin.castSucc)

A prefix over a predicate that ignores its last coordinate is the prefix without it. The new level is vacuous whichever polarity it is given, the universe being nonempty.

One more level

noncomputable def DescriptiveComplexity.Draw.PrenexPack.succ {M : FirstOrder.Language} {k : ℕ} {φ : M.Formula (Fin k)} (pk : PrenexPack φ) : PrenexPack φ

A prefix normal form with one more level: the matrix lifted past a new innermost variable it does not mention. Iterating it puts any pack above any level count, which is how the reduction's block index is kept nonempty.

Equations

• pk.succ = { n := pk.n + 1, kLe := ⋯, pol := pk.pol, mat := FirstOrder.Language.BoundedFormula.liftAt 1 pk.n pk.mat, isQF := ⋯, spec := ⋯ }

@[simp]

theorem DescriptiveComplexity.Draw.PrenexPack.succ_n {M : FirstOrder.Language} {k : ℕ} {φ : M.Formula (Fin k)} (pk : PrenexPack φ) : pk.succ.n = pk.n + 1

The padded pack has one more level.

The encoding layout, and the record a source is packed into

noncomputable def DescriptiveComplexity.Draw.encDim {L : FirstOrder.Language} (X : ExpExpansion L) : ℕ

The encoding budget: one coordinate per component of the one-hot code, one per payload position, and nothing else.

Equations

• DescriptiveComplexity.Draw.encDim X = Nat.card (DescriptiveComplexity.Draw.PtCode X) + DescriptiveComplexity.blockArityBound X.B

noncomputable def DescriptiveComplexity.Draw.ptFin {L : FirstOrder.Language} {X : ExpExpansion L} : PtCode X ≃ Fin (Nat.card (PtCode X))

The code components, numbered.

Equations

• DescriptiveComplexity.Draw.ptFin = (Fintype.equivFin (DescriptiveComplexity.Draw.PtCode X)).trans (finCongr ⋯)

noncomputable def DescriptiveComplexity.Draw.stdLayout {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (h : encDim X ≤ dd) : EncLayout (PtCode X) (blockArityBound X.B) dd

The standard layout: the code in the first coordinates, the payload right after it, both read off DescriptiveComplexity.Draw.ptFin.

Equations

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

theorem DescriptiveComplexity.Draw.stdLayout_lt {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (h : encDim X ≤ dd) (j : Fin dd) (hj : (∃ (q : PtCode X), (stdLayout h).cIx q = j) ∨ ∃ (p : Fin (blockArityBound X.B)), (stdLayout h).pIx p = j) : ↑j < encDim X

The layout inhabits the budget: every coordinate it names is below encDim.

noncomputable def DescriptiveComplexity.Draw.Data.ofSource {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) {dd : ℕ} (hdd : encDim X ≤ dd) : Data L

A source packed into a DescriptiveComplexity.Draw.Data: the prenex packs of every formula the program evaluates, each padded by one level so that the block index is nonempty, and the standard layout at a dimension the caller chooses.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ki_pos {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) {dd : ℕ} (hdd : encDim X ≤ dd) : 0 < (ofSource X d hdd).ki

The packed record's block index is nonempty: the output pack was padded.