Deterministic unrolling into uniform P/poly -- proof internals

This module packages the direct deterministic unrolling family first through conditional FL seams and then through the verified canonical padded serializer, yielding the unconditional machines-to-circuits containment.

theorem Complexity.TM.DecidesInTime.mem_UniformPPoly_of_directUnrollingCode_mem_FL_internal {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

Internal packaging of one polynomial-time decider and its direct-code generator as a logspace-uniform polynomial-size circuit family.

theorem Complexity.TM.DecidesInTime.mem_UniformPPoly_of_paddedDirectUnrollingCode_mem_FL_internal {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

Internal packaging through the regularly padded family. Unlike the direct family, its positive gate-count header is a closed polynomial expression.

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

Internal conditional containment: if every polynomial-horizon direct unrolling code map belongs to FL, then P is contained in uniform P/poly.

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

Internal conditional containment through the padded exact-code target.

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

Internal FL witness for the regularly padded serializer at the normalized polynomial horizon.

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

Internal unconditional packaging of one polynomial-time decider as a logspace-uniform polynomial-size circuit family.

theorem Complexity.P_subset_UniformPPoly_internal : P ⊆ UniformPPoly

Internal machines-to-uniform-circuits containment.

theorem Complexity.UniformPPoly_eq_P_internal : UniformPPoly = P

Internal logspace-uniform circuit characterization of deterministic polynomial time.