ProvidedSplits.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.firstProper line 21
Source documentation
A guarded scan. Invalid proposals never change the arithmetic product invariant of the factoring controller.
```
def firstProper (m : ℕ) : List ℕ→ℕ
  | [] => 0
  | d::ds => if ProperDivisor m d then d else firstProper m ds
```
lemma OAI.ExactQuantumFactoring.firstProper_of_mem line 25
lemma OAI.ExactQuantumFactoring.firstProper_sound line 37
def OAI.ExactQuantumFactoring.orderSplit line 47
lemma OAI.ExactQuantumFactoring.orderSplit_good line 52
Source documentation
ars are the supplied list entries paired with the recorded order outputs. When the good list entry has its true order, the actual guarded scan splits.
```
lemma orderSplit_good {m n : ℕ} (hm : 2 ≤ m) (hb : m < 2^n) (hodd : Odd m)
    (p₀ : Component m) (ars : List (ℕ×ℕ))
    (u : (ZMod m)ˣ) (hf : FavorableUnit (by omega : m≠0) hb p₀ u)
    (hmem : ((u : ZMod m).val,orderOf u)∈ars) : ProperDivisor m (orderSplit m ars) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FavorableUnit, OAI.ExactQuantumFactoring.orderSplit
def OAI.ExactQuantumFactoring.rootProposals line 64
Source documentation
Root searches are clocked by the ORIGINAL input length n.
```
def rootProposals (m n : ℕ) : List ℕ :=
…
```
def OAI.ExactQuantumFactoring.rootSplit line 67
lemma OAI.ExactQuantumFactoring.perfectPower_proper line 69
lemma OAI.ExactQuantumFactoring.rootSplit_good line 81
def OAI.ExactQuantumFactoring.suppliedDivisor line 91
lemma OAI.ExactQuantumFactoring.suppliedDivisor_good line 95

theorem OAI.ExactQuantumFactoring.supplied_node_complete line 115

Source documentation

The all-good node completion used in the source. The chosen divisor is now an actual even/root/order scan, not an assumed proper-divisor oracle.

theorem supplied_node_complete {N n : ℕ} (hN : 2 ≤ N) (hb : N < 2^n)
    (outputs : ℕ→ℕ→List (ℕ×ℕ))
    (hgood : ∀ i m (hm : 2 ≤ m) (hle : m ≤ N), ¬m.Prime → Odd m →
      ¬Primality.PerfectPower m →
      ∃ (p₀ : Component m) (u : (ZMod m)ˣ),
        FavorableUnit (by omega : m≠0) (hle.trans_lt hb) p₀ u ∧
        ((u : ZMod m).val,orderOf u)∈outputs i m) :
    ∃ ps, run (fun i m => suppliedDivisor m n (outputs i m)) (2*n) 0 [N]=some ps ∧
      (∀ p∈ps,p.Prime) ∧ ps.prod=N ∧ ps.length < n := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.PerfectPower, OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FavorableUnit, OAI.ExactQuantumFactoring.suppliedDivisor