Canonical CNFs in the imported depth-three model

Literal polarity agrees in both models. Clause conversion removes duplicates, so it preserves evaluation and does not increase width. An OR of CNFs is converted with an exact gate count.

def Complexity.CNF.toDepthThree {n : ℕ} (F : CNF n) : DepthThreeLowerBound.CNF (Fin n)

Convert a canonical CNF to the imported set-of-literals representation.

Equations

• F.toDepthThree = List.map (fun (C : List (Complexity.Literal n)) => (List.map (fun (l : Complexity.Literal n) => (l.var, l.polarity)) C).toFinset) F.clauses

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.Circuit3.BottomIndex {n : ℕ} (Fs : List (Complexity.CNF n)) : Type

A clause occurrence, indexed by its CNF and then its position.

Equations

• Complexity.DepthThreeLowerBound.Circuit3.BottomIndex Fs = ((j : Fin Fs.length) × Fin Fs[j].clauses.length)

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.bottomEquiv {n : ℕ} (Fs : List (Complexity.CNF n)) : Fin (Fintype.card (BottomIndex Fs)) ≃ BottomIndex Fs

Enumerate clause occurrences as numbered bottom gates.

Equations

• Complexity.DepthThreeLowerBound.Circuit3.bottomEquiv Fs = (Fintype.equivFin (Complexity.DepthThreeLowerBound.Circuit3.BottomIndex Fs)).symm

def Complexity.DepthThreeLowerBound.Circuit3.clauseInputs {n : ℕ} (C : List (Complexity.Literal n)) : RawClause (Fin n)

Convert canonical literals to signed gate inputs.

Equations

• Complexity.DepthThreeLowerBound.Circuit3.clauseInputs C = List.map (fun (l : Complexity.Literal n) => Sum.inl (l.var, l.polarity)) C

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.ofCNFs {n : ℕ} (Fs : List (Complexity.CNF n)) : Circuit3 (Fin n)

Realize an OR of canonical CNFs as an unrestricted three-layer circuit.

Equations

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