Polynomial-time padding of layered Boolean circuits

The input width and target layer count use unary encodings. Existing and generated node references use binary encodings, and the full nested list encoding charges every copied node and layer delimiter. The certificates apply to all schedules, including invalid references and schedules longer than the target.

Main results

• Cslib.Circuits.Boolean.Layered.computableInPolyTime_identityLayer: generate a row of binary-indexed copies from a unary width.
• Cslib.Circuits.Boolean.Layered.computableInPolyTime_padTo: compute the final width and append the actual copy layers in uniform polynomial time.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_identityLayer {α : Type} {input : α ↪ List Bool} {width : α → ℕ} (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => identityLayer (width a)) input (Turing.MultiTapeTM.encList encNode)

Enumerate the row in unary and encode each copy node's wire index in binary.

theorem Cslib.Circuits.Boolean.Layered.computableInPolyTime_padTo {α : Type} {input : α ↪ List Bool} {inputCount target : α → ℕ} {layers : α → List (List Node)} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (htarget : Turing.MultiTapeTM.ComputableInPolyTime target input Turing.MultiTapeTM.encUnary) (hlayers : Turing.MultiTapeTM.ComputableInPolyTime layers input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => padTo (inputCount a) (target a) (layers a)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode))

Padding is polynomial in the complete encoded input, including its unary target.