Documentation

Complexitylib.Algebraic.LowerBound.AC0.ParityNormalForm

Normal-form width lower bounds for restricted parity #

This module proves the final structural obstruction in the standard parity lower-bound argument. If a DNF computes parity after a restriction with at least one live variable, some term contains every live variable. Dually, if a CNF computes that restricted parity, some clause contains every live variable. Consequently either normal form has width at least the live count.

The proof uses sensitivity rather than counting formulas. Starting from an input on which restricted parity has the relevant truth value, a witnessing term or falsified clause must mention every live variable: otherwise flipping an absent live variable would preserve the witness while changing parity. This is uniform in the arity and contains no finite search.

source
def Algebraic.AC0.Parity.UpToNegation {n : ℕ} (candidate : ScalarFunction Bool n) :
Prop

A Boolean function is parity up to a possible output negation. This is the invariant preserved while following a chain of internal NOT gates.

Equations
Instances For
    source
    theorem Algebraic.AC0.Parity.upToNegation_self {n : ℕ} :
    UpToNegation (function n)

    Parity itself is parity up to output negation.

    source
    theorem Algebraic.AC0.Parity.UpToNegation.negate {n : ℕ} {candidate : ScalarFunction Bool n} (phase : UpToNegation candidate) :
    UpToNegation fun (input : Fin n → Bool) => !candidate input

    The parity-up-to-negation predicate is closed under output negation.

    source
    @[simp]
    theorem Algebraic.AC0.Parity.upToNegation_negate_iff {n : ℕ} (candidate : ScalarFunction Bool n) :
    (UpToNegation fun (input : Fin n → Bool) => !candidate input) ↔ UpToNegation candidate

    Output negation does not change whether a function is parity up to negation.

    source
    theorem Algebraic.AC0.Parity.exists_restrict_eq_true_of_live {n : ℕ} (rho : PartialAssignment n) (selected : Fin n) (live : selected ∈ rho.liveVariables) :
    ∃ (input : Fin n → Bool), (function n).restrict rho input = true

    Restricted parity attains true whenever at least one selected coordinate is live.

    source
    theorem Algebraic.AC0.Parity.exists_restrict_eq_false_of_live {n : ℕ} (rho : PartialAssignment n) (selected : Fin n) (live : selected ∈ rho.liveVariables) :
    ∃ (input : Fin n → Bool), (function n).restrict rho input = false

    Restricted parity attains false whenever at least one selected coordinate is live.

    source
    theorem Algebraic.AC0.DNF.exists_term_covering_liveVariables_of_computes_parity {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (liveNonempty : rho.liveVariables.Nonempty) (computes : ∀ (input : Fin n → Bool), formula.eval input = (Parity.function n).restrict rho input) :
    ∃ term ∈ formula.terms, rho.liveVariables ⊆ LiteralSet.support term

    Every DNF computing nonconstant restricted parity contains a term whose support covers all live variables.

    source
    theorem Algebraic.AC0.DNF.liveCount_le_width_of_computes_parity {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (bound : ℕ) (bounded : formula.WidthAtMost bound) (computes : ∀ (input : Fin n → Bool), formula.eval input = (Parity.function n).restrict rho input) :
    rho.liveCount ≤ bound

    A bounded-width DNF computing restricted parity leaves no more live variables than its width.

    source
    theorem Algebraic.AC0.CNF.exists_clause_covering_liveVariables_of_computes_parity {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) (liveNonempty : rho.liveVariables.Nonempty) (computes : ∀ (input : Fin n → Bool), formula.eval input = (Parity.function n).restrict rho input) :
    ∃ clause ∈ formula.clauses, rho.liveVariables ⊆ LiteralSet.support clause

    Every CNF computing nonconstant restricted parity contains a clause whose support covers all live variables.

    source
    theorem Algebraic.AC0.CNF.liveCount_le_width_of_computes_parity {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) (bound : ℕ) (bounded : formula.WidthAtMost bound) (computes : ∀ (input : Fin n → Bool), formula.eval input = (Parity.function n).restrict rho input) :
    rho.liveCount ≤ bound

    A bounded-width CNF computing restricted parity leaves no more live variables than its width.

    source
    theorem Algebraic.AC0.DNF.liveCount_le_width_of_computes_parityUpToNegation {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (bound : ℕ) (bounded : formula.WidthAtMost bound) (candidate : ScalarFunction Bool n) (phase : Parity.UpToNegation candidate) (computes : ∀ (input : Fin n → Bool), formula.eval input = candidate.restrict rho input) :
    rho.liveCount ≤ bound

    The width obstruction is insensitive to complementing parity's output.

    source
    theorem Algebraic.AC0.CNF.liveCount_le_width_of_computes_parityUpToNegation {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) (bound : ℕ) (bounded : formula.WidthAtMost bound) (candidate : ScalarFunction Bool n) (phase : Parity.UpToNegation candidate) (computes : ∀ (input : Fin n → Bool), formula.eval input = candidate.restrict rho input) :
    rho.liveCount ≤ bound

    The width obstruction is insensitive to complementing parity's output.