Polynomial counters for direct tableau serialization

This module exposes the normalized horizon and closed polynomial counters used by the log-space tableau serializer. Their evaluations are literal equalities to the padded family's bounds, so the generator can compute its header and padding frontier without first counting the emitted raw gates.

Main results

• directSerializerHorizonPolynomial_input_le supplies n + 1 ≤ T(n).
• directSerializerGateBoundPolynomial_eval identifies the padding target.
• directSerializerFrontierPolynomial_eval identifies the post-padding wire.
• directSerializerGateCountPolynomial_eval identifies the code header.
• DecidesInTime.directSerializerHorizon safely enlarges a time witness.

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Complexity.TM.directSerializerGateCountPolynomial_eval {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 {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)

Enlarging a polynomial time bound to the serializer's normalized horizon preserves language decision correctness.