Polynomial counters for direct tableau serialization -- proof internals

theorem Complexity.TM.directSerializerHorizonPolynomial_eval_internal (q : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (directSerializerHorizonPolynomial q) = Polynomial.eval n q + n + 1

theorem Complexity.TM.directSerializerHorizonPolynomial_input_le_internal (q : Polynomial ℕ) (n : ℕ) : n + 1 ≤ Polynomial.eval n (directSerializerHorizonPolynomial q)

theorem Complexity.TM.directSerializerGateBoundPolynomial_eval_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (tm.directSerializerGateBoundPolynomial q) = tm.directUnrollingGateBound (fun (x : ℕ) => Polynomial.eval x (directSerializerHorizonPolynomial q)) n

theorem Complexity.TM.directSerializerFrontierPolynomial_eval_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (tm.directSerializerFrontierPolynomial q) = n + tm.directUnrollingGateBound (fun (x : ℕ) => Polynomial.eval x (directSerializerHorizonPolynomial q)) n

theorem Complexity.TM.directSerializerGateCountPolynomial_eval_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (tm.directSerializerGateCountPolynomial q) = tm.directUnrollingGateBound (fun (x : ℕ) => Polynomial.eval x (directSerializerHorizonPolynomial q)) n + 1

theorem Complexity.TM.DecidesInTime.directSerializerHorizon_internal {k : ℕ} {tm : TM k} {L : Language} (q : Polynomial ℕ) (hdec : tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x q) : tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x (directSerializerHorizonPolynomial q)