The reduction into the register channel

DescriptiveComplexity.Problems.Wide.Reduce assembles the reduction into DescriptiveComplexity.WideAccept: the record, the interpretation, the transport and the hardness statement. This file does the same at the register channel – the same record, the same doubling, the same transport, and one change: the interpretation writes down the handed program (nexInterpHandedPad), whose channel writes for the argument elements and the one below them, and the problem it lands in is DescriptiveComplexity.WideRegAccept.

The transport is unchanged because it never reads which problem is being asked about (wideRegProblem_wideRegInterp_iff is wideProblem_wideInterp_iff at the other interpretation), so this half of the reduction is free. What is not free is the machine's correctness, which is the run of DescriptiveComplexity.Draw.Data.wideRegAccept_regLaid_of_rules on the yes-side and DescriptiveComplexity.Problems.Wide.DrawNo on the no-side.

The interpretation the reduction emits

noncomputable def DescriptiveComplexity.Draw.dblWideRegInterp {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (n : ℕ) : FOInterpretation ((newLang L).sum FirstOrder.Language.order) FirstOrder.Language.wide ((srcDt X d).NexITagPad ((srcDt X d).d.B.ι → Bool) n) (srcDt X d).dd

The handed machine of a source, written down over the doubled universe: DescriptiveComplexity.Draw.dblWideInterp with the clocked program that is handed its file, and the channel that writes for the argument elements and the element below them. The program carries n junk rule names, which is what buys its clock the room the count asks for (PadRules.lean); at n = 0 it is the plain program with its sites relabeled.

Equations

• DescriptiveComplexity.Draw.dblWideRegInterp X d n = (DescriptiveComplexity.Draw.srcDt X d).nexInterpHandedPad ⋯ ⋯ none n

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

The handed machine of a source, written down in the instance: the machine over the doubled universe, composed with the doubling.

Equations

• DescriptiveComplexity.Draw.wideRegInterp X d n = (DescriptiveComplexity.Draw.dblWideRegInterp X d n).comp (DescriptiveComplexity.Draw.dblInterp L).ordExtend

The composite's universe is the machine's

noncomputable def DescriptiveComplexity.Draw.wideRegInterpEquiv {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] (n : ℕ) : FirstOrder.Language.wide.Equiv ((wideRegInterp X d n).Map A) ((dblWideRegInterp X d n).Map ((dblInterp L).Map A))

The composite interpretation's universe is the machine's over the doubled universe, at the handed machine: the composition equivalence followed by the order extension's, exactly as at the laid one.

Equations

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

The interpreted structure reads the handed program's table

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.srcNexRTagOrder {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (n : ℕ) : LinearOrder ((srcDt X d).NexRIxPad ((srcDt X d).d.B.ι → Bool) n)

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

Equations

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

@[reducible, inline]

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

Equations

• DescriptiveComplexity.Draw.srcNexPFOrder X d = DescriptiveComplexity.finiteLinearOrder (DescriptiveComplexity.Draw.srcDt X d).NexPF

theorem DescriptiveComplexity.Draw.srcRegReads {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (d : StepDef (X.E.sum FirstOrder.Language.order)) (e : Env (newLang L)) (n : ℕ) : ((srcDt X d).nexProgHandedPad e.zero e.one ⋯ ⋯ ((srcDt X d).regionSpec e.zero e.one) (fun (v : (srcDt X d).VarIx) => (srcDt X d).varArgsOf e.zero e.one v) none n).table.Reads

The interpreted structure reads the handed program's table – srcReads at the program a reduction into DescriptiveComplexity.WideRegAccept emits.

The machine decides the fixed point

theorem DescriptiveComplexity.Draw.wideRegAccept_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] (n : ℕ) (_harity : ∀ (iv : (srcDt X d).d.B.ι), 0 < (srcDt X d).d.B.arity iv) (_htags : 52 * (4 + (srcDt X d).eDim) * Nat.card (srcDt X d).KIx + 52 * (4 + (srcDt X d).eDim) + 52 * (15 + (srcDt X d).dimC) + 2 ≤ Nat.card ((srcDt X d).NexRIxPad ((srcDt X d).d.B.ι → Bool) n)) : WideRegAccept.Holds ((dblWideRegInterp X d n).Map (srcEnv L A).α) ↔ ∃ (σ : (srcDt X d).d.B.Assignment ((srcDt X d).X.Map (srcEnv L A).α)), (srcDt X d).X.Map (srcEnv L A).α ⊨ (srcDt X d).d.out

The emitted machine accepts exactly when some stage satisfies the kernel, read over the doubled universe and at the order the encoding pulls back. This is dwideAcceptSpace_srcEnv_iff at the handed machine: the record's own facts – its table is read (srcRegReads), its payload fits, its dimension has slack, its channel marks the argument elements – plus the two the source side owes, that every guessed variable has an argument and that the padded rule names outnumber the constant the clock is measured against.

theorem DescriptiveComplexity.Draw.wideRegAccept_kernel_iff {L : FirstOrder.Language} [L.IsRelational] (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (K : NexKernel L) (n : ℕ) (_harity : ∀ (iv : (srcDt K.X K.toStepDef).d.B.ι), 0 < (srcDt K.X K.toStepDef).d.B.arity iv) (_htags : 52 * (4 + (srcDt K.X K.toStepDef).eDim) * Nat.card (srcDt K.X K.toStepDef).KIx + 52 * (4 + (srcDt K.X K.toStepDef).eDim) + 52 * (15 + (srcDt K.X K.toStepDef).dimC) + 2 ≤ Nat.card ((srcDt K.X K.toStepDef).NexRIxPad ((srcDt K.X K.toStepDef).d.B.ι → Bool) n)) : WideRegAccept.Holds ((dblWideRegInterp K.X K.toStepDef n).Map (srcEnv L A).α) ↔ K.Holds ((relExp K.X).Map ((dblInterp L).Map A))

The handed machine decides the kernel, at the doubled universe: the record's correctness (wideRegAccept_srcEnv_iff) read through NexKernel.holds_iff_structure₁, which is the same proposition spelled the kernel's way. This is hmach's content, with the two obligations the source side owes still in front of it.

theorem DescriptiveComplexity.Draw.wideRegProblem_wideRegInterp_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) (n : ℕ) {Q₀ : DecisionProblem X.E} (hmach : PW.Holds ((dblWideRegInterp X d n).Map (srcEnv L A).α) ↔ Q₀.Holds ((relExp X).Map ((dblInterp L).Map A))) : PW.Holds ((wideRegInterp X d n).Map A) ↔ Q₀.Holds (X.Map A)

The emitted instance is a yes-instance exactly when the source is, for any problem about wide machines: the composite's universe is the machine's over the doubled universe (wideRegInterpEquiv), the caller says what the machine decides there, and the relativized expansion's points are the original's. Which problem PW is, the transport never asks – which is why the register channel costs nothing here.

theorem DescriptiveComplexity.Draw.wideRegAccept_wideRegInterp_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] (n : ℕ) {Q₀ : DecisionProblem X.E} (hmach : WideRegAccept.Holds ((dblWideRegInterp X d n).Map (srcEnv L A).α) ↔ Q₀.Holds ((relExp X).Map ((dblInterp L).Map A))) : WideRegAccept.Holds ((wideRegInterp X d n).Map A) ↔ Q₀.Holds (X.Map A)

The emitted instance is a yes-instance of acceptance on a clock at the register channel exactly when the source is, given the handed machine's own correctness at the doubled universe.

The reduction, and NEXPTIME-hardness

theorem DescriptiveComplexity.ExpDefinable.ordered_fo_reduction_wideRegAccept {L : FirstOrder.Language} [L.IsRelational] {Q : DecisionProblem L} (h : ExpDefinable NP Q) : Nonempty (OrderedFOReduction Q WideRegAccept)

Every NEXPTIME source problem reduces to acceptance on a clock at the register channel. The drawing is the EXPSPACE reduction's at the kernel's own step definition; only the program written down and the channel it is handed change. Two paddings make it unconditional: the kernel's variables gain an argument (NexKernel.withArg), which the machine needs to address a stage on its tape, and the program gains as many junk rule names as the clock's count asks for (PadRules.lean), which costs the drawing nothing and buys its budget outright.

theorem DescriptiveComplexity.wideRegAccept_NEXPTIME_hard : NEXPTIME.Hard WideRegAccept

Acceptance on a clock at the register channel is NEXPTIME-hard.

theorem DescriptiveComplexity.wideRegAccept_NEXPTIME_complete : NEXPTIME.Complete WideRegAccept

Acceptance on a clock at the register channel is NEXPTIME-complete. The membership half is DescriptiveComplexity.wideRegAccept_mem_NEXPTIME.