The data of the EXPSPACE reduction, bundled

Everything the EXPSPACE program is built from, in one record: the expansion, the partial-fixed-point definition, one prenex pack per step formula and one for the output sentence, and the encoding layout with its coordinate budget. On top of it, the derived dimensions the slot and control inventories of DescriptiveComplexity.Problems.Wide.DrawSlots are sized by: the variable index DescriptiveComplexity.Draw.Data.VarIx (none is the output), the prefix lengths nOf and their maximum ki, the outer block count ko, the classified atoms of each matrix (DescriptiveComplexity.Draw.Data.kindOf) and their counts.

The point of bundling: the program's phase and rule types are indexed by this data (one call site per variable, per atom, per argument position), so every site file takes one Draw.Data and nothing else, and the dimensions are defined as the exact maxima rather than constrained by inequalities.

structure DescriptiveComplexity.Draw.Data (L : FirstOrder.Language) : Type 1

The data of the EXPSPACE reduction: the expansion, the definition, the prenex packs, and the encoding layout with its coordinate budget.

• X : ExpExpansion L

  The exponential expansion the machine's tape simulates.

• d : StepDef (self.X.E.sum FirstOrder.Language.order)

  The partial-fixed-point definition being iterated.

• pk (i : self.d.B.ι) : PrenexPack (self.d.step i)

  A prenex pack per step formula.

• pkOut : PrenexPack (FirstOrder.Language.Formula.relabel Empty.elim self.d.out)

  A prenex pack for the output sentence, its (no) free variables re-bound.

• domPk (t : self.X.Tag) : PrenexPack (FirstOrder.Language.Formula.relabel Empty.elim (self.X.dom t))

  A prenex pack per domain sentence of the expansion: the gate's dom sub-evaluation runs its prefix as an element loop.

• relPk {n : ℕ} (r : self.X.E.Relations n) (τ : Fin n → self.X.Tag) : PrenexPack (FirstOrder.Language.Formula.relabel Empty.elim (self.X.relSentence r τ))

  A prenex pack per defining sentence of the expansion, at each relation symbol and tuple of tags: the expansion atoms' sub-folds run these.

• dd0 : ℕ

  The coordinate budget of the encodings: the name slots of a mark.

• dd : ℕ

  The dimension of the interpretation.

• ly : EncLayout (PtCode self.X) (blockArityBound self.X.B) self.dd

  The encoding layout of the points.

• lyLt (j : Fin self.dd) : ((∃ (q : PtCode self.X), self.ly.cIx q = j) ∨ ∃ (p : Fin (blockArityBound self.X.B)), self.ly.pIx p = j) → ↑j < self.dd0

  The layout inhabits the first dd0 coordinates, so a padded cell's mark can carry its own encoding-relevant coordinates in name slots.

• dd0Le : self.dd0 ≤ self.dd

  The budget fits in the dimension.

The variable index

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.VarIx {L : FirstOrder.Language} (dt : Data L) : Type

The variables the program evaluates a formula for: the fixed-point variables, and (none) the output sentence.

Equations

• dt.VarIx = Option dt.d.B.ι

noncomputable def DescriptiveComplexity.Draw.Data.ko {L : FirstOrder.Language} (dt : Data L) : ℕ

The number of outer argument blocks: enough for every variable's arguments.

Equations

• dt.ko = DescriptiveComplexity.blockArityBound dt.d.B

def DescriptiveComplexity.Draw.Data.arOf {L : FirstOrder.Language} (dt : Data L) : dt.VarIx → ℕ

The arity of a variable – the number of blocks its address prefix reads; 0 for the output.

Equations

• dt.arOf none = 0
• dt.arOf (some i) = dt.d.B.arity i

@[reducible]

def DescriptiveComplexity.Draw.Data.nOf {L : FirstOrder.Language} (dt : Data L) : dt.VarIx → ℕ

The prefix length of a variable's pack. Reducible: the pack's own statements are about (dt.pk i).n, and rw matches at implicit transparency.

Equations

• dt.nOf none = dt.pkOut.n
• dt.nOf (some i) = (dt.pk i).n

@[reducible]

def DescriptiveComplexity.Draw.Data.polOf {L : FirstOrder.Language} (dt : Data L) : dt.VarIx → ℕ → Bool

The polarities of a variable's pack.

Equations

• dt.polOf none = dt.pkOut.pol
• dt.polOf (some i) = (dt.pk i).pol

@[reducible]

def DescriptiveComplexity.Draw.Data.matOf {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf v)

The matrix of a variable's pack.

Equations

