CNF substitution preserves evaluation and cannot increase width

Every surviving variable comes from the scope of the original clause. The union of these singleton or empty images has at most the original width.

theorem Complexity.DepthThreeLowerBound.Clause.eval_subst_proof {V : Type u_1} {W : Type u_2} (α : V → W ⊕ Bool) (C : Clause V) (x : Cube W) : (Option.map (fun (D : Clause W) => D.eval x) (subst α C)).getD true = C.eval (GateInput.assignment α x)

theorem Complexity.DepthThreeLowerBound.Clause.width_subst_le_proof {V : Type u_1} {W : Type u_2} (α : V → W ⊕ Bool) (C : Clause V) (D : Clause W) (h : subst α C = some D) : D.width ≤ C.width

theorem Complexity.DepthThreeLowerBound.CNF.eval_subst_proof {V : Type u_1} {W : Type u_2} (H : CNF V) (α : V → W ⊕ Bool) (x : Cube W) : (H.subst α).eval x = H.eval (GateInput.assignment α x)

theorem Complexity.DepthThreeLowerBound.CNF.WidthAtMost.subst_proof {V : Type u_1} {W : Type u_2} {H : CNF V} {k : ℕ} (h : H.WidthAtMost k) (α : V → W ⊕ Bool) : (H.subst α).WidthAtMost k