30 Boolean Analysis — Normal Form Conversion

30.1 Overview

This module bridges the depth-2 Boolean circuit representation (NAndCircuit / NOrCircuit built from literals BoolCircuit.Lit) and the DNF/CNF normal forms used by the switching lemma. It defines the conversion of circuit literals and clauses into switching-lemma terms, and proves that these conversions preserve evaluation, term width, and the structural hypotheses (no repeated indices, variable-injectivity) required downstream.

30.2 Declarations

Definition 30.1 Convert a circuit literal to a switching-lemma literal

✓

Maps a Boolean-circuit literal \(l : \texttt{BoolCircuit.Lit}\, n\) to the corresponding switching-lemma \(\texttt{Literal}\, n\), recording the same variable index and polarity.

Theorem 30.2 Conversion preserves literal evaluation

✓

For every literal \(l\) and input \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the circuit evaluation \(l.\mathrm{eval}\, x\) equals the evaluation of its converted literal \(l.\mathrm{toLiteral}.\mathrm{eval}\, x\).

Definition 30.3 AND-clause to a term

✓

Sends an AND-clause \(\texttt{NAndCircuit}.\mathrm{clause}\, lits\) to the \(\texttt{Term}\) (a conjunction of literals) obtained by mapping each circuit literal through Lit.toLiteral.

Definition 30.4 OR-clause to a term

✓

Sends an OR-clause \(\texttt{NOrCircuit}.\mathrm{clause}\, lits\) to the \(\texttt{Term}\) obtained by mapping each circuit literal through Lit.toLiteral; this term plays the role of one CNF clause (a disjunction of literals).

Definition 30.5 Depth-2 OR-circuit to a DNF

✓

Converts a depth-2 \(\texttt{NOrCircuit}\) (an OR of AND-clauses) into a \(\texttt{DNF}\), the list of terms obtained by converting each AND-clause via NAndCircuit.clauseToTerm; a bare clause maps to the empty DNF.

Definition 30.6 Depth-2 AND-circuit to a CNF

✓

Converts a depth-2 \(\texttt{NAndCircuit}\) (an AND of OR-clauses) into a \(\texttt{CNF}\), the list of clauses obtained by converting each OR-clause via NOrCircuit.clauseToTerm; a bare clause maps to the empty CNF.

Theorem 30.7 Conjunction of literals evaluates as a term

✓

For any list of literals \(lits\) and input \(x\), the right fold of \(\& \& \) over the literal evaluations (starting from \(\mathrm{true}\)) equals the term evaluation \(\texttt{Term.eval}\, (lits.\mathrm{map}\, \texttt{Lit.toLiteral})\, x\).

Theorem 30.8 Disjunction of literals evaluates as a CNF clause

✓

For any list of literals \(lits\) and input \(x\), the right fold of \(||\) over the literal evaluations (starting from \(\mathrm{false}\)) equals the CNF clause evaluation \(\texttt{CNF.evalClause}\, (lits.\mathrm{map}\, \texttt{Lit.toLiteral})\, x\).

Theorem 30.9 Depth-2 OR-circuit evaluates as its DNF

✓

If every child \(c\) of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause, then for all \(x\) the circuit evaluation \((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{eval}\, x\) equals the DNF evaluation \(\texttt{DNF.eval}\, ((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{toDNF})\, x\).

Theorem 30.10 Depth-2 AND-circuit evaluates as its CNF

✓

If every child \(c\) of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause, then for all \(x\) the circuit evaluation \((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{eval}\, x\) equals the CNF evaluation \(\texttt{CNF.eval}\, ((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{toCNF})\, x\).

Theorem 30.11 Converted AND-clause has no repeated indices

✓

If the variable indices of an AND-clause’s literals are pairwise distinct, then the converted term \((\texttt{NAndCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm}\) has the Nodup property.

Theorem 30.12 Variable-injectivity of a converted AND-clause

✓

If the literal indices of an AND-clause are distinct, then within the converted term any two literals sharing the same variable are equal.

Theorem 30.13 Converted OR-clause has no repeated indices

✓

If the variable indices of an OR-clause’s literals are pairwise distinct, then the converted term \((\texttt{NOrCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm}\) has the Nodup property.

Theorem 30.14 Variable-injectivity of a converted OR-clause

✓

If the literal indices of an OR-clause are distinct, then within the converted term any two literals sharing the same variable are equal.

Theorem 30.15 Width of a converted AND-clause

✓

The width of the term obtained from an AND-clause equals the number of its literals: \(\texttt{Term.width}\, (\texttt{NAndCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm} = lits.\mathrm{length}\).

Theorem 30.16 Width of a converted OR-clause

✓

The width of the term obtained from an OR-clause equals the number of its literals: \(\texttt{Term.width}\, (\texttt{NOrCircuit}.\mathrm{clause}\, lits\, h).\mathrm{clauseToTerm} = lits.\mathrm{length}\).

Theorem 30.17 Width bound for the DNF of a depth-2 OR-circuit

✓

If every AND-clause child has at most \(w\) literals (with distinct indices), then the DNF \((\texttt{NOrCircuit}.\mathrm{node}\, cs).\mathrm{toDNF}\) has width at most \(w\).

Theorem 30.18 Width bound for the CNF of a depth-2 AND-circuit

✓

If every OR-clause child has at most \(w\) literals (with distinct indices), then the CNF \((\texttt{NAndCircuit}.\mathrm{node}\, cs).\mathrm{toCNF}\) has width at most \(w\).

Theorem 30.19 DNF terms of a depth-2 OR-circuit have no repeated indices

✓

If every child of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause with distinct literal indices, then every term in the resulting DNF has the Nodup property.

Theorem 30.20 Variable-injectivity of the DNF of a depth-2 OR-circuit

✓

If every child of an \(\texttt{NOrCircuit}.\mathrm{node}\, cs\) is an AND-clause with distinct literal indices, then in every term of the resulting DNF any two literals on the same variable are equal.

Theorem 30.21 CNF clauses of a depth-2 AND-circuit have no repeated indices

✓

If every child of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause with distinct literal indices, then every clause in the resulting CNF has the Nodup property.

Theorem 30.22 Variable-injectivity of the CNF of a depth-2 AND-circuit

✓

If every child of an \(\texttt{NAndCircuit}.\mathrm{node}\, cs\) is an OR-clause with distinct literal indices, then in every clause of the resulting CNF any two literals on the same variable are equal.