OAI/Computability/QuantumFactoring/AuxiliaryTree.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Occurrence-preserving bounds for the canonical p−1 auxiliary tree in Section5. Equal labels under different parents remain separate list entries.

  1. def OAI.ExactQuantumFactoring.AuxiliaryTree.children line 14
  2. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.mem_children line 17
  3. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.child_bounds line 26
  4. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.child_even line 31
  5. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.grandchild_half line 36
  6. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.children_prod_le line 46
  7. def OAI.ExactQuantumFactoring.AuxiliaryTree.level line 59

    Source documentation

    A level is a list, not a set: multiplicities of occurrences are retained.

    def level (M : ℕ) : ℕ → List ℕ
  | 0 => [M]
  | k+1 => (children M).flatMap (fun d => level d k)

    Mentions: OAI.ExactQuantumFactoring.AuxiliaryTree.children

  8. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_bounds line 63
  9. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_two_step line 75
  10. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_empty line 91
  11. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.prod_flatMap line 99
  12. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_prod_le line 105
  13. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.pow_length_le_prod line 117
  14. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_length_lt line 126
  15. def OAI.ExactQuantumFactoring.AuxiliaryTree.splitWeight line 132
  16. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.splitWeight_bound line 134
  17. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.level_weight_lt line 141
  18. def OAI.ExactQuantumFactoring.AuxiliaryTree.taskBound line 164

    Source documentation

    The source's whole-tree task cap, expressed without real logarithms.

    def taskBound (M n : ℕ) : ℕ :=
…
  19. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.taskBound_le line 167
  20. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.transitions_bound line 175
  21. lemma OAI.ExactQuantumFactoring.AuxiliaryTree.transitions_lt_slots line 184