Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.HalvingCounts

Exact counts for fixed halving phases #

A successful menu candidate contains enough clean requests for a fixed prefix. Power-of-two batches halve until the singleton phase accepts the last request; no runtime counters are needed for these sizes.

source
theorem Algebraic.MassProduction.Nonuniform.HalfClean.cleanCount {capacity active : ℕ} {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] (state : PhaseState V (Projectivization K V) capacity active) (candidate : Fin active → Projectivization K V) (successful : HalfClean state candidate) :
(active + 1) / 2 ≤ Nat.card { index : Fin active // Clean (fun (index : Fin active) (direction : Projectivization K V) => puncturedLine (state.2 index) direction) (phaseOccupied state) candidate index }

The half-clean predicate provides the rounded-up acceptance count.

source
def Algebraic.MassProduction.Nonuniform.acceptedCount (depth : ℕ) :
ℕ

Number accepted by the phase whose pending batch has 2^depth requests.

Equations
Instances For
    source
    def Algebraic.MassProduction.Nonuniform.pendingCount (depth : ℕ) :
    ℕ

    Number remaining after the fixed clean prefix is accepted.

    Equations
    Instances For
      source
      theorem Algebraic.MassProduction.Nonuniform.acceptedCount_positive (depth : ℕ) :
      0 < acceptedCount depth

      Every nonempty power-of-two phase accepts at least one request.

      source
      theorem Algebraic.MassProduction.Nonuniform.acceptedCount_le (depth : ℕ) :
      acceptedCount depth ≤ Sorting.networkRecords depth

      The accepted prefix fits in the current request array.

      source
      theorem Algebraic.MassProduction.Nonuniform.acceptedCount_add_pendingCount (depth : ℕ) :
      acceptedCount depth + pendingCount depth = Sorting.networkRecords depth

      Accepted and pending counts partition the batch exactly.

      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.acceptedCount_zero :
      acceptedCount 0 = 1

      The singleton phase accepts its only request.

      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.pendingCount_zero :
      pendingCount 0 = 0

      The singleton phase leaves no pending requests.

      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.acceptedCount_succ (depth : ℕ) :
      acceptedCount (depth + 1) = Sorting.networkRecords depth

      A larger phase accepts exactly the next smaller power of two.

      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.pendingCount_succ (depth : ℕ) :
      pendingCount (depth + 1) = Sorting.networkRecords depth

      A larger phase leaves exactly the next smaller power of two.