Freezing the acceptance probability past the halting time

A probabilistic machine whose paths all halt within T steps has the same acceptance probability at every later time bound: the extra choice bits are read by no transition, so they only refine the sample space uniformly. This lets a machine's arbitrary time-bound function be replaced by a polynomial that dominates it, which is what makes the Lautemann matrix predicate computable — see Complexitylib.Classes.PH.SipserLautemann.Matrix.

Main results

• card_filter_blockFst_eq — a prefix fiber of the seed space has 2 ^ b points
• NTM.acceptProb_eq_of_allPathsHaltIn — the acceptance probability is frozen past the halting time
• NTM.acceptsWithProb_of_le, NTM.rejectsWithProb_of_le — the bounded-error conditions transfer to any pointwise-larger time bound

theorem Complexity.card_filter_blockFst_eq (a b : ℕ) (seed : Fin a → Bool) : {w : Fin (a + b) → Bool | blockFst a b w = seed}.card = 2 ^ b

Every prefix fiber of the seed space has exactly 2 ^ b points: fixing the first a bits leaves the last b free.

theorem Complexity.NTM.acceptProb_eq_of_allPathsHaltIn {n : ℕ} {tm : NTM n} {T : ℕ → ℕ} (hN : tm.AllPathsHaltIn T) (x : List Bool) {T' : ℕ} (hle : T x.length ≤ T') : tm.acceptProb x T' = tm.acceptProb x (T x.length)

The acceptance probability is frozen past the halting time. If all paths halt within T (|x|) steps, running the machine for any longer bound leaves the acceptance probability unchanged: the surplus choice bits partition the enlarged sample space into equal fibers over the original one. This is the AllPathsHaltIn form of NTM.acceptProb_eq_of_le_of_allChoicesHalt, with a scalar larger clock (NTM.acceptProb_eq_of_le_of_allPathsHaltIn is the version for a pointwise-larger clock function).

theorem Complexity.NTM.acceptsWithProb_of_le {n : ℕ} {tm : NTM n} {L : Language} {T T' : ℕ → ℕ} {c : ℚ} (hN : tm.AllPathsHaltIn T) (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.AcceptsWithProb L T c) : tm.AcceptsWithProb L T' c

The completeness condition transfers to any pointwise-larger time bound.

theorem Complexity.NTM.rejectsWithProb_of_le {n : ℕ} {tm : NTM n} {L : Language} {T T' : ℕ → ℕ} {s : ℚ} (hN : tm.AllPathsHaltIn T) (hle : ∀ (m : ℕ), T m ≤ T' m) (h : tm.RejectsWithProb L T s) : tm.RejectsWithProb L T' s

The soundness condition transfers to any pointwise-larger time bound.