The enumerator's bounds, in the input's length

⚠️ Unreviewed by Bolton

Every quantity the enumerator's contracts and windows are stated in terms of — the width of a pair, the number of digits in a counter, the running time of a stage — is bounded by a polynomial in the input's length. This file collects those bounds.

Main results

• PolyExists.dropTop_length_le, PolyExists.pair_length_le — the witness and the pair it goes into are no wider than the horizon's exponent allows
• PolyExists.bits_length_le — a counter below the horizon has that many digits
• PolyExists.tally_le — a tally never exceeds its count

theorem Complexity.PolyExists.dropTop_length_le (m j N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hj : j < N) : (dropTop (j + 1)).length ≤ m

A witness below the horizon is no longer than the exponent.

theorem Complexity.PolyExists.pair_length_le (x : List Bool) (m j N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hj : j < N) : (pair x (dropTop (j + 1))).length ≤ 2 * x.length + 2 + m

And the pair it goes into is bounded too.

theorem Complexity.PolyExists.bits_length_le (m j N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hj : j ≤ N) : j.bits.length ≤ m + 1

A counter at most the horizon has at most m + 1 digits.

theorem Complexity.PolyExists.tally_le (P : ℕ → Bool) (v : ℕ) : NTM.tally P v ≤ v

A tally never exceeds its count.

theorem Complexity.PolyExists.binarySuccTime_le' (m v N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hv : v ≤ N) : TM.binarySuccTime v ≤ 2 * (m + 1) + 2

The successor's running time, in digits.

theorem Complexity.PolyExists.binaryBumpTime_le' (m j N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hj : j < N) : TM.binaryBumpTime (dropTop (j + 1)) ≤ 2 * m + 2

The witness advance's running time.

theorem Complexity.PolyExists.binaryEqTime_le' (m j N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hj : j < N) : TM.binaryEqTime (j + 1).bits N.bits ≤ m + 2

The comparison's running time.

theorem Complexity.PolyExists.eval_mono (r : Polynomial ℕ) {a b : ℕ} (h : a ≤ b) : Polynomial.eval a r ≤ Polynomial.eval b r

A polynomial with natural coefficients is monotone.

The bounds themselves

def Complexity.PolyExists.bP (lx m : ℕ) : ℕ

The width of the pair the matrix machine reads.

Equations

• Complexity.PolyExists.bP lx m = 2 * lx + 2 + m

def Complexity.PolyExists.bHb (lx m sb : ℕ) : ℕ

The window the matrix machine needs.

Equations

• Complexity.PolyExists.bHb lx m sb = Complexity.PolyExists.bP lx m + sb + 2

def Complexity.PolyExists.bH (lx m sb : ℕ) : ℕ

The wipe height.

Equations

• Complexity.PolyExists.bH lx m sb = Complexity.PolyExists.bHb lx m sb + 1

def Complexity.PolyExists.bB (lx m : ℕ) : ℕ

The bound on the heads the rewinds have to chase.

Equations

• Complexity.PolyExists.bB lx m = lx + 1 + (2 * lx + m + 4) + (m + 4)

def Complexity.PolyExists.bG (lx m sb : ℕ) : ℕ

The uniform bound on every head of every intermediate state.

Equations

• Complexity.PolyExists.bG lx m sb = Complexity.PolyExists.bHb lx m sb + 1 + Complexity.PolyExists.bB lx m + (Complexity.PolyExists.bP lx m + 1)

theorem Complexity.PolyExists.bP_le_bHb (lx m sb : ℕ) : bP lx m ≤ bHb lx m sb

theorem Complexity.PolyExists.bHb_lt_bH (lx m sb : ℕ) : bHb lx m sb + 1 ≤ bH lx m sb

theorem Complexity.PolyExists.bP_lt_bH (lx m sb : ℕ) : bP lx m + 1 ≤ bH lx m sb

theorem Complexity.PolyExists.bB_le_bG (lx m sb : ℕ) : bB lx m ≤ bG lx m sb

theorem Complexity.PolyExists.bHb_le_bG (lx m sb : ℕ) : bHb lx m sb + 1 ≤ bG lx m sb

theorem Complexity.PolyExists.bP_le_bG (lx m sb : ℕ) : bP lx m + 1 ≤ bG lx m sb

theorem Complexity.PolyExists.one_le_bG (lx m sb : ℕ) : 1 ≤ bG lx m sb

theorem Complexity.PolyExists.one_le_bB (lx m : ℕ) : 1 ≤ bB lx m

theorem Complexity.PolyExists.one_le_bHb (lx m sb : ℕ) : 1 ≤ bHb lx m sb

