OAI/Computability/QuantumFactoring/ChildQueueBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.wordMember_count line 17
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.active_count line 29
3. def OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.oneBound line 38
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushOne_count line 40
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.oneBound_mono line 57
6. theorem OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushAll_count line 64

   Source documentation

   The all-child queue update is quadratic in the number of prime fields, not an exponentially duplicated expression. Bounds hold on ALL inputs.

   theorem pushAll_count {k w c : ℕ} (s : ℕ) (as : List (BooleanNetwork k w))
       (hs : ∀ b∈as,b.net.count ≤ c) :
       (pushAll s as).net.count ≤ as.length*oneBound s w c as.length := by
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.pushAll, OAI.ExactQuantumFactoring.BitArithmetic.ChildQueue.oneBound