The EXPSPACE reduction, assembled

Everything the reduction stands on is built elsewhere; this file chooses the constants and puts them together.

• the base is the doubled universe, never a singleton, whose bottom and top are the marked copy of the instance's minimum and the junk copy of its maximum (DescriptiveComplexity.Draw.isBot_dblPt, isTop_dblPt);
• the data is the relativized expansion packed by DescriptiveComplexity.Draw.Data.ofSource, at a dimension wide enough for both the encoding and the payload (DescriptiveComplexity.Draw.srcDim) – the knot being that the slot inventory depends on the encoding budget, so the budget is chosen first and the record built twice at the same budget.

The payload bound Fintype.card (CtlIx ⊕ SlotIx) ≤ dd is not here, and the reason is worth recording. It is true because no budget of the record reads the dimension, but it is not rfl: DescriptiveComplexity.Draw.Data.nOf and every budget above it is defined by a match on dt.VarIx, so the matcher takes the whole record as a parameter and two records differing in any field are opaque to each other. What closes it is Finset.sup_congr down the chain, each step instantiated at a constructor of the index so that the matcher reduces.

The extremes of the doubled universe

theorem DescriptiveComplexity.Draw.isBot_dblPt {L : FirstOrder.Language} {A : Type} [LinearOrder A] {a : A} (ha : IsBot a) : IsBot (dblPt false a)

theorem DescriptiveComplexity.Draw.isTop_dblPt {L : FirstOrder.Language} {A : Type} [LinearOrder A] {a : A} (ha : IsTop a) : IsTop (dblPt true a)

The budgets do not read the dimension

Every budget of a DescriptiveComplexity.Draw.Data is a function of the expansion, the step definition and the packs; none reads the dimension. That is not rfl, though: DescriptiveComplexity.Draw.Data.nOf and its relatives are defined by a match, so their compiled matchers take the whole record as a parameter and two records differing in the dimension are opaque to each other. What closes it is a congruence at every level, each instantiated at a constructor of the scrutinee, where the matcher reduces.

theorem DescriptiveComplexity.Draw.ofSource_nOf {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') (v : (Data.ofSource X d h).VarIx) : (Data.ofSource X d h).nOf v = (Data.ofSource X d h').nOf v

theorem DescriptiveComplexity.Draw.ofSource_natOf {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') (v : (Data.ofSource X d h).VarIx) : (Data.ofSource X d h).natOf v = (Data.ofSource X d h').natOf v

theorem DescriptiveComplexity.Draw.ofSource_kindDepth {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') {n : ℕ} (κ : MatAtom X d.B n) : (Data.ofSource X d h).kindDepth κ = (Data.ofSource X d h').kindDepth κ

theorem DescriptiveComplexity.Draw.ofSource_kindReads {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') {n : ℕ} (κ : MatAtom X d.B n) : (Data.ofSource X d h).kindReads κ = (Data.ofSource X d h').kindReads κ

theorem DescriptiveComplexity.Draw.ofSource_kindArgs {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') {n : ℕ} (κ : MatAtom X d.B n) : (Data.ofSource X d h).kindArgs κ = (Data.ofSource X d h').kindArgs κ

