De Morgan duality for bounded normal forms

Negating every literal turns a term into its complementary clause and a clause into its complementary term. Mapping this operation across the outer list gives exact DNF/CNF duals. This module proves semantic complementation, width preservation, compatibility with restriction, and invariance of semantic decision-tree depth under output negation.

def Algebraic.AC0.LiteralSet.negate {n : ℕ} (set : LiteralSet n) : LiteralSet n

Flip the satisfying value of every literal in a literal set.

Equations

• set.negate = { requirements := fun (index : Fin n) => Option.map (fun (value : Bool) => !value) (set.requirements index) }

@[simp]

theorem Algebraic.AC0.LiteralSet.negate_requirements {n : ℕ} (set : LiteralSet n) (index : Fin n) : set.negate.requirements index = Option.map (fun (value : Bool) => !value) (set.requirements index)

@[simp]

theorem Algebraic.AC0.LiteralSet.negate_negate {n : ℕ} (set : LiteralSet n) : set.negate.negate = set

@[simp]

theorem Algebraic.AC0.LiteralSet.support_negate {n : ℕ} (set : LiteralSet n) : set.negate.support = set.support

@[simp]

theorem Algebraic.AC0.LiteralSet.width_negate {n : ℕ} (set : LiteralSet n) : set.negate.width = set.width

theorem Algebraic.AC0.LiteralSet.negate_hitBy_iff_conflictsWith {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : set.negate.HitBy rho ↔ set.ConflictsWith rho

A fixed value satisfies a negated literal exactly when it conflicts with the source literal.

theorem Algebraic.AC0.LiteralSet.negate_conflictsWith_iff_hitBy {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : set.negate.ConflictsWith rho ↔ set.HitBy rho

A fixed value conflicts with a negated literal exactly when it satisfies the source literal.

theorem Algebraic.AC0.LiteralSet.residual_negate {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : set.negate.residual rho = (set.residual rho).negate

Removing fixed coordinates commutes with literal negation.

@[simp]

theorem Algebraic.AC0.Clause.eval_negate_term {n : ℕ} (term : Term n) (input : Fin n → Bool) : eval (LiteralSet.negate term) input = !term.eval input

A clause made of the negated literals is true exactly when the source term is false.

theorem Algebraic.AC0.Clause.restrict_negate_term {n : ℕ} (term : Term n) (rho : PartialAssignment n) : restrict (LiteralSet.negate term) rho = Option.map LiteralSet.negate (term.restrict rho)

Clause restriction of a negated term is the negation of term restriction.

@[simp]

theorem Algebraic.AC0.Term.eval_negate_clause {n : ℕ} (clause : Clause n) (input : Fin n → Bool) : eval (LiteralSet.negate clause) input = !clause.eval input

A term made of the negated literals is true exactly when the source clause is false.

theorem Algebraic.AC0.Term.restrict_negate_clause {n : ℕ} (clause : Clause n) (rho : PartialAssignment n) : restrict (LiteralSet.negate clause) rho = Option.map LiteralSet.negate (clause.restrict rho)

Term restriction of a negated clause is the negation of clause restriction.

def Algebraic.AC0.DNF.negate {n : ℕ} (formula : DNF n) : CNF n

De Morgan dual of a DNF: negate every term into a clause.

Equations

• formula.negate = { clauses := List.map Algebraic.AC0.LiteralSet.negate formula.terms }

@[simp]

theorem Algebraic.AC0.DNF.negate_clauses {n : ℕ} (formula : DNF n) : formula.negate.clauses = List.map LiteralSet.negate formula.terms

@[simp]

theorem Algebraic.AC0.DNF.eval_negate {n : ℕ} (formula : DNF n) (input : Fin n → Bool) : formula.negate.eval input = !formula.eval input

De Morgan duality complements DNF semantics.

theorem Algebraic.AC0.DNF.WidthAtMost.negate {n : ℕ} {formula : DNF n} {bound : ℕ} (bounded : formula.WidthAtMost bound) : formula.negate.WidthAtMost bound

De Morgan duality preserves a width bound.

def Algebraic.AC0.CNF.negate {n : ℕ} (formula : CNF n) : DNF n

De Morgan dual of a CNF: negate every clause into a term.

Equations

• formula.negate = { terms := List.map Algebraic.AC0.LiteralSet.negate formula.clauses }

@[simp]

theorem Algebraic.AC0.CNF.negate_terms {n : ℕ} (formula : CNF n) : formula.negate.terms = List.map LiteralSet.negate formula.clauses

@[simp]

theorem Algebraic.AC0.CNF.eval_negate {n : ℕ} (formula : CNF n) (input : Fin n → Bool) : formula.negate.eval input = !formula.eval input

De Morgan duality complements CNF semantics.

theorem Algebraic.AC0.CNF.WidthAtMost.negate {n : ℕ} {formula : CNF n} {bound : ℕ} (bounded : formula.WidthAtMost bound) : formula.negate.WidthAtMost bound

De Morgan duality preserves a width bound.

@[simp]

theorem Algebraic.AC0.DNF.negate_negate {n : ℕ} (formula : DNF n) : formula.negate.negate = formula

@[simp]

theorem Algebraic.AC0.CNF.negate_negate {n : ℕ} (formula : CNF n) : formula.negate.negate = formula

theorem Algebraic.AC0.DNF.negate_restrict {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) : (formula.restrict rho).negate = formula.negate.restrict rho

DNF restriction commutes exactly with De Morgan duality.

theorem Algebraic.AC0.CNF.negate_restrict {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) : (formula.restrict rho).negate = formula.negate.restrict rho

CNF restriction commutes exactly with De Morgan duality.

theorem Algebraic.AC0.DecisionTree.DepthAtMost.negate {n : ℕ} {function : ScalarFunction Bool n} {bound : ℕ} (bounded : DepthAtMost function bound) : DepthAtMost (fun (input : Fin n → Bool) => !function input) bound

Negating all leaves preserves an upper bound on semantic decision-tree depth.

@[simp]

theorem Algebraic.AC0.DecisionTree.depthAtMost_negate_iff {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : DepthAtMost (fun (input : Fin n → Bool) => !function input) bound ↔ DepthAtMost function bound

Semantic upper decision-tree depth is invariant under output negation.

theorem Algebraic.AC0.DecisionTree.DepthAtLeast.negate {n : ℕ} {function : ScalarFunction Bool n} {bound : ℕ} (lower : DepthAtLeast function bound) : DepthAtLeast (fun (input : Fin n → Bool) => !function input) bound

Negating all leaves preserves a lower bound on semantic decision-tree depth.

@[simp]

theorem Algebraic.AC0.DecisionTree.depthAtLeast_negate_iff {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : DepthAtLeast (fun (input : Fin n → Bool) => !function input) bound ↔ DepthAtLeast function bound

Semantic lower decision-tree depth is invariant under output negation.