Normalizing unbounded AND/OR circuits to negation-normal formulas

Each gate first replaces its arbitrarily long input table by the finite set of distinct signed source wires. This is semantically exact because AND and OR are idempotent. It also closes an important quantitative loophole: the circuit model counts gates rather than wire incidences, so duplicate inputs must not inflate the normalized formula.

def Complexity.Gate.signedSupport {W : ℕ} (gate : Gate Basis.unboundedAndOr W) (outerNegated : Bool) : Finset (Fin W × Bool)

The distinct signed source wires read by a gate, after composing every edge-negation flag with an optional outer negation.

Equations

• gate.signedSupport outerNegated = Finset.image (fun (input : Fin gate.fanIn) => (gate.inputs input, outerNegated ^^ gate.negated input)) Finset.univ

@[irreducible]

noncomputable def Complexity.Circuit.wireAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (negated : Bool) (wire : Fin (N + G)) : AC0Formula N

Unfold one circuit wire into a negation-normal unbounded formula.

The negated parameter requests either the wire value or its complement. De Morgan duality pushes that request through every gate, so negation reaches only input literals. Distinct signed gate inputs are used exactly once.

Equations

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

noncomputable def Complexity.Circuit.outputAC0Formula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.unboundedAndOr N M G) (output : Fin M) : AC0Formula N

Normalize one selected output gate to a negation-normal unbounded formula.

Equations

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