OAI/Computability/QuantumFactoring/FavorableSplit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.component_modulus_two_lt line 17
2. lemma OAI.ExactQuantumFactoring.unitCRT_apply line 27
3. theorem OAI.ExactQuantumFactoring.favorable_split line 38

   Source documentation

   A favorable CRT event supplies a proper split from the actual true order.

   theorem favorable_split {m n : ℕ} (hm : 2 ≤ m) (hb : m < 2^n) (hodd : Odd m)
       (p₀ : Component m) (a : (ZMod m)ˣ) (hf : FavorableUnit (by omega : m≠0) hb p₀ a) :
       2 ∣ orderOf a ∧ FactorController.ProperDivisor m (splitGcd a) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FavorableUnit, OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.splitGcd

4. def OAI.ExactQuantumFactoring.canonicalUnit line 65

   Source documentation

   The distinguished CRT residue used in the list-completion branch. The parameter p₀ is subsequently chosen as the least prime component.

   noncomputable def canonicalUnit {m : ℕ} (hm : m≠0) (p₀ : Component m) : (ZMod m)ˣ :=
   …

   Mentions: OAI.ExactQuantumFactoring.Component

5. lemma OAI.ExactQuantumFactoring.canonicalUnit_component line 68
6. lemma OAI.ExactQuantumFactoring.component_neg_one_order line 72
7. lemma OAI.ExactQuantumFactoring.canonicalUnit_favorable line 80