Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.Weight

A finite trace weight for the native controller's potential #

Main definitions #

Main results #

This weight is a mathematical potential, not an assumed execution-time certificate. A separate native execution proof must show that actual instructions decrease it sufficiently.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.traceWeight {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr n)) :
ℕ

Weighting each call by its request count plus one pays for scans and fixed controller work.

Instances For
    source
    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.epochAllowance (n : ℕ) :
    ℕ

    A timestamp budget for a node with n levels remaining. A leaf scans no children; an internal node scans ten children, each of which may use its own recursive budget.

    Instances For
      source
      @[simp]
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.epochAllowance_zero :
      epochAllowance 0 = 0

      A leaf needs no new child-set timestamp.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.epochAllowance_succ (n : ℕ) :
      10 * (1 + epochAllowance n) ≤ epochAllowance (n + 1)

      Ten fresh child scans and all ten recursive budgets fit in the parent's allowance.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.mul_epochAllowance_le {n k : ℕ} (hk : k ≤ 10) :
      k * (1 + epochAllowance n) ≤ epochAllowance (n + 1)

      Every partial traversal of the ten children fits the same concrete timestamp allowance.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.epochAllowance_le (n : ℕ) :
      epochAllowance n ≤ 2 * 10 ^ n

      The timestamp budget is bounded by twice the original leaf-array size.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.traceWeight_zero (S : Finset (MatrixMultiplication.Schonhage.OutStr 0)) :
      traceWeight S = 4096 * (S.card + 1)

      The weight of the zero-depth root, including the empty-query boundary.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.traceWeight_le {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr n)) :
      traceWeight S ≤ 4096 * (2 * (n + 1) * (MatrixMultiplication.Schonhage.leaves S).card + 1)

      The existing leaf/passed-set theorem bounds this potential without a runtime assumption.

      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.traceWeight_succ {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) :
      traceWeight S = 4096 * (S.card + 1) + ∑ lam : MatrixMultiplication.Schonhage.Term, if (MatrixMultiplication.Schonhage.childSet S lam).Nonempty then traceWeight (MatrixMultiplication.Schonhage.childSet S lam) else 0

      One root's scan budget and the weights of exactly its nonempty children.

      source
      def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childWeightPrefix {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (k : ℕ) :
      ℕ

      Potential contributed by the child subtrees with numerical labels below k. This is a finite sum of mathematical trace weights, not an assumed execution-time bound.

      Instances For
        source
        @[simp]
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childWeightPrefix_zero {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) :
        childWeightPrefix S 0 = 0

        No child potential has been spent before the first term.

        source
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childWeightPrefix_succ {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (k : Fin 10) :
        childWeightPrefix S (↑k + 1) = childWeightPrefix S ↑k + if (MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits k)).Nonempty then traceWeight (MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits k)) else 0

        Advancing the native term counter adds exactly the next nonempty child's potential.

        source
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.traceWeight_succ_prefix {n : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) :
        traceWeight S = 4096 * (S.card + 1) + childWeightPrefix S 10

        After all ten terms, the child-prefix potential is exactly the recursive part of the existing mathematical trace weight, in the program's unchanged numerical term order.

        source
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.node_local_cost_le (N : ℕ) :
        7 * N + 30 + 10 * (20 * N + 44 + (31 * N + 31)) + 28 ≤ 4096 * (N + 1)

        The complete local controller work fits within the root summand of traceWeight. The terms account for entry, ten scan/push/accumulate pairs, return, and all loop controls. Empty children use less work than the displayed pair. Child recursive work is separate.