ControllerQueries.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.FactorController.queries line 18

Source documentation

The actual queried moduli, in chronological order. A rejected divisor aborts and does not query nonexistent later work.

def queries (choose : ℕ→ℕ→ℕ) : ℕ→ℕ→List ℕ→List (ℕ×ℕ)
  | _, _, [] => []
  | 0, _, _::_ => []
  | fuel+1, i, m::ms =>
    if m.Prime then queries choose fuel (i+1) ms
    else (i,m)::(if ProperDivisor m (choose i m) then
      queries choose fuel (i+1) (choose i m::m/choose i m::ms) else [])

Mentions: OAI.ExactQuantumFactoring.FactorController.ProperDivisor

lemma OAI.ExactQuantumFactoring.FactorController.queries_length line 26
theorem OAI.ExactQuantumFactoring.FactorController.run_complete_on_queries line 42
Source documentation
All-good is required ONLY at queries of this very run, not at a table of counterfactual future requests. Exhaustion is excluded by the split weight.
```
theorem run_complete_on_queries (choose : ℕ→ℕ→ℕ) {fuel i : ℕ} {ms : List ℕ}
    (hms : ∀ m∈ms, 2 ≤ m) (hw : weight ms ≤ fuel)
    (hg : ∀ im∈queries choose fuel i ms, ProperDivisor im.2 (choose im.1 im.2)) :
    ∃ ps, run choose fuel i ms=some ps := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorController.weight, OAI.ExactQuantumFactoring.FactorController.queries, OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.FactorController.run
lemma OAI.ExactQuantumFactoring.FactorController.queries_bounded line 87

theorem OAI.ExactQuantumFactoring.FactorController.supplied_node_complete_on_queries line 118

Source documentation

Instantiate the local event with the source's favorable list and actual true-order outputs. Only recorded queries, no counterfactual oracle inputs.

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

Mentions: OAI.ExactQuantumFactoring.FactorController.queries, OAI.ExactQuantumFactoring.suppliedDivisor, OAI.ExactQuantumFactoring.Primality.PerfectPower, OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FavorableUnit, OAI.ExactQuantumFactoring.FactorController.run