OAI/Computability/QuantumFactoring/FlatVerifiedData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalTree.lookupFields line 20

   Source documentation

   Data lookup runs on the retained flat rows, not on a factorization oracle.

   def lookupFields (rows : List (ℕ×List ℕ)) (m : ℕ) : List ℕ :=
   …

2. def OAI.ExactQuantumFactoring.PhysicalTree.lookupPrimes line 25
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.lookupFields_correct line 28
4. lemma OAI.ExactQuantumFactoring.PhysicalTree.encoding_filter line 45
5. lemma OAI.ExactQuantumFactoring.PhysicalTree.lookupPrimes_correct line 58
6. def OAI.ExactQuantumFactoring.PhysicalTree.logDivisorPrimes line 63
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.logDivisorPrimes_correct line 66
8. lemma OAI.ExactQuantumFactoring.PhysicalTree.log_child_present line 72
9. def OAI.ExactQuantumFactoring.PhysicalTree.logTotientPrimes line 81

   Source documentation

   The only factor data used are supplied parent factors and already verified p−1 rows. This representation is a mathematical list interface; its Boolean implementation is a separate obligation, not hidden in this definition.

   noncomputable def logTotientPrimes (rows : List (ℕ×List ℕ)) (M m : ℕ) : List ℕ :=
   …

10. lemma OAI.ExactQuantumFactoring.PhysicalTree.logTotientPrimes_correct line 86
11. theorem OAI.ExactQuantumFactoring.PhysicalTree.verified_log_strip_order line 128