Negation-normal formulas for CSLib unbounded AND/OR circuits

Use the existing wire normalization through a program-only typed adapter. The adapter's unused output does not enter the selected formula, so it adds no depth or formula-size cost.

def Complexity.CslibAC0.lineGate {n g : ℕ} (l : Cslib.Circuits.Line Basis.unboundedAndOr.signature n g) : Gate Basis.unboundedAndOr (n + g)

A CSLib line read through the typed circuit wire numbering.

Equations

• Complexity.CslibAC0.lineGate l = { op := l.op.op, fanIn := l.op.fanIn, arityOk := ⋯, inputs := fun (a : Fin l.op.fanIn) => (l.wires a).index, negated := l.op.negated }

def Complexity.CslibAC0.asTyped {n g : ℕ} [NeZero n] (p : Cslib.Circuits.Program Basis.unboundedAndOr.signature n g) : Circuit Basis.unboundedAndOr n 1 g

Use the existing typed wire normalizer on a CSLib program. The auxiliary output is unused.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CslibAC0.outputFormula {n : ℕ} [NeZero n] (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1) : AC0Formula n

Unfold a CSLib output to a negation-normal formula, removing repeated signed wires.

Equations

• Complexity.CslibAC0.outputFormula c = (Complexity.CslibAC0.asTyped c.program).wireAC0Formula false (c.outputs 0).index