def Complexity.PolyExists.bW (st lx m sb pro epi : ℕ) : ℕ

The window the whole machine runs in: the uniform head bound plus one summand for every stage's own budget. Sums, not maxima, so that the whole thing is visibly a polynomial in the input's length.

Equations

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

theorem Complexity.PolyExists.bG_le_bW (st lx m sb pro epi : ℕ) : bG lx m sb ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.one_le_bW (st lx m sb pro epi : ℕ) : 1 ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage1 (st lx m sb pro epi : ℕ) : bG lx m sb + 1 ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage2 (st lx m sb pro epi : ℕ) (x w : List Bool) (hx : x.length = lx) (hw : w.length ≤ m) : bG lx m sb + TM.pairInputWorkTime x w ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage3 (st lx m sb pro epi : ℕ) : bG lx m sb + (1 + 1 + (2 * (max (bB lx m + 2) (3 * (bB lx m + 3) + 1) + 1) + 1)) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage4 (st lx m sb pro epi P : ℕ) (hP : P ≤ bP lx m) : bG lx m sb + (2 * P + 5) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage6 (st lx m sb pro epi : ℕ) : bG lx m sb + (1 + 1 + (2 * (max (bHb lx m sb + 2) (1 * (bHb lx m sb + 3) + 1) + 1) + 1)) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage8 (st lx m sb pro epi a r v : ℕ) (ha : TM.binarySuccTime a ≤ 2 * (m + 1) + 2) (hr : TM.binarySuccTime r ≤ 2 * (m + 1) + 2) (hv : TM.binarySuccTime v ≤ 2 * (m + 1) + 2) : bG lx m sb + (3 * (max (1 + 1 + max (TM.binarySuccTime a) (TM.binarySuccTime r) + 5) (TM.binarySuccTime v) + 1) + 1) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage9 (st lx m sb pro epi t : ℕ) (ht : t ≤ 2 * m + 2) : bG lx m sb + t ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_stage10 (st lx m sb pro epi H : ℕ) (hH : H = bH lx m sb) : bG lx m sb + (st * (H + 4) + H * 4 + 8 + 1 + (st * (H + 4) + 1)) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_test (st lx m sb pro epi N j : ℕ) (hj : TM.binaryEqTime (j + 1).bits N.bits ≤ m + 2) : bG lx m sb + testTime (bB lx m) N j ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_copy (st lx m sb pro epi : ℕ) : 1 + (lx + 1) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_rewind (st lx m sb pro epi : ℕ) : lx + 1 + (1 + 1 + (2 * (max (bB lx m + 2) (1 * (bB lx m + 3) + 1) + 1) + 1)) ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_prologue (st lx m sb pro epi : ℕ) : 1 + pro ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_epilogue (st lx m sb pro epi e : ℕ) (he : e ≤ epi) : 1 + e ≤ bW st lx m sb pro epi

theorem Complexity.PolyExists.bW_matrix (st lx m sb pro epi : ℕ) : bHb lx m sb ≤ bW st lx m sb pro epi

The bounds as polynomials

noncomputable def Complexity.PolyExists.bPPoly (p : Polynomial ℕ) : Polynomial ℕ

The width of the pair, as a polynomial in the input's length.

Equations

• Complexity.PolyExists.bPPoly p = Polynomial.C 2 * Polynomial.X + Polynomial.C 2 + p

@[simp]

theorem Complexity.PolyExists.bPPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bPPoly p) = bP lx (Polynomial.eval lx p)

noncomputable def Complexity.PolyExists.bHbPoly (p s : Polynomial ℕ) : Polynomial ℕ

The matrix machine's window, as a polynomial.

Equations

• Complexity.PolyExists.bHbPoly p s = Complexity.PolyExists.bPPoly p + s.comp (Complexity.PolyExists.bPPoly p) + Polynomial.C 2

@[simp]

theorem Complexity.PolyExists.bHbPoly_eval (p s : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bHbPoly p s) = bHb lx (Polynomial.eval lx p) (Polynomial.eval (bP lx (Polynomial.eval lx p)) s)

noncomputable def Complexity.PolyExists.bHPoly (p s : Polynomial ℕ) : Polynomial ℕ

The wipe height, as a polynomial.

Equations

• Complexity.PolyExists.bHPoly p s = Complexity.PolyExists.bHbPoly p s + 1

@[simp]

theorem Complexity.PolyExists.bHPoly_eval (p s : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bHPoly p s) = bH lx (Polynomial.eval lx p) (Polynomial.eval (bP lx (Polynomial.eval lx p)) s)

noncomputable def Complexity.PolyExists.bBPoly (p : Polynomial ℕ) : Polynomial ℕ

The rewind bound, as a polynomial.

