Balanced padding and the dual depth-three polarity

Use the existing balanced padding: XOR the original verdict with a fresh first bit. The same three-layer wiring represents an AND-OR-AND circuit by complementing every input literal and constant and exchanging AND with OR.

noncomputable def Complexity.DepthThreeLowerBound.balancedLanguage (w : List Bool) : Bool

XOR the language on the tail with the first input bit, defaulting to false.

Equations

• Complexity.DepthThreeLowerBound.balancedLanguage w = (Complexity.DepthThreeLowerBound.language w.tail ^^ w.headD false)

noncomputable def Complexity.DepthThreeLowerBound.balancedFamily (n : ℕ) : Cube (Fin (n + 1)) → Bool

The exactly balanced extension of the hard length-n function.

Equations

• Complexity.DepthThreeLowerBound.balancedFamily n = Algebraic.Cutwidth.balancePad fun (x : Cslib.BitString n) => Complexity.DepthThreeLowerBound.language (List.ofFn x)

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.dualEval {V : Type u_1} (C : Circuit3 V) (x : Cube V) : Bool

Evaluate the same wiring as AND-OR-AND with every bottom input complemented.

Equations

• C.dualEval x = decide (∀ j ∈ C.top, ∃ i ∈ C.middle j, ∀ l ∈ C.bottom i, l.eval x = false)

def Complexity.DepthThreeLowerBound.Circuit3.ComputesDual {V : Type u_1} (C : Circuit3 V) (f : Cube V → Bool) : Prop

The AND-OR-AND interpretation agrees with the specified Boolean function.

Equations

• C.ComputesDual f = ∀ (x : Complexity.DepthThreeLowerBound.Cube V), C.dualEval x = f x