TableTotient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.totientScan line 18
Source documentation
Strip a given prime multiset, updating Euler's totient one prime factor at a time. The supplied list may contain redundant factors.
```
def totientScan : List ℕ → ℕ → ℕ
  | [], _ => 1
  | p::ps, v => if p ∣ v then
      (if p ∣ v/p then p else p-1)*totientScan ps (v/p)
    else totientScan ps v
```
lemma OAI.ExactQuantumFactoring.totientScan_exact line 24
theorem OAI.ExactQuantumFactoring.PhysicalTree.table_totient_exact line 56
Source documentation
The same rectangular table which suffices for order stripping supplies Euler's totient of every positive divisor of the group exponent.
```
theorem table_totient_exact {n N M m d : ℕ} {rows : List (ℕ×List ℕ)}
    (h : CompleteLog n N rows) (hM : M∈rows.map Prod.fst) (hM0 : M≠0)
    (hm : 2 ≤ m) (hb : m < 2^n) (hd : m∣M) (hd0 : 0 < d) (hdt : d∣m.totient) :
    totientScan (List.flatten (List.replicate n (tableFactors rows))) d=d.totient := by
…
```
Mentions: OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.totientScan, OAI.ExactQuantumFactoring.PhysicalTree.tableFactors