Equations

• Complexity.PolyExists.bBPoly p = Polynomial.X + 1 + (Polynomial.C 2 * Polynomial.X + p + Polynomial.C 4) + (p + Polynomial.C 4)

@[simp]

theorem Complexity.PolyExists.bBPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bBPoly p) = bB lx (Polynomial.eval lx p)

noncomputable def Complexity.PolyExists.bGPoly (p s : Polynomial ℕ) : Polynomial ℕ

The uniform head bound, as a polynomial.

Equations

• Complexity.PolyExists.bGPoly p s = Complexity.PolyExists.bHbPoly p s + 1 + Complexity.PolyExists.bBPoly p + (Complexity.PolyExists.bPPoly p + 1)

@[simp]

theorem Complexity.PolyExists.bGPoly_eval (p s : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bGPoly p s) = bG lx (Polynomial.eval lx p) (Polynomial.eval (bP lx (Polynomial.eval lx p)) s)

noncomputable def Complexity.PolyExists.capPoly (p : Polynomial ℕ) : Polynomial ℕ

The Horner cap, as a polynomial.

Equations

• Complexity.PolyExists.capPoly p = Polynomial.C ((Complexity.TM.polyCoeffs p).sum + 1) * (Polynomial.X + 1) ^ (Complexity.TM.polyCoeffs p).length

@[simp]

theorem Complexity.PolyExists.capPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (capPoly p) = prologueCap p lx

noncomputable def Complexity.PolyExists.opBudgetPoly (p : Polynomial ℕ) : Polynomial ℕ

The register machine's per-operation budget, as a polynomial.

Equations

• Complexity.PolyExists.opBudgetPoly p = Polynomial.C 32 * (Complexity.PolyExists.capPoly p + Polynomial.C 2) ^ 3

@[simp]

theorem Complexity.PolyExists.opBudgetPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (opBudgetPoly p) = TM.opBudget (prologueCap p lx)

noncomputable def Complexity.PolyExists.layerBudgetPoly (p : Polynomial ℕ) : Polynomial ℕ

Its per-layer budget.

Equations

• Complexity.PolyExists.layerBudgetPoly p = Polynomial.C 4 * Complexity.PolyExists.opBudgetPoly p + Polynomial.C 3

@[simp]

theorem Complexity.PolyExists.layerBudgetPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (layerBudgetPoly p) = TM.layerBudget (prologueCap p lx)

noncomputable def Complexity.PolyExists.proPoly (p q : Polynomial ℕ) : Polynomial ℕ

The prologue's running time, dominated by a polynomial.

Equations

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

theorem Complexity.PolyExists.prologueTime_le (p q : Polynomial ℕ) (lx : ℕ) : prologueTime p q lx ≤ Polynomial.eval lx (proPoly p q)

noncomputable def Complexity.PolyExists.epiPoly (p : Polynomial ℕ) : Polynomial ℕ

The epilogue's running time, dominated by a polynomial.

Equations

• Complexity.PolyExists.epiPoly p = Polynomial.C 6 * p + Polynomial.C 50

theorem Complexity.PolyExists.epilogueTime_le (m A N : ℕ) (hN : N = 2 ^ (m + 1) - 1) (hA : A ≤ N) : epilogueTime A ≤ 6 * m + 50

noncomputable def Complexity.PolyExists.bWPoly (st : ℕ) (p s q : Polynomial ℕ) : Polynomial ℕ

The enumerator's space bound, as a polynomial.

Equations

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

@[simp]

theorem Complexity.PolyExists.bWPoly_eval (st : ℕ) (p s q : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (bWPoly st p s q) = bW st lx (Polynomial.eval lx p) (Polynomial.eval (bP lx (Polynomial.eval lx p)) s) (Polynomial.eval lx (proPoly p q)) (Polynomial.eval lx (epiPoly p))

@[simp]

theorem Complexity.PolyExists.epiPoly_eval (p : Polynomial ℕ) (lx : ℕ) : Polynomial.eval lx (epiPoly p) = 6 * Polynomial.eval lx p + 50

theorem Complexity.PolyExists.tally_pos_iff (P : ℕ → Bool) (N : ℕ) : 0 < NTM.tally P N ↔ ∃ j < N, P j = true

A tally is positive exactly when something below the count satisfied the predicate.

theorem Complexity.PolyExists.tally_pos_iff_mem (L' : Language) (p : Polynomial ℕ) (x : List Bool) (N : ℕ) (hN : N = 2 ^ (Polynomial.eval x.length p + 1) - 1) : 0 < NTM.tally (enumP L' x) N ↔ x ∈ polyExistsLang p L'

What the machine computes is membership in the bounded existential.

The enumerator, instantiated

theorem Complexity.PolyExists.enum_bounds {f : ℕ → ℕ} (s : Polynomial ℕ) (hs : ∀ (n : ℕ), f n ≤ Polynomial.eval n s) (p : Polynomial ℕ) (x : List Bool) (j : ℕ) (hj : j < 2 ^ (Polynomial.eval x.length p + 1) - 1) : 1 + TM.pairInputWorkTime x (dropTop (j + 1)) ≤ bB x.length (Polynomial.eval x.length p) ∧ (pair x (dropTop (j + 1))).length + f (pair x (dropTop (j + 1))).length + 2 ≤ bHb x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s) ∧ (pair x (dropTop (j + 1))).length + 1 ≤ bH x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s) ∧ 1 + 1 + TM.binaryEqTime (j + 1).bits (2 ^ (Polynomial.eval x.length p + 1) - 1).bits ≤ bB x.length (Polynomial.eval x.length p) ∧ (pair x (dropTop (j + 1))).length + 1 ≤ bG x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)