• dt.matOf none = dt.pkOut.mat
• dt.matOf (some i) = (dt.pk i).mat

theorem DescriptiveComplexity.Draw.Data.matOf_isQF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : (dt.matOf v).IsQF

theorem DescriptiveComplexity.Draw.Data.arOf_le_nOf {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.arOf v ≤ dt.nOf v

theorem DescriptiveComplexity.Draw.Data.arOf_le_ko {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.arOf v ≤ dt.ko

noncomputable def DescriptiveComplexity.Draw.Data.ki {L : FirstOrder.Language} (dt : Data L) : ℕ

The number of inner argument blocks: the longest prefix among the packs.

Equations

• dt.ki = Finset.univ.sup dt.nOf

theorem DescriptiveComplexity.Draw.Data.nOf_le_ki {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.nOf v ≤ dt.ki

The classified atoms

def DescriptiveComplexity.Draw.Data.atomsOf {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : List (((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf v))

The atoms of a variable's matrix, in evaluation order.

Equations

• dt.atomsOf v = DescriptiveComplexity.Draw.qfAtoms (dt.matOf v)

def DescriptiveComplexity.Draw.Data.natOf {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : ℕ

The number of atoms of a variable's matrix.

Equations

• dt.natOf v = (dt.atomsOf v).length

noncomputable def DescriptiveComplexity.Draw.Data.natMax {L : FirstOrder.Language} (dt : Data L) : ℕ

The largest atom count among the matrices: the size of the verdict inventory.

Equations

• dt.natMax = Finset.univ.sup dt.natOf

theorem DescriptiveComplexity.Draw.Data.natOf_le_natMax {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.natOf v ≤ dt.natMax

noncomputable def DescriptiveComplexity.Draw.Data.kindOf {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : MatAtom dt.X dt.d.B (dt.nOf v)

The kind of an atom, read off the syntax: the index data of the per-atom call sites.

Equations

• dt.kindOf v a = (DescriptiveComplexity.Draw.matAtom? ((dt.atomsOf v).get a)).get ⋯

theorem DescriptiveComplexity.Draw.Data.matAtom?_get {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : matAtom? ((dt.atomsOf v).get a) = some (dt.kindOf v a)

The classifier agrees with the kind.

The slot and control inventories, sized

The control dimensions

noncomputable def DescriptiveComplexity.Draw.Data.kindDepth {L : FirstOrder.Language} (dt : Data L) {n : ℕ} : MatAtom dt.X dt.d.B n → ℕ

The prefix depth of an expansion atom's defining sentences, maximized over the tag tuples; 0 for the other kinds, whose loops are the coordinate ones.

Equations

• dt.kindDepth (DescriptiveComplexity.Draw.MatAtom.exp e a) = Finset.univ.sup fun (τ : Fin k → dt.X.Tag) => (dt.relPk e τ).n
• dt.kindDepth x✝ = 0

noncomputable def DescriptiveComplexity.Draw.Data.kindReads {L : FirstOrder.Language} (dt : Data L) {n : ℕ} : MatAtom dt.X dt.d.B n → ℕ

The leaf-read budget of an atom: the block-atom count of its defining sentences' matrices – the base-vocabulary atoms are guards and take no trip – 2 for the coordinate loops of an equality or order atom, 0 for a stage atom.

Equations

• dt.kindReads (DescriptiveComplexity.Draw.MatAtom.exp e a) = Finset.univ.sup fun (τ : Fin k → dt.X.Tag) => (DescriptiveComplexity.Draw.blkAtoms (dt.relPk e τ).mat).length
• dt.kindReads (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = 2
• dt.kindReads (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = 2
• dt.kindReads (DescriptiveComplexity.Draw.MatAtom.stage i a) = 0

noncomputable def DescriptiveComplexity.Draw.Data.domDepth {L : FirstOrder.Language} (dt : Data L) : ℕ

The domain sentences' largest prefix depth.

Equations

• dt.domDepth = Finset.univ.sup fun (t : dt.X.Tag) => (dt.domPk t).n

noncomputable def DescriptiveComplexity.Draw.Data.domReads {L : FirstOrder.Language} (dt : Data L) : ℕ

The domain sentences' largest read-leaf count.

Equations

• dt.domReads = Finset.univ.sup fun (t : dt.X.Tag) => (DescriptiveComplexity.Draw.blkAtoms (dt.domPk t).mat).length

noncomputable def DescriptiveComplexity.Draw.Data.eDim {L : FirstOrder.Language} (dt : Data L) : ℕ

The loop-variable budget: the coordinate loops' width and every element loop's depth.

Equations

• dt.eDim = max (max dt.dd0 dt.domDepth) (Finset.univ.sup fun (v : dt.VarIx) => Finset.univ.sup fun (a : Fin (dt.natOf v)) => dt.kindDepth (dt.kindOf v a))

noncomputable def DescriptiveComplexity.Draw.Data.nfDim {L : FirstOrder.Language} (dt : Data L) : ℕ

The leaf-read budget.

Equations

• dt.nfDim = max dt.domReads (Finset.univ.sup fun (v : dt.VarIx) => Finset.univ.sup fun (a : Fin (dt.natOf v)) => dt.kindReads (dt.kindOf v a))

noncomputable def DescriptiveComplexity.Draw.Data.kindArgs {L : FirstOrder.Language} (dt : Data L) {n : ℕ} : MatAtom dt.X dt.d.B n → ℕ

The number of argument points an atom's kind reads the tags of: the arity of an expansion atom, 0 for the other kinds.

Equations

• dt.kindArgs (DescriptiveComplexity.Draw.MatAtom.exp e a) = k
• dt.kindArgs x✝ = 0

noncomputable def DescriptiveComplexity.Draw.Data.ntgDim {L : FirstOrder.Language} (dt : Data L) : ℕ

The tag-flag budget: one per argument position of an expansion atom and tag, and one block's worth for the gates – whose domain evaluation reads the tag of the single block it gates, and which must be paid for even when no expansion atom occurs.

Equations

• dt.ntgDim = ((Finset.univ.sup fun (v : dt.VarIx) => Finset.univ.sup fun (a : Fin (dt.natOf v)) => dt.kindArgs (dt.kindOf v a)) + 1) * Fintype.card dt.X.Tag

noncomputable def DescriptiveComplexity.Draw.Data.naDim {L : FirstOrder.Language} (dt : Data L) : ℕ

The accumulator budget: one per prefix level, and one over.

Equations

• dt.naDim = dt.ki + 1

theorem DescriptiveComplexity.Draw.Data.dd0_le_eDim {L : FirstOrder.Language} (dt : Data L) : dt.dd0 ≤ dt.eDim

theorem DescriptiveComplexity.Draw.Data.domDepth_le_eDim {L : FirstOrder.Language} (dt : Data L) : dt.domDepth ≤ dt.eDim

theorem DescriptiveComplexity.Draw.Data.kindDepth_le_eDim {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : dt.kindDepth (dt.kindOf v a) ≤ dt.eDim

theorem DescriptiveComplexity.Draw.Data.domReads_le_nfDim {L : FirstOrder.Language} (dt : Data L) : dt.domReads ≤ dt.nfDim

theorem DescriptiveComplexity.Draw.Data.kindArgs_mul_card_le_ntgDim {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : dt.kindArgs (dt.kindOf v a) * Fintype.card dt.X.Tag ≤ dt.ntgDim

An expansion atom's tag flags fit: one per argument position and tag.

theorem DescriptiveComplexity.Draw.Data.card_le_ntgDim {L : FirstOrder.Language} (dt : Data L) : Fintype.card dt.X.Tag ≤ dt.ntgDim

A gate's tag flags fit: one block's worth is always paid for.

theorem DescriptiveComplexity.Draw.Data.kindReads_le_nfDim {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : dt.kindReads (dt.kindOf v a) ≤ dt.nfDim

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.CtlIx {L : FirstOrder.Language} (dt : Data L) : Type

The control slots of the program, at the computed budgets.

Equations

• dt.CtlIx = DescriptiveComplexity.Draw.Ctl dt.eDim dt.naDim dt.natMax dt.nfDim dt.ntgDim

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.SlotIx {L : FirstOrder.Language} (dt : Data L) : Type

The track slots of the program.

Equations

• dt.SlotIx = DescriptiveComplexity.Draw.Slot dt.d.B.ι dt.ko dt.ki dt.dd0

@[instance_reducible]

noncomputable instance DescriptiveComplexity.Draw.Data.instDecidableEqSlotIx {L : FirstOrder.Language} (dt : Data L) : DecidableEq dt.SlotIx

The slots' equality is classically decidable – the variable index only carries Finite, and the rules that update slots (Function.update) are noncomputable throughout.

Equations

• dt.instDecidableEqSlotIx = Classical.decEq dt.SlotIx

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.KIx {L : FirstOrder.Language} (dt : Data L) : Type

The block-index type of the program's addresses.

Equations

• dt.KIx = (Fin dt.ko ⊕ₗ Fin dt.ki)