Bounds on the lower-order construction costs

An exponential gap absorbs the minterm tables, pattern banks, hash circuits, and final collision repairs. Only the OR-per-chunk terms remain at leading order.

theorem Complexity.CircuitSparseSynthesis.Internal.two_pow_add_one_le (k : ℕ) : 2 ^ k + 1 ≤ 2 ^ (k + 1)

theorem Complexity.CircuitSparseSynthesis.Internal.hashBudget_le (p m : ℕ) (width : m ≤ 2 * p) : hashBudget (2 * p) m ≤ 32 * (p + 1) ^ 2

theorem Complexity.CircuitSparseSynthesis.Internal.mintermBudget_le {p k l gap : ℕ} (width : k + l ≤ 2 * p) (columns : k ≤ gap) (rows : l ≤ gap) : (2 ^ k + 2 ^ l) * (2 * (k + l) + 1) ≤ (8 * p + 2) * 2 ^ gap

theorem Complexity.CircuitSparseSynthesis.Internal.sparseTableBudget_le {p k l K gap : ℕ} (width : k + l ≤ 2 * p) (columns : k ≤ gap) (rows : l ≤ gap) (bank : (k + 1) * K ≤ gap) (chunks : K ≤ p) : sparseTableBudget k l K (2 ^ p) ≤ 2 ^ p / K + 12 * (p + 1) * 2 ^ gap

theorem Complexity.CircuitSparseSynthesis.Internal.partialTableBudget_le {p k l K gap : ℕ} (width : k + l ≤ 2 * p) (columns : k ≤ gap) (rows : l ≤ gap) (bank : 4 * k + 6 + K ≤ gap) : partialTableBudget k l K (2 ^ p) ≤ 2 ^ p / K + 10 * (p + 1) * 2 ^ gap

theorem Complexity.CircuitSparseSynthesis.Internal.residualBudget_le {p h a steps : ℕ} (hsmall : h ≤ p) (enough : p + h ≤ a * steps) : 2 ^ (2 * p) / (2 ^ a) ^ steps ≤ 2 ^ (p - h)

def Complexity.CircuitSparseSynthesis.Internal.synthesisError (p h : ℕ) : ℕ

A common bound for all auxiliary costs, with an exponential margin of h bits.

Equations

• Complexity.CircuitSparseSynthesis.Internal.synthesisError p h = 100 * (p + 1) ^ 3 * 2 ^ (p - h)

theorem Complexity.CircuitSparseSynthesis.Internal.sparseFiniteBudget_le {p h k l K a steps : ℕ} (hsmall : h ≤ p) (width : k + l ≤ 2 * p) (columns : k ≤ p - h) (rows : l ≤ p - h) (bank : (k + 1) * K ≤ p - h) (chunks : K ≤ p) (stages : steps ≤ p + 1) (enough : p + h ≤ a * steps) : sparseFiniteBudget (2 * p) k l K p a steps ≤ steps * (2 ^ p / K) + synthesisError p h

theorem Complexity.CircuitSparseSynthesis.Internal.partialFiniteBudget_le {p h k l K : ℕ} (hsmall : h ≤ p) (width : k + l ≤ 2 * p) (expanded : p + h ≤ k + l) (columns : k ≤ p - h) (rows : l ≤ p - h) (bank : 4 * k + 6 + K ≤ p - h) : partialFiniteBudget (2 * p) k l K (2 ^ p) ≤ 2 ^ p / K + synthesisError p h