Documentation

Complexitylib.Algebraic.LowerBound.AC0.ParityRoot

Root-selected quantitative AC0 parity lower bound #

This module selects a canonical scale from Mathlib's verified natural-number nthRoot. Let

q = Nat.nthRoot (d - 1) n / 20

and use t = q - 1. Once 40^(d-1) <= n, one has q >= 2 and 20 * (t + 1) <= Nat.nthRoot (d - 1) n, so the scale theorem applies. Every depth-d parity circuit, even with arbitrary internal NOT gates, then satisfies

2^q <= 20 * (q - 1) * S.

This is a conventional explicit form of the exp(Omega(n^(1/(d-1)))) lower bound, with conservative constants chosen for the exact first-moment proof. Root selection is symbolic and uniform; it does not enumerate circuits or run bounded experiments.

source
def Algebraic.AC0.ParityParameters.rootQuotient (n depth : ℕ) :
ℕ

The integer root, divided by the scale constant.

Equations
Instances For
    source
    def Algebraic.AC0.ParityParameters.rootScale (n depth : ℕ) :
    ℕ

    Target tree depth obtained by reserving one unit below the root quotient.

    Equations
    Instances For
      source
      theorem Algebraic.AC0.ParityParameters.rootQuotient_two_le (n depth : ℕ) (twoLeDepth : 2 ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      2 ≤ rootQuotient n depth

      Above the explicit threshold, the root quotient is at least two.

      source
      theorem Algebraic.AC0.ParityParameters.one_le_rootScale (n depth : ℕ) (twoLeDepth : 2 ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      1 ≤ rootScale n depth

      The selected tree depth is positive above the threshold.

      source
      theorem Algebraic.AC0.ParityParameters.rootScale_succ (n depth : ℕ) (twoLeDepth : 2 ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      rootScale n depth + 1 = rootQuotient n depth

      Adding back the reserved unit recovers the root quotient.

      source
      theorem Algebraic.AC0.ParityParameters.twenty_mul_rootScale_succ_le_nthRoot (n depth : ℕ) (twoLeDepth : 2 ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      20 * (rootScale n depth + 1) ≤ (depth - 1).nthRoot n

      The scaled selected depth lies below the verified integer root.

      source
      theorem Algebraic.AC0.ParityParameters.rootScale_inputLarge (n depth : ℕ) (twoLeDepth : 2 ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      (20 * (rootScale n depth + 1)) ^ (depth - 1) ≤ n

      The root-selected scale satisfies the input-size premise of the scale theorem.

      source
      theorem Algebraic.AC0.Circuit.parity_size_tradeoff_at_root_raw {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      2 ^ ParityParameters.rootQuotient n depth ≤ 20 * ParityParameters.rootScale n depth * Program.cost andOrCost circuit.program

      Root-selected product-form lower bound for depth-d parity circuits, allowing arbitrary internal NOT gates at zero cost.

      source
      theorem Algebraic.AC0.Circuit.parity_size_tradeoff_at_root {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      2 ^ ParityParameters.rootQuotient n depth ≤ 20 * ParityParameters.rootScale n depth * Program.cost andOrCost circuit.program

      Compatibility wrapper for the checked input-negation presentation.

      source
      theorem Algebraic.AC0.Circuit.parity_andOrCost_lower_bound_at_root_raw {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      2 ^ ParityParameters.rootQuotient n depth / (20 * ParityParameters.rootScale n depth) ≤ Program.cost andOrCost circuit.program

      Root-selected lower bound with the AND/OR cost isolated by natural-number floor division, allowing arbitrary internal NOT gates at zero cost.

      source
      theorem Algebraic.AC0.Circuit.parity_andOrCost_lower_bound_at_root {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (inputLarge : 40 ^ (depth - 1) ≤ n) :
      2 ^ ParityParameters.rootQuotient n depth / (20 * ParityParameters.rootScale n depth) ≤ Program.cost andOrCost circuit.program

      Compatibility wrapper for the checked input-negation presentation.