OAI/Computability/QuantumFactoring/TablePrimeSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTree.tableFactors_cover line 20
2. def OAI.ExactQuantumFactoring.leastDivisorIn line 35

   Source documentation

   A distinguished component can be tested by polynomially many pairwise comparisons, without constructing the least prime factor of an unknown N.

   def leastDivisorIn (ps : List ℕ) (m p : ℕ) : Prop := ∀ q∈ps,q∣m→p≤q

3. lemma OAI.ExactQuantumFactoring.leastDivisorIn_iff line 37
4. def OAI.ExactQuantumFactoring.tableCanonical line 49

   Source documentation

   Redundant rectangular-table entries and harmless dummy primes are ignored unless they divide m; duplicates impose exactly the same congruence.

   noncomputable def tableCanonical (ps : List ℕ) (a m n : ℕ) : Prop := by
   …

5. lemma OAI.ExactQuantumFactoring.tableCanonical_correct line 54