TableOrder.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.divisorPrimes_subset line 17
lemma OAI.ExactQuantumFactoring.primeRecord_support_subset line 29
def OAI.ExactQuantumFactoring.PhysicalTree.tableFactors line 44
Source documentation
A fixed rectangular table of prime candidates. Unused rows and zero padding become 2. This requires no support enumeration or factor search.
```
def tableFactors (rows : List (ℕ×List ℕ)) : List ℕ :=
…
```
lemma OAI.ExactQuantumFactoring.PhysicalTree.tableFactors_prime line 47
lemma OAI.ExactQuantumFactoring.PhysicalTree.lookupPrimes_subset_table line 59
lemma OAI.ExactQuantumFactoring.PhysicalTree.logTotientPrimes_subset_table line 74
lemma OAI.ExactQuantumFactoring.PhysicalTree.dvd_cover_power line 93
Source documentation
A support-covering list gives a known multiple after n repetitions, because every prime exponent of an n-bit positive integer is at most n.
```
lemma dvd_cover_power {v n : ℕ} (ps : List ℕ) (hv : v≠0) (hb : v≤2^n)
    (hp : ∀ p∈ps,p.Prime) (hcover : ∀ p : ℕ,p.Prime→p∣v→p∈ps) : v∣ps.prod^n := by
…
```
theorem OAI.ExactQuantumFactoring.PhysicalTree.table_strip_order line 111
Source documentation
A rectangular verified data table is sufficient to recover the same literal multiplicative order. No unbounded support extraction is required.
```
theorem table_strip_order {n N M m : ℕ} {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) (a : (ZMod m)ˣ) :
    stripOrderFactors a (List.flatten (List.replicate n (tableFactors rows)))
      ((tableFactors rows).prod^n)=orderOf a := by
…
```
Mentions: OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.stripOrderFactors, OAI.ExactQuantumFactoring.PhysicalTree.tableFactors