Native codes for the existing half-split balanced circuit

The constructor keeps the exact Circuit.balanced topology, including the order of gate blocks. Its private dynamic program fills contiguous-interval rows in increasing interval length. The loop count is the length of the complete leaf-code list, never a binary arity parameter.

Main definitions

• Cslib.Circuits.Boolean.balancedCode: the complete raw code of a balanced circuit.

Main results

• Cslib.Circuits.Boolean.balancedCode_eq_code: exact agreement with Circuit.balanced.
• Cslib.Circuits.Boolean.computableInPolyTime_balancedCode: uniform construction from binary input arity and native generators of the complete operator, fallback and leaf codes.

The resource proof counts all gates, gate arguments and outputs, including dead gates, and controls the binary lengths of wire references. Thus an arbitrarily large unused input arity does not become a unary resource bound. Every stored interval, invalid-interval fallback, row and table frame is charged; the captured input is charged by the native loop combinator.

References

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

def Cslib.Circuits.Boolean.balancedCode (n : ℕ) (op unit : List (Op × List ℕ) × List ℕ) (leaves : List (List (Op × List ℕ) × List ℕ)) : List (Op × List ℕ) × List ℕ

Generate the exact half-split code on shared inputs. The supplied fallback is returned only for an empty leaf list. Malformed codes are transformed as data, without arity-sized loops.

theorem Cslib.Circuits.Boolean.balancedCode_eq_code {n r : ℕ} (op : Circuit signature (r + r) r) (unit : Circuit signature n r) (leaves : List (Circuit signature n r)) : balancedCode n op.code unit.code (List.map Circuit.code leaves) = (op.balanced unit leaves).code

Exact raw-code agreement, including empty fallback programs, unused operators, dead gates and the existing half-split order of all intermediate gate blocks.

theorem Cslib.Circuits.Boolean.computableInPolyTime_balancedCode {α : Type} {enc : α ↪ List Bool} {n : α → ℕ} {op unit : α → List (Op × List ℕ) × List ℕ} {leaves : α → List (List (Op × List ℕ) × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hop : Turing.MultiTapeTM.ComputableInPolyTime op enc encCode) (hu : Turing.MultiTapeTM.ComputableInPolyTime unit enc encCode) (hl : Turing.MultiTapeTM.ComputableInPolyTime leaves enc (Turing.MultiTapeTM.encList encCode)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => balancedCode (n a) (op a) (unit a) (leaves a)) enc encCode

Uniform native generation from the binary shared-input count and the complete operator, fallback and leaf codes. The derived bound charges every interval row and its list framing; no well-formedness, fixed arity or assumed construction-runtime bound is required.