Documentation

Complexitylib.Algebraic.LowerBound.AC0.ParitySurvivors

Integer survivor schedules for parity depth reduction #

The probabilistic schedule retains a real fraction of the live variables, but the layer theorem requires natural-number targets. This module uses ordinary floor division: divide once by 20, then by 20t at every later round.

The schedule is antitone, lies below the corresponding real retained ratio at each step, and has the exact closed form

a_(i+1) = n / (20 * (20*t)^i).

These are symbolic rounding lemmas. No parameter enumeration or numerical experiment is involved.

source
def Algebraic.AC0.ParityParameters.retentionDivisor (t : ℕ) :
ℕ → ℕ

First-round and later-round integer divisors.

Equations
Instances For
    source
    def Algebraic.AC0.ParityParameters.retained (n t : ℕ) :
    ℕ → ℕ

    Integer survivor targets obtained by iterated floor division.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.AC0.ParityParameters.retained_zero (n t : ℕ) :
      retained n t 0 = n
      source
      @[simp]
      theorem Algebraic.AC0.ParityParameters.retained_succ (n t level : ℕ) :
      retained n t (level + 1) = retained n t level / retentionDivisor t level
      source
      theorem Algebraic.AC0.ParityParameters.retained_succ_le (n t level : ℕ) :
      retained n t (level + 1) ≤ retained n t level

      Each floor-division step can only decrease the target.

      source
      theorem Algebraic.AC0.ParityParameters.retained_antitone (n t : ℕ) :
      Antitone (retained n t)

      The integer survivor schedule is antitone in the round number.

      source
      theorem Algebraic.AC0.ParityParameters.retained_positive_of_final (n t : ℕ) {level rounds : ℕ} (levelLe : level ≤ rounds) (finalPositive : 0 < retained n t rounds) :
      0 < retained n t level

      Positivity of a later survivor target implies positivity at every earlier round.

      source
      theorem Algebraic.AC0.ParityParameters.retained_closed (n t level : ℕ) :
      retained n t (level + 1) = n / (20 * (20 * t) ^ level)

      Exact closed form for every positive-index survivor target.

      source
      theorem Algebraic.AC0.ParityParameters.retained_shrinks_nnreal (n t level : ℕ) :
      ↑(retained n t (level + 1)) ≤ retentionRatio t level * ↑(retained n t level)

      Floor division stays below the intended retained ratio, first stated in the finite nonnegative reals.

      source
      theorem Algebraic.AC0.ParityParameters.retained_shrinks (n t level : ℕ) :
      ↑(retained n t (level + 1)) ≤ ↑(retentionRatio t level) * ↑(retained n t level)

      The floor-division inequality in the extended nonnegative reals used by the probability schedule.