Documentation

Complexitylib.Algebraic.LowerBound.AC0.ParitySeparation

Parity is not in AC0 #

This module passes from the finite switching-lemma tradeoff to the qualitative complexity-class separation. Given fixed polynomial cost and fixed logical depth bounds, choose the diagonal input width

n = (20 * (t + 1))^(d - 1).

The finite theorem forces 2^(t+1) <= 20 * t * S(n), while substituting this input width into the polynomial upper bound leaves a fixed polynomial in t. The latter is eventually at most 2^t, giving a contradiction.

The reusable family theorem works directly for arbitrary internal NOT gates: the switching argument follows free NOT chains semantically and charges only AND/OR gates. The checked AC0.Computable endpoint is retained as a specialization, while AC0.RawComputable now follows without dual-rail normalization or its factor-two cost expansion.

source
def Algebraic.AC0.ParityParameters.diagonalInput (depth scale : ℕ) :
ℕ

The input width used to diagonalize against fixed size and depth bounds.

Equations
Instances For
    source
    theorem Algebraic.AC0.ParityParameters.scaledPolynomial_le (coefficient degree depth scale : ℕ) (scalePositive : 0 < scale) :
    20 * scale * (coefficient * (diagonalInput depth scale + 1) ^ degree) ≤ 20 * coefficient * (2 * 40 ^ (depth - 1)) ^ degree * scale ^ ((depth - 1) * degree + 1)

    Substituting the diagonal input width into a fixed polynomial gives a fixed polynomial in the scale parameter. The constants are deliberately coarse; only their independence from scale matters.

    source
    theorem Algebraic.AC0.Family.not_computes_parity_raw (family : Circuit.Family signature 1) (polynomialCost : family.HasPolynomialCost andOrCost) (constantDepth : HasConstantLogicalDepth family) :
    ¬family.Computes interpretation Parity.targetFamily

    No family with polynomial AND/OR cost and constant logical depth computes parity at every input width, even when NOT gates occur at arbitrary internal wires.

    source
    theorem Algebraic.AC0.Family.not_computes_parity (family : Circuit.Family signature 1) (polynomialCost : family.HasPolynomialCost andOrCost) (constantDepth : HasConstantLogicalDepth family) (_negationsAtInputs : ∀ (n : ℕ), Program.NegationsAtInputs (family.circuit n).program) :
    ¬family.Computes interpretation Parity.targetFamily

    Compatibility specialization to families with checked input-level negations.

    source
    theorem Algebraic.AC0.parity_not_computable :
    ¬Computable Parity.targetFamily

    The parity target family is not computable by nonuniform AC0 as defined by the library's checked source model.

    source
    theorem Algebraic.AC0.parity_not_raw_computable :
    ¬RawComputable Parity.targetFamily

    Parity is not computable even in the raw presentation that allows NOT gates at arbitrary internal wires. This conclusion is now direct and does not pass through dual-rail normalization.