Every hypothesis the enumerator's contract and window need, at one input.

theorem Complexity.PolyExists.enumTM_decides {k : ℕ} (M : TM k) {L' : Language} {f : ℕ → ℕ} (s : Polynomial ℕ) (hs : ∀ (n : ℕ), f n ≤ Polynomial.eval n s) (hdecS : M.DecidesInSpace L' f) (hdec : M.DecidesInTime L' (M.spaceTimeBound f)) (p : Polynomial ℕ) (x : List Bool) (N H B Hb bBody bTest : ℕ) (hNdef : N = 2 ^ (Polynomial.eval x.length p + 1) - 1) (hHdef : H = bH x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)) (hBdef : B = bB x.length (Polynomial.eval x.length p)) (hHbdef : Hb = bHb x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)) (hbBody : ∀ v < N, bodyTime k x (M.spaceTimeBound f) H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v) ≤ bBody) (hbTest : ∀ v < N, testTime B N v ≤ bTest) : ∃ (c' : Cfg (enumTapes k) (enumTM M p (bHPoly p s)).Q), (enumTM M p (bHPoly p s)).reaches ((enumTM M p (bHPoly p s)).initCfg x) c' ∧ (enumTM M p (bHPoly p s)).halted c' ∧ (x ∈ polyExistsLang p L' → c'.output.cells 1 = Γ.one) ∧ (x ∉ polyExistsLang p L' → c'.output.cells 1 = Γ.zero)

The enumerator decides the bounded existential.

theorem Complexity.PolyExists.enumTM_space {k : ℕ} (M : TM k) {L' : Language} {f : ℕ → ℕ} (s : Polynomial ℕ) (hs : ∀ (n : ℕ), f n ≤ Polynomial.eval n s) (hdecS : M.DecidesInSpace L' f) (hdec : M.DecidesInTime L' (M.spaceTimeBound f)) (hne : M.qstart ≠ M.qhalt) (p : Polynomial ℕ) (x : List Bool) (N H B Hb G W bBody bTest : ℕ) (hNdef : N = 2 ^ (Polynomial.eval x.length p + 1) - 1) (hHdef : H = bH x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)) (hBdef : B = bB x.length (Polynomial.eval x.length p)) (hHbdef : Hb = bHb x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)) (hGdef : G = bG x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s)) (hWdef : W = bW (scratchTargets k).length x.length (Polynomial.eval x.length p) (Polynomial.eval (bP x.length (Polynomial.eval x.length p)) s) (Polynomial.eval x.length (proPoly p (bHPoly p s))) (Polynomial.eval x.length (epiPoly p))) (hbBody : ∀ v < N, bodyTime k x (M.spaceTimeBound f) H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v) ≤ bBody) (hbTest : ∀ v < N, testTime B N v ≤ bTest) (c' : Cfg (enumTapes k) (enumTM M p (bHPoly p s)).Q) : (enumTM M p (bHPoly p s)).reaches ((enumTM M p (bHPoly p s)).initCfg x) c' → c'.WithinDecisionSpace x.length W

The enumerator keeps a polynomial window.

theorem Complexity.PolyExists.exists_loop_bounds {k : ℕ} (M : TM k) (f : ℕ → ℕ) (x : List Bool) (L' : Language) (N H B Hb : ℕ) : ∃ (bBody : ℕ) (bTest : ℕ), (∀ v < N, bodyTime k x (M.spaceTimeBound f) H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v) ≤ bBody) ∧ ∀ v < N, testTime B N v ≤ bTest

The two loop budgets exist. Both are finite suprema over the counter range — they need not be polynomial, since the loop's time never enters the space accounting.