Polynomial-time compilation into consecutive layers

The certificates follow the actual raw compiler: compute the depth table and selected-output maximum, then generate both microlevels at each depth. The input count and internal enumeration counters are unary; source wire references and emitted node references are binary. Every layer, node, delimiter and output selector is included in the output encoding.

The construction is uniform in the input count, gate count and number of designated outputs. It is polynomial-time on all raw code, without a well-formedness or promised-depth hypothesis.

Main results

• Cslib.Circuits.Boolean.Layered.computableInPolyTime_prepareLayer, computableInPolyTime_finishLayer: generate the two microlevels of a depth.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_schedule: generate all levels.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_compile: compute depths and emit the complete schedule and output selectors.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_carry {α : Type} {input : α ↪ List Bool} {depths : α → List ℕ} {level wire : α → ℕ} (hdepths : Turing.MultiTapeTM.ComputableInPolyTime depths input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) (hlevel : Turing.MultiTapeTM.ComputableInPolyTime level input Turing.MultiTapeTM.encUnary) (hwire : Turing.MultiTapeTM.ComputableInPolyTime wire input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => carry (depths a) (level a) (wire a)) input encNode

Decide whether a unary-numbered wire is already available, then emit its binary copy index.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_prepareFirst {α : Type} {input : α ↪ List Bool} {gate : α → Op × List ℕ} (hgate : Turing.MultiTapeTM.ComputableInPolyTime gate input encGate) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prepareFirst (gate a)) input encNode

Prepare the first intermediate, retaining binary source references.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_prepareSecond {α : Type} {input : α ↪ List Bool} {gate : α → Op × List ℕ} (hgate : Turing.MultiTapeTM.ComputableInPolyTime gate input encGate) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prepareSecond (gate a)) input encNode

Prepare the second intermediate, retaining the binary source reference.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_finish {α : Type} {input : α ↪ List Bool} {inputCount gateCount gateIndex : α → ℕ} {op : α → Op} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hg : Turing.MultiTapeTM.ComputableInPolyTime gateCount input Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime gateIndex input Turing.MultiTapeTM.encUnary) (hop : Turing.MultiTapeTM.ComputableInPolyTime op input encOp) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => finish (inputCount a) (gateCount a) (gateIndex a) (op a)) input encNode

Finish a gate, computing scratch positions in unary before emitting binary indices.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_prepareLayer {α : Type} {input : α ↪ List Bool} {inputCount level : α → ℕ} {gates : α → List (Op × List ℕ)} {depths : α → List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates input (Turing.MultiTapeTM.encList encGate)) (hdepths : Turing.MultiTapeTM.ComputableInPolyTime depths input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) (hlevel : Turing.MultiTapeTM.ComputableInPolyTime level input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prepareLayer (inputCount a) (gates a) (depths a) (level a)) input (Turing.MultiTapeTM.encList encNode)

Generate a preparation layer, charging the complete framed node list.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_finishLayer {α : Type} {input : α ↪ List Bool} {inputCount level : α → ℕ} {gates : α → List (Op × List ℕ)} {depths : α → List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates input (Turing.MultiTapeTM.encList encGate)) (hdepths : Turing.MultiTapeTM.ComputableInPolyTime depths input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) (hlevel : Turing.MultiTapeTM.ComputableInPolyTime level input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => finishLayer (inputCount a) (gates a) (depths a) (level a)) input (Turing.MultiTapeTM.encList encNode)

Generate a finishing layer, including copies and all cleared scratch slots.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_schedule {α : Type} {input : α ↪ List Bool} {inputCount depth : α → ℕ} {gates : α → List (Op × List ℕ)} {depths : α → List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates input (Turing.MultiTapeTM.encList encGate)) (hdepths : Turing.MultiTapeTM.ComputableInPolyTime depths input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) (hdepth : Turing.MultiTapeTM.ComputableInPolyTime depth input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => schedule (inputCount a) (gates a) (depths a) (depth a)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode))

Generate both microlevels at every computed unary depth, charging their full encoding.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_compile {α : Type} {input : α ↪ List Bool} {inputCount : α → ℕ} {code : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableInPolyTime code input encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => compile (inputCount a) (code a)) input encCompiled

Compile arbitrary raw code in native polynomial time. The input count is unary; all source references and output selectors are binary. Depth computation and the entire emitted schedule are included, with no validity premise or fixed input/output arity.