The semantic switching lemma

This module exposes the representation-independent consequence of the canonical DNF switching injection. For a width-t DNF under the independent p-random restriction, the probability that the restricted Boolean function has decision-tree depth at least s is at most (5pt)^s.

The event concerns every decision tree computing the restricted function. The proof does not search for an optimal tree: semantic depth at least s forces the explicitly constructed canonical tree to have depth at least s, after which the canonical switching lemma applies.

theorem Algebraic.AC0.RandomRestriction.probability_depthAtLeast_restrict_le_five {n widthBound : ℕ} (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => DecisionTree.DepthAtLeast (formula.restrict rho).eval pathLength) ≤ (5 * ↑p * ↑widthBound) ^ pathLength

Hastad's switching lemma, decision-tree form. A width-t DNF left under a p-random restriction has semantic decision-tree depth at least s with probability at most (5pt)^s.

Here DecisionTree.DepthAtLeast f s means that every decision tree computing f has depth at least s; in particular, threshold zero is the certain event.

theorem Algebraic.AC0.RandomRestriction.probability_not_depthAtMost_restrict_le_five {n widthBound : ℕ} (formula : DNF n) (bounded : formula.WidthAtMost widthBound) (depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ¬DecisionTree.DepthAtMost (formula.restrict rho).eval depthBound) ≤ (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Equivalent off-by-one form: the probability that the restricted DNF has no computing tree of depth at most depthBound is at most (5pt)^(depthBound + 1).

theorem Algebraic.AC0.RandomRestriction.probability_cnf_depthAtLeast_restrict_le_five {n widthBound : ℕ} (formula : CNF n) (bounded : formula.WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => DecisionTree.DepthAtLeast (formula.restrict rho).eval pathLength) ≤ (5 * ↑p * ↑widthBound) ^ pathLength

Hastad's switching lemma, CNF form. A width-t CNF left under a p-random restriction has semantic decision-tree depth at least s with probability at most (5pt)^s. This is the exact De Morgan dual of the DNF theorem.

theorem Algebraic.AC0.RandomRestriction.probability_cnf_not_depthAtMost_restrict_le_five {n widthBound : ℕ} (formula : CNF n) (bounded : formula.WidthAtMost widthBound) (depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ¬DecisionTree.DepthAtMost (formula.restrict rho).eval depthBound) ≤ (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Equivalent off-by-one CNF form: failure to have a depth-d computing tree has probability at most (5pt)^(d + 1).