OAI/Computability/QuantumFactoring/TraceBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.list_map_sum_le line 17
2. lemma OAI.ExactQuantumFactoring.Logged.traverse_requests_length line 27
3. def OAI.ExactQuantumFactoring.AuxiliaryTree.visits line 41
4. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.sum_map_range line 45
5. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.visits_length line 52
6. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.visits_length_le line 62
7. theorem OAI.ExactQuantumFactoring.DataProducer.build_requests_length line 76

   Source documentation

   A failing producer only visits a prefix of the genuine occurrence tree. Whenever it proceeds below a node, the validated factor list forces exactly the canonical children. This bound does not assume that any stochastic test passed.

   theorem build_requests_length (n : ℕ) (choose : Choices) (depth : ℕ) (path : List ℕ) (m : ℕ) :
       (build n choose depth path m).requests.length  ≤  (visits depth m).length := by
   …

   Mentions: OAI.ExactQuantumFactoring.DataProducer.Choices, OAI.ExactQuantumFactoring.DataProducer.build

8. lemma OAI.ExactQuantumFactoring.DataProducer.full_requests_length line 98
9. def OAI.ExactQuantumFactoring.DataProducer.splitRequests line 104

   Source documentation

   Count every local splitting request, including the final failed one.

   noncomputable def splitRequests (n : ℕ) (choose : Choices) (depth : ℕ) (m : ℕ) : List (NodeKey×(ℕ×ℕ)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.DataProducer.Choices, OAI.ExactQuantumFactoring.DataProducer.NodeKey

10. lemma OAI.ExactQuantumFactoring.DataProducer.splitRequests_length line 108
11. lemma OAI.ExactQuantumFactoring.DataProducer.padded_transition_bound line 118