From a problem over an expansion to one with value invention

The two halves built in DescriptiveComplexity.SecondOrderNewExpPull and DescriptiveComplexity.SecondOrderNewExpBuild meet here: a problem that a Σ₁ sentence decides over an exponential expansion is decided by a Σ₁ sentence with exponentially bounded value invention (DescriptiveComplexity.ExpDefinable.toSigmaSONewExp).

The two constants of the bound are read off the expansion: one invented value per assignment of its block with one nullary variable added per tag, so their number is 2 ^ (c · nᵈ) with c the number of variables and d the largest arity. Nothing about the source problem enters the bound – its own Σ₁ block rides along inside the guess, over the extended universe, and is read at the values naming the points.

theorem DescriptiveComplexity.ExpDefinable.toSigmaSONewExp {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : ExpDefinable NP P) : ∃ (c : ℕ) (d : ℕ), SigmaSONewExpDefinable c d P

NEXPTIME ⊆ ∃SO[new, exp c d]: a problem decided in NP over an exponential expansion is decided by a Σ₁ sentence that invents at most 2 ^ (c · nᵈ) values.

theorem DescriptiveComplexity.mem_NEXPTIME_iff_sigmaSONewExpDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : NEXPTIME.Mem P ↔ ∃ (c : ℕ) (d : ℕ), SigmaSONewExpDefinable c d P

∃SO[new, exp] = NEXPTIME: a problem is decided one exponential up in NP exactly when a Σ₁ sentence with exponentially bounded value invention decides it. The two constants are the expansion's – how many variables its block has, once one nullary variable per tag is added, and how wide they are – and no single pair serves every problem, so they are quantified.