OAI/Computability/QuantumFactoring/HardCofactor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.exists_distinct_components line 19

   Source documentation

   The randomized splitter is invoked only after the prime and perfect-power cases. Such an input has two genuinely different prime-power components.

   lemma exists_distinct_components {m : ℕ} (hm : 2 ≤ m) (hc : ¬m.Prime)
       (hp : ¬Primality.PerfectPower m) : ∃ p₀ p₁ : Component m, p₁≠p₀ := by
   …

   Mentions: OAI.ExactQuantumFactoring.Primality.PerfectPower, OAI.ExactQuantumFactoring.Component