theorem DescriptiveComplexity.Draw.ofSource_ki {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).ki = (Data.ofSource X d h').ki

theorem DescriptiveComplexity.Draw.ofSource_naDim {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).naDim = (Data.ofSource X d h').naDim

theorem DescriptiveComplexity.Draw.ofSource_natMax {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).natMax = (Data.ofSource X d h').natMax

theorem DescriptiveComplexity.Draw.ofSource_eDim {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).eDim = (Data.ofSource X d h').eDim

theorem DescriptiveComplexity.Draw.ofSource_nfDim {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).nfDim = (Data.ofSource X d h').nfDim

theorem DescriptiveComplexity.Draw.ofSource_ntgDim {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).ntgDim = (Data.ofSource X d h').ntgDim

theorem DescriptiveComplexity.Draw.ofSource_ctlIx {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).CtlIx = (Data.ofSource X d h').CtlIx

The control inventory does not read the dimension.

theorem DescriptiveComplexity.Draw.ofSource_slotIx {L : FirstOrder.Language} {X : ExpExpansion L} {d : StepDef (X.E.sum FirstOrder.Language.order)} {dd dd' : ℕ} (h : encDim X ≤ dd) (h' : encDim X ≤ dd') : (Data.ofSource X d h).SlotIx = (Data.ofSource X d h').SlotIx

Nor does the track inventory.

The record a source is packed into, at a dimension that fits

noncomputable def DescriptiveComplexity.Draw.srcData0 {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : Data L

The record at the bare encoding budget: only its slot and control inventories are read, and neither depends on the dimension.

Equations

• DescriptiveComplexity.Draw.srcData0 X d = DescriptiveComplexity.Draw.Data.ofSource X d ⋯

noncomputable def DescriptiveComplexity.Draw.srcDim {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : ℕ

The dimension the reduction works at: one coordinate of slack beyond the encoding budget, and wide enough for a rule's payload.

Equations

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

theorem DescriptiveComplexity.Draw.encDim_lt_srcDim {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : encDim X < srcDim X d

noncomputable def DescriptiveComplexity.Draw.srcData {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : Data L

The record the reduction works at.

Equations

• DescriptiveComplexity.Draw.srcData X d = DescriptiveComplexity.Draw.Data.ofSource X d ⋯

theorem DescriptiveComplexity.Draw.srcData_dd0 {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : (srcData X d).dd0 = encDim X

theorem DescriptiveComplexity.Draw.srcData_dd {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : (srcData X d).dd = srcDim X d

theorem DescriptiveComplexity.Draw.srcData_dd0_lt {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : (srcData X d).dd0 < (srcData X d).dd

theorem DescriptiveComplexity.Draw.srcData_payload_le {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : Fintype.card ((srcData X d).CtlIx ⊕ (srcData X d).SlotIx) ≤ (srcData X d).dd

A rule's payload fits the dimension: the inventories do not read it, so the count taken at the bare encoding budget is the count at the real one.

noncomputable def DescriptiveComplexity.Draw.srcKIx {L : FirstOrder.Language} (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : (srcData X d).KIx

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

Equations

• DescriptiveComplexity.Draw.srcKIx X d = Sum.inrₗ ⟨0, ⋯⟩

The interpretation the reduction emits

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.srcDt {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : Data (newLang L)

The record the reduction runs at: the relativized expansion, packed.

Equations

• DescriptiveComplexity.Draw.srcDt X d = DescriptiveComplexity.Draw.srcData (DescriptiveComplexity.Draw.relExp X) d

noncomputable def DescriptiveComplexity.Draw.srcAccept {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (e : Env (newLang L)) : (srcDt X d).PF → ((srcDt X d).CtlIx → e.α) → Prop

The accepting predicate of the emitted program: the output machinery's exit phase, with its verdict read from the control.

Equations

• DescriptiveComplexity.Draw.srcAccept X d e p f = (p = DescriptiveComplexity.Draw.OuterPh.acceptP ∧ ((DescriptiveComplexity.Draw.srcDt X d).varArgsOf e.zero e.one none).accBit f)

theorem DescriptiveComplexity.Draw.uGDefinable_srcAccept {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (p : (srcDt X d).PF) : UGDefinable fun (e : Env (newLang L)) (f : (srcDt X d).CtlIx → e.α) (x : (srcDt X d).SlotIx → e.α) => srcAccept X d e p f

noncomputable def DescriptiveComplexity.Draw.dblWideInterp {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : FOInterpretation ((newLang L).sum FirstOrder.Language.order) FirstOrder.Language.wide (srcDt X d).ITag (srcDt X d).dd

The machine of a source, written down over the doubled universe.

Equations

• DescriptiveComplexity.Draw.dblWideInterp X d = DescriptiveComplexity.Draw.Data.drawInterp ⋯ ⋯ ⋯ DescriptiveComplexity.Draw.OuterPh.start (DescriptiveComplexity.Draw.Data.regFileMark ⋯)

noncomputable def DescriptiveComplexity.Draw.wideInterp {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.wide ((srcDt X d).ITag × (Fin (srcDt X d).dd → Bool)) ((srcDt X d).dd * 1)

The machine of a source, written down in the instance: the machine over the doubled universe, composed with the doubling. The dimension is unchanged – the doubling is one-dimensional – and the tags only gain a Boolean per coordinate.

Equations

• DescriptiveComplexity.Draw.wideInterp X d = (DescriptiveComplexity.Draw.dblWideInterp X d).comp (DescriptiveComplexity.Draw.dblInterp L).ordExtend

The composite's universe is the machine's

noncomputable def DescriptiveComplexity.Draw.wideInterpEquiv {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] : FirstOrder.Language.wide.Equiv ((wideInterp X d).Map A) ((dblWideInterp X d).Map ((dblInterp L).Map A))

The composite interpretation's universe is the machine's over the doubled universe: the composition equivalence, followed by the order extension's.

Equations

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

The interpreted structure reads the program's table

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.srcRTagOrder {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : LinearOrder (srcDt X d).RTag

The two orders the run layer wants on the rule names and the phases: an arbitrary one on each, the same one the interpretation compares tags with.

Equations

• DescriptiveComplexity.Draw.srcRTagOrder X d = DescriptiveComplexity.finiteLinearOrder (DescriptiveComplexity.Draw.srcDt X d).RTag

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.srcPFOrder {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) : LinearOrder (srcDt X d).PF

Equations

• DescriptiveComplexity.Draw.srcPFOrder X d = DescriptiveComplexity.finiteLinearOrder (DescriptiveComplexity.Draw.srcDt X d).PF

theorem DescriptiveComplexity.Draw.srcReads {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (e : Env (newLang L)) : ((srcDt X d).progOf e.zero e.one ⋯ ⋯).table.Reads

The interpreted structure reads the emitted program's table.

The machine decides the fixed point

noncomputable def DescriptiveComplexity.Draw.srcEnv (L : FirstOrder.Language) [L.IsRelational] (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Env (newLang L)

The environment the reduction runs at: the doubled universe, with the marked copy of the instance's minimum and the junk copy of its maximum as the two designated elements.

Equations

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

theorem DescriptiveComplexity.Draw.dwideAcceptSpace_srcEnv_iff {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : DWideAcceptSpace.Holds ((dblWideInterp X d).Map (srcEnv L A).α) ↔ (srcDt X d).d.PFPHolds ((srcDt X d).X.Map (srcEnv L A).α)

The emitted machine accepts exactly when the partial fixed point holds, read over the doubled universe and at the order the encoding pulls back.

theorem DescriptiveComplexity.Draw.wideProblem_wideInterp_iff {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (PW : DecisionProblem FirstOrder.Language.wide) {Q₀ : DecisionProblem X.E} (hmach : PW.Holds ((dblWideInterp X d).Map (srcEnv L A).α) ↔ Q₀.Holds ((relExp X).Map ((dblInterp L).Map A))) : PW.Holds ((wideInterp X d).Map A) ↔ Q₀.Holds (X.Map A)

The transport from the doubled universe to the instance, for any question asked of the emitted machine. Three isomorphisms and nothing else: the composite's universe is the machine's (wideInterpEquiv), the caller says what the machine decides over the doubled universe, and the relativized expansion's points are the original's (relExpMapEquiv). Which problem PW is – acceptance in bounded space, acceptance on a clock, deterministic or not – the transport never asks.

theorem DescriptiveComplexity.Draw.wideAccept_wideInterp_iff {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {Q₀ : DecisionProblem X.E} (hmach : WideAccept.Holds ((dblWideInterp X d).Map (srcEnv L A).α) ↔ Q₀.Holds ((relExp X).Map ((dblInterp L).Map A))) : WideAccept.Holds ((wideInterp X d).Map A) ↔ Q₀.Holds (X.Map A)

The emitted instance is a yes-instance of acceptance on a clock exactly when the source is, given the clocked machine's own correctness at the doubled universe. The transport is wideProblem_wideInterp_iff's and nothing else – which problem the machine is asked about it never reads – so this half of the NEXPTIME reduction is free: what is not is the hypothesis, the clocked program's run against the kernel.

theorem DescriptiveComplexity.Draw.dwideAcceptSpace_wideInterp_iff {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {Q₀ : DecisionProblem X.E} (hd : ∀ (M : Type) [inst : X.E.Structure M] [inst_1 : LinearOrder M] [Finite M] [Nonempty M], Q₀.Holds M ↔ d.PFPHolds M) : DWideAcceptSpace.Holds ((wideInterp X d).Map A) ↔ Q₀.Holds (X.Map A)

The emitted instance is a yes-instance exactly when the source is: the composite's universe is the machine's over the doubled universe, the machine decides the fixed point there, the fixed point is the problem of the relativized expansion, and that expansion's points are the original's.

The reduction, and EXPSPACE-hardness

theorem DescriptiveComplexity.SOPFPDefinable.ordered_fo_reduction_dwideAcceptSpace {L : FirstOrder.Language} [L.IsRelational] {Q : DecisionProblem L} (h : SOPFPDefinable Q) : Nonempty (OrderedFOReduction Q DWideAcceptSpace)

Every SO(≤, PFP) definable problem reduces to deterministic acceptance in bounded space on a wide machine.

theorem DescriptiveComplexity.ExpDefinable.ordered_fo_reduction_wideAccept {L : FirstOrder.Language} [L.IsRelational] {Q : DecisionProblem L} (h : ExpDefinable NP Q) (hmach : ∀ (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (Q₀ : DecisionProblem X.E) (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], WideAccept.Holds ((Draw.dblWideInterp X d).Map (Draw.srcEnv L A).α) ↔ Q₀.Holds ((Draw.relExp X).Map ((Draw.dblInterp L).Map A))) : Nonempty (OrderedFOReduction Q WideAccept)

Every NEXPTIME source problem reduces to acceptance on a clock, given the clocked machine's correctness at each doubled universe. The reduction is the EXPSPACE one's drawing at the kernel's own step definition – the record is the same one (DescriptiveComplexity.Draw.Data.ofKernel is ofSource at NexKernel.toStepDef), so the dimension, the tags and the transport are all as they were, and only what the machine decides changes.

theorem DescriptiveComplexity.dwideAcceptSpace_EXPSPACE_hard : EXPSPACE.Hard DWideAcceptSpace

Deterministic acceptance in bounded space on a wide machine is EXPSPACE-hard.

theorem DescriptiveComplexity.dwideAcceptSpace_EXPSPACE_complete : EXPSPACE.Complete DWideAcceptSpace

Deterministic acceptance in bounded space on a wide machine is EXPSPACE-complete. The membership half is DescriptiveComplexity.dwideAcceptSpace_mem_EXPSPACE; the hardness half is the reduction above, run at the doubled universe so that the machine always has two elements to write bits with.

theorem DescriptiveComplexity.wideAccept_NEXPTIME_hard (hmach : ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (X : ExpExpansion L') (d : StepDef (X.E.sum FirstOrder.Language.order)) (Q₀ : DecisionProblem X.E) (A : Type) [inst_1 : L'.Structure A] [inst_2 : LinearOrder A] [inst_3 : Finite A] [inst_4 : Nonempty A], WideAccept.Holds ((Draw.dblWideInterp X d).Map (Draw.srcEnv L' A).α) ↔ Q₀.Holds ((Draw.relExp X).Map ((Draw.dblInterp L').Map A))) : NEXPTIME.Hard WideAccept

Acceptance on a clock on a wide machine is NEXPTIME-hard, given the clocked machine's correctness. Everything but that hypothesis is the EXPSPACE route's: the same drawing, the same transport, the same discharge – which is why the estimate for this half was «no design».

theorem DescriptiveComplexity.wideAccept_NEXPTIME_complete (hmach : ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (X : ExpExpansion L') (d : StepDef (X.E.sum FirstOrder.Language.order)) (Q₀ : DecisionProblem X.E) (A : Type) [inst_1 : L'.Structure A] [inst_2 : LinearOrder A] [inst_3 : Finite A] [inst_4 : Nonempty A], WideAccept.Holds ((Draw.dblWideInterp X d).Map (Draw.srcEnv L' A).α) ↔ Q₀.Holds ((Draw.relExp X).Map ((Draw.dblInterp L').Map A))) : NEXPTIME.Complete WideAccept

Acceptance on a clock on a wide machine is NEXPTIME-complete, given the clocked machine's correctness. The membership half is DescriptiveComplexity.wideAccept_mem_NEXPTIME and is unconditional; the hardness half is the reduction above.

theorem DescriptiveComplexity.wideAcceptSpace_EXPSPACE_hard : EXPSPACE.Hard WideAcceptSpace

Acceptance in bounded space on a wide machine is EXPSPACE-hard: hardness travels forward along the reduction that adds the determinism promise.

theorem DescriptiveComplexity.wideAcceptSpace_EXPSPACE_complete : EXPSPACE.Complete WideAcceptSpace

Acceptance in bounded space on a wide machine is EXPSPACE-complete.