31 Boolean Analysis — Recursive Reduction
31.1 Overview
This module collects the helper lemmas used in the recursive proof of the LMN circuit reduction. It relates restrictions, the structural parameters of a circuit (depth, size, fan-in) to those of its children, expresses the evaluation of an AND/OR node under a restriction, and combines compression with the switching lemma to bound the decision-tree depth of a node after a further random restriction.
31.2 Declarations
If a node circuit \(\mathrm{node}\, \mathit{isAnd}\, cs\) has depth at most \(d\), then every child \(c \in cs\) has depth at most \(d - 1\).
If a node circuit \(\mathrm{node}\, \mathit{isAnd}\, cs\) has size at most \(s\), then the sum of the sizes of its children is at most \(s - 1\).
If a node circuit \(\mathrm{node}\, \mathit{isAnd}\, cs\) has maximum fan-in at most \(w\), then every child \(c \in cs\) has maximum fan-in at most \(w\).
If a node circuit \(\mathrm{node}\, \mathit{isAnd}\, cs\) has size at most \(s\), then every child \(c \in cs\) has size at most \(s - 1\).
The restriction of the evaluation of a node circuit equals the conjunction or disjunction, according to \(\mathit{isAnd}\), of the restricted evaluations of its children. That is, \(\mathrm{restrictFn}\, (\mathrm{eval}\, (\mathrm{node}\, \mathit{isAnd}\, cs))\, \rho \) sends \(x\) to the fold-\(\mathrm{and}\) over \(cs\) of \(\mathrm{restrictFn}\, c.\mathrm{eval}\, \rho \, x\) when \(\mathit{isAnd}\) is true, and to the corresponding fold-\(\mathrm{or}\) otherwise.
If every child \(c \in cs\) satisfies \(\mathrm{dtDepth}(\mathrm{restrictFn}\, c.\mathrm{eval}\, \rho ) \le l\), then there is a CNF \(\psi \) of width at most \(l\) that computes the restriction of the AND node: \(\mathrm{CNF.eval}\, \psi \, x = \mathrm{restrictFn}\, (\mathrm{eval}\, (\mathrm{node}\, \mathrm{true}\, cs))\, \rho \, x\) for all \(x\).
If every child \(c \in cs\) satisfies \(\mathrm{dtDepth}(\mathrm{restrictFn}\, c.\mathrm{eval}\, \rho ) \le l\), then there is a DNF \(\varphi \) of width at most \(l\) that computes the restriction of the OR node: \(\mathrm{DNF.eval}\, \varphi \, x = \mathrm{restrictFn}\, (\mathrm{eval}\, (\mathrm{node}\, \mathrm{false}\, cs))\, \rho \, x\) for all \(x\).
Suppose \(0 \lt l\), \(0 \lt n\), and every child \(c \in cs\) satisfies \(\mathrm{dtDepth}(\mathrm{restrictFn}\, c.\mathrm{eval}\, \rho _1) \le l\). Then under a further Bernoulli random restriction \(\rho _2\) with parameter \(1/(40 l)\), the probability that the restricted node \(\mathrm{restrictFn}\, (\mathrm{eval}\, (\mathrm{node}\, \mathit{isAnd}\, cs))\, (\mathrm{composeRestr}\, \rho _1\, \rho _2)\) has decision-tree depth greater than \(t\) is at most