A kernel, packed as the data of a wide program

The source side of the NEXPTIME reduction, in the record the machine layer is already written against. A DescriptiveComplexity.NexKernel is an expansion, a block of relation variables to guess and a first-order sentence to check of the guess; a DescriptiveComplexity.Draw.Data is an expansion, a DescriptiveComplexity.StepDef – a block, a step formula per variable, an output sentence – and the packs and layout the program computes with.

The kernel is a step definition whose steps are never read. Put the guessed block where the fixed-point variables go and the kernel where the output sentence goes, and the two records are the same record: the tracks a symbol carries are indexed by the block either way, the atoms of the sentence classify by DescriptiveComplexity.Draw.MatAtom – which reads a block, not an iteration – and DescriptiveComplexity.Draw.StepDef.out_iff_gateMat is already what the output evaluation of a fixed-point program computes. So the whole address, control and evaluation layer above Draw.Data serves a nondeterministic program with nothing added, and what is new is the program alone: it guesses the tracks the iteration would have written, then runs the output evaluation once.

The step formulas of a packed kernel are ⊥, and the only trace they leave is in the sizes: the derived dimensions of DescriptiveComplexity.Draw.Data are maxima over the variables, so each of them is the kernel's own value or the (vacuous) demand of an unread step, whichever is larger. A larger inventory costs a wider control and nothing else.

def DescriptiveComplexity.NexKernel.toStepDef {L : FirstOrder.Language} (K : NexKernel L) : StepDef (K.X.E.sum FirstOrder.Language.order)

A kernel as a step definition: the guessed block, the kernel as the output sentence, and step formulas that no nondeterministic program reads.

Equations

• K.toStepDef = { B := K.B, step := fun (x : K.B.ι) => ⊥, out := K.ker }

@[simp]

theorem DescriptiveComplexity.NexKernel.toStepDef_B {L : FirstOrder.Language} (K : NexKernel L) : K.toStepDef.B = K.B

@[simp]

theorem DescriptiveComplexity.NexKernel.toStepDef_out {L : FirstOrder.Language} (K : NexKernel L) : K.toStepDef.out = K.ker

noncomputable def DescriptiveComplexity.Draw.Data.ofKernel {L : FirstOrder.Language} (K : NexKernel L) {dd : ℕ} (hdd : encDim K.X ≤ dd) : Data L

A kernel packed into a DescriptiveComplexity.Draw.Data: the same packing as a source's (DescriptiveComplexity.Draw.Data.ofSource), at the step definition the kernel is.

Equations

• DescriptiveComplexity.Draw.Data.ofKernel K hdd = DescriptiveComplexity.Draw.Data.ofSource K.X K.toStepDef hdd

@[simp]

theorem DescriptiveComplexity.Draw.Data.ofKernel_X {L : FirstOrder.Language} (K : NexKernel L) {dd : ℕ} (hdd : encDim K.X ≤ dd) : (ofKernel K hdd).X = K.X

@[simp]

theorem DescriptiveComplexity.Draw.Data.ofKernel_d {L : FirstOrder.Language} (K : NexKernel L) {dd : ℕ} (hdd : encDim K.X ≤ dd) : (ofKernel K hdd).d = K.toStepDef

@[simp]

theorem DescriptiveComplexity.Draw.Data.ofKernel_dd {L : FirstOrder.Language} (K : NexKernel L) {dd : ℕ} (hdd : encDim K.X ≤ dd) : (ofKernel K hdd).dd = dd

What a nondeterministic program has to decide

The evaluation the machine performs, stated where it can be read off the record: the guess of an assignment of the block for which the gated alternating prefix of the output sentence's matrix holds. A fixed-point program computes one such prefix per stage and one for its output; a nondeterministic one computes only the second, over tracks it guessed rather than iterated, so the statement below is DescriptiveComplexity.Draw.StepDef.out_iff_gateMat under an existential and nothing else.

theorem DescriptiveComplexity.Draw.Data.exists_out_iff_gateMat {L : FirstOrder.Language} (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (dt.X.Map A)] (hne : zero ≠ one) (V : Fin dt.pkOut.n → (Fin dt.dd → A) → Prop) : (∃ (σ : dt.d.B.Assignment (dt.X.Map A)), dt.X.Map A ⊨ dt.d.out) ↔ ∃ (σ : dt.d.B.Assignment (dt.X.Map A)), altQuantFrom dt.pkOut.pol (gateMat (encMap dt.ly zero one) (IsEnc dt.ly zero one) dt.pkOut.pol fun (w : Fin dt.pkOut.n → dt.X.Map A) => dt.pkOut.mat.Realize default w) 0 V

The guess-and-check reading of the output sentence: some assignment of the block satisfies it exactly when some assignment passes the gated prefix of its matrix. This is the last statement of the source side that mentions no machine.

theorem DescriptiveComplexity.Draw.NexKernel.holds_iff_structure₁ {L : FirstOrder.Language} (K : NexKernel L) {M : Type} [K.X.E.Structure M] [LinearOrder M] : K.Holds M ↔ ∃ (σ : K.B.Assignment M), M ⊨ K.ker

The kernel, read as a packed record's output sentence. The two sides are the same proposition: DescriptiveComplexity.NexKernel.Holds names the expanded structure by DescriptiveComplexity.SOBlock.structure, and a packed record's output evaluation names it by DescriptiveComplexity.SOBlock.structure₁, which is that structure summed with the base's. This is what carries the source side across DescriptiveComplexity.Draw.Data.exists_out_iff_gateMat.