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

The machine decides the fixed point

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. Registered in the Lax archive as Lax822549.WideMachinesComplete.wideRegAccept_NEXPTIME_complete.