Polynomial counters for direct tableau serialization -- definitions

The streaming generator normalizes an arbitrary polynomial time bound so its horizon contains the complete input. It also evaluates three fixed natural polynomials: the padded gate bound, the wire frontier after that padding, and the positive member's gate-count header. Keeping these values as polynomials lets the binary polynomial subroutine compute them in logarithmic workspace.

noncomputable def Complexity.TM.directSerializerHorizonPolynomial (q : Polynomial ℕ) : Polynomial ℕ

Normalize a polynomial horizon so n + 1 represented tape cells always fit inside the bounded tableau.

Equations

• Complexity.TM.directSerializerHorizonPolynomial q = q + Polynomial.X + Polynomial.C 1

noncomputable def Complexity.TM.directSerializerGateBoundPolynomial {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : Polynomial ℕ

Closed padded gate bound for the normalized horizon.

Equations

• tm.directSerializerGateBoundPolynomial q = Polynomial.C (Complexity.CircuitUnrolling.acceptanceSizeCoeff tm.toNTM) * (Complexity.TM.directSerializerHorizonPolynomial q + Polynomial.C 2) ^ 3

noncomputable def Complexity.TM.directSerializerFrontierPolynomial {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : Polynomial ℕ

First unused wire after the padded gates, before the final output copy.

Equations

• tm.directSerializerFrontierPolynomial q = Polynomial.X + tm.directSerializerGateBoundPolynomial q

noncomputable def Complexity.TM.directSerializerGateCountPolynomial {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : Polynomial ℕ

Number encoded in the positive tagged circuit header, including the terminal output-copy gate.

Equations

• tm.directSerializerGateCountPolynomial q = tm.directSerializerGateBoundPolynomial q + Polynomial.C 1