Semantic and width guarantees for CNF input substitution

These lemmas transport OpenAI's hard-slice correlation bounds to representations of its full language. Constants and repeated target variables are both allowed.

theorem Complexity.DepthThreeLowerBound.Clause.eval_subst {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)

A substituted clause agrees with the original on the induced assignment.

theorem Complexity.DepthThreeLowerBound.Clause.width_subst_le {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

Substituting constants or identifying variables cannot increase clause width.

theorem Complexity.DepthThreeLowerBound.CNF.eval_subst {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)

A substituted CNF agrees with the original on the induced assignment.

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

Input substitution preserves every clause-width bound.