Encoded sizes of layered Boolean circuits

The node encoding charges two tag bits, both binary reference positions, and all pair framing. A valid node reading a row of width w needs at most 10 + 3 * (log₂ w + 1) bits. Applying the list framing twice gives an explicit bound for a well-formed schedule whose input and every layer have width at most w. The bounds include zero-width rows and constant nodes.

Main results

• Cslib.Circuits.Boolean.Layered.length_encNode: exact size in terms of both reference words.
• Cslib.Circuits.Boolean.Layered.length_encNode_le: logarithmic size for a valid node.
• Cslib.Circuits.Boolean.Layered.WellFormed.length_encList_le: the complete schedule encoding.

References

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

theorem Cslib.Circuits.Boolean.Layered.length_encNode (node : Node) : (encNode node).length = 10 + 2 * (Turing.MultiTapeTM.encNat node.code.2.1).length + (Turing.MultiTapeTM.encNat node.code.2.2).length

Exact node length: tags and framing cost ten bits; the first binary reference is framed.

theorem Cslib.Circuits.Boolean.Layered.length_encNode_le {node : Node} {width : ℕ} (h : Node.Valid width node) : (encNode node).length ≤ 10 + 3 * (width.log2 + 1)

Valid references have logarithmic binary encodings; the bound also covers constants.

theorem Cslib.Circuits.Boolean.Layered.WellFormed.length_encList_le {inputCount width : ℕ} {layers : List (List Node)} (h : WellFormed inputCount layers) (hinput : inputCount ≤ width) (hlayers : ∀ layer ∈ layers, layer.length ≤ width) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encNode)) layers).length ≤ layers.length * (2 * width * (6 * (width.log2 + 1) + 21) + 1)

A well-formed schedule of bounded width has bounded complete encoding, including every node delimiter and every layer delimiter. The initial input width is bounded separately.