Deterministic unrolling into uniform P/poly

This module packages the verified log-space tableau serializer into the machines-to-circuits direction of uniform P/poly. The conditional seams remain available for alternate serializers. The canonical padded serializer discharges the padded seam at a normalized horizon; no theorem discharges the unpadded directUnrollingCode seam.

Main results

• TM.DecidesInTime.mem_UniformPPoly_of_directUnrollingCode_mem_FL packages one polynomial-time decider and direct-code generator.
• P_subset_UniformPPoly_of_directUnrollingCode_mem_FL packages the resulting conditional class containment.
• The corresponding paddedDirectUnrollingCode theorems target the regular family whose gate-count header is known before gate emission begins.
• P_subset_UniformPPoly and UniformPPoly_eq_P are the completed headline.

theorem Complexity.TM.DecidesInTime.mem_UniformPPoly_of_directUnrollingCode_mem_FL {k : ℕ} {tm : TM k} {L : Language} (q : Polynomial ℕ) (hdec : tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x q) (hgen : (fun (x : List Bool) => tm.directUnrollingCode (fun (x : ℕ) => Polynomial.eval x q) x.length) ∈ FL) : L ∈ UniformPPoly

A polynomial-time decider belongs to uniform P/poly whenever its direct unrolling code map is computable in logarithmic space.

The hypothesis hgen is not known for this unpadded code; the verified generator targets paddedDirectUnrollingCode, and TM.DecidesInTime.mem_UniformPPoly is the unconditional result.

theorem Complexity.TM.DecidesInTime.mem_UniformPPoly_of_paddedDirectUnrollingCode_mem_FL {k : ℕ} {tm : TM k} {L : Language} (q : Polynomial ℕ) (hdec : tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x q) (hgen : (fun (x : List Bool) => tm.paddedDirectUnrollingCode (fun (x : ℕ) => Polynomial.eval x q) x.length) ∈ FL) : L ∈ UniformPPoly

A polynomial-time decider belongs to uniform P/poly whenever its regularly padded exact code map is computable in logarithmic space.

theorem Complexity.P_subset_UniformPPoly_of_directUnrollingCode_mem_FL (hgen : ∀ {k : ℕ} (tm : TM k) (q : Polynomial ℕ), (fun (x : List Bool) => tm.directUnrollingCode (fun (x : ℕ) => Polynomial.eval x q) x.length) ∈ FL) : P ⊆ UniformPPoly

If every polynomial-horizon direct unrolling code map belongs to FL, then every language in P has a logspace-uniform polynomial-size circuit family.

The hypothesis hgen is not known for the unpadded code; the unconditional containment P_subset_UniformPPoly (and UniformPPoly_eq_P) goes through the padded code instead.

theorem Complexity.P_subset_UniformPPoly_of_paddedDirectUnrollingCode_mem_FL (hgen : ∀ {k : ℕ} (tm : TM k) (q : Polynomial ℕ), (fun (x : List Bool) => tm.paddedDirectUnrollingCode (fun (x : ℕ) => Polynomial.eval x q) x.length) ∈ FL) : P ⊆ UniformPPoly

If every polynomial-horizon padded unrolling code map belongs to FL, then every language in P has a logspace-uniform polynomial-size family.

theorem Complexity.TM.paddedDirectUnrollingCode_mem_FL {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (fun (input : List Bool) => tm.paddedDirectUnrollingCode (fun (x : ℕ) => Polynomial.eval x (directSerializerHorizonPolynomial q)) input.length) ∈ FL

The canonical streaming transducer computes every regularly padded direct unrolling code at the normalized polynomial horizon in logarithmic space.

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

Every language decided by a deterministic machine within a polynomial time bound has a logspace-uniform polynomial-size circuit family.

theorem Complexity.P_subset_UniformPPoly : P ⊆ UniformPPoly

Deterministic polynomial time is contained in logspace-uniform P/poly.

theorem Complexity.UniformPPoly_eq_P : UniformPPoly = P

Logspace-uniform polynomial-size circuits characterize deterministic polynomial time.