RetrospectiveOrder.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.stripOrderPrime line 17
Source documentation
One occurrence of the source's prime-stripping loop. A repeated prime factor list supplies exactly as many attempts as its known multiplicity.
```
def stripOrderPrime {G : Type*} [Monoid G] [DecidableEq G] (a : G) (q v : ℕ) : ℕ :=
…
```
def OAI.ExactQuantumFactoring.stripOrderFactors line 20
lemma OAI.ExactQuantumFactoring.stripOrderPrime_multiple line 24
lemma OAI.ExactQuantumFactoring.quotient_dvd_tail line 45
theorem OAI.ExactQuantumFactoring.stripOrderFactors_exact line 55
Source documentation
Complete factor stripping: no excess prime can survive a scan of a known factorization of a multiple of the initial quotient. There is no call to an order oracle in this algorithm.
```
theorem stripOrderFactors_exact {G : Type*} [Monoid G] [DecidableEq G]
    (a : G) (hr : 0 < orderOf a) (qs : List ℕ)
    (hp : ∀ q∈qs, q.Prime) (k : ℕ) (hk : k∣qs.prod) :
    stripOrderFactors a qs (orderOf a*k)=orderOf a := by
…
```
Mentions: OAI.ExactQuantumFactoring.stripOrderFactors
theorem OAI.ExactQuantumFactoring.strip_totient_factors line 76
Source documentation
Specializing to the known factorization of phi(m), as in source §5. The factor list is explicit input produced by the completed auxiliary tree.
```
theorem strip_totient_factors {m : ℕ} (hm : 2 ≤ m) (a : (ZMod m)ˣ)
    (qs : List ℕ) (hp : ∀ q∈qs,q.Prime) (hprod : qs.prod=m.totient) :
    stripOrderFactors a qs m.totient=orderOf a := by
…
```
Mentions: OAI.ExactQuantumFactoring.stripOrderFactors