OAI/Computability/QuantumFactoring/CRTLevels.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.Component line 17
2. instance OAI.ExactQuantumFactoring.componentNeZero line 19
3. abbrev OAI.ExactQuantumFactoring.ComponentUnits line 23
4. def OAI.ExactQuantumFactoring.unitCRT line 26
5. lemma OAI.ExactQuantumFactoring.component_order_level_lt line 30
6. def OAI.ExactQuantumFactoring.componentLevel line 45
7. lemma OAI.ExactQuantumFactoring.componentLevel_card line 49
8. def OAI.ExactQuantumFactoring.favorableCount line 60

   Source documentation

   Closed form for the number of favorable unit residues. Only n+1 levels and the prime-power factors occur; there is no modulo-m residue enumeration.

   def favorableCount (m n : ℕ) : ℕ :=
   …

9. def OAI.ExactQuantumFactoring.FavorableUnit line 64
10. lemma OAI.ExactQuantumFactoring.equal_component_card line 69
11. theorem OAI.ExactQuantumFactoring.favorableCount_eq_card line 90

    Source documentation

    The exact source F is the cardinality of the actual CRT favorable event.

    theorem favorableCount_eq_card {m n : ℕ} (hm : m ≠ 0) (hmn : m < 2^n)
        (hodd : Odd m) (p₀ : Component m) :
        favorableCount m n = Nat.card {a : (ZMod m)ˣ // FavorableUnit hm hmn p₀ a} := by
    …

    Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.favorableCount, OAI.ExactQuantumFactoring.FavorableUnit

12. theorem OAI.ExactQuantumFactoring.totient_le_twice_favorableCount line 105

    Source documentation

    At least half the units are favorable whenever there are two distinct odd prime-power components, exactly as in Section 5.

    theorem totient_le_twice_favorableCount {m n : ℕ} (hm : m ≠ 0) (hmn : m < 2^n)
        (hodd : Odd m) (p₀ p₁ : Component m) (hne : p₁ ≠ p₀) :
        m.totient ≤ 2 * favorableCount m n := by
    …

    Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.favorableCount