FactorController.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Bounded, guarded binary factor controller for a single auxiliary-tree node. Only proper divisors are accepted and primality is tested, never assumed. The mathematical prime-factor count is used solely in its termination proof.

def OAI.ExactQuantumFactoring.FactorController.ProperDivisor line 16
instance OAI.ExactQuantumFactoring.FactorController.(instance at line 17) line 17
lemma OAI.ExactQuantumFactoring.FactorController.ProperDivisor.quotient line 19
lemma OAI.ExactQuantumFactoring.FactorController.splitWeight_pos line 31
lemma OAI.ExactQuantumFactoring.FactorController.splitWeight_mul line 40
lemma OAI.ExactQuantumFactoring.FactorController.splitWeight_split line 45
def OAI.ExactQuantumFactoring.FactorController.weight line 51
lemma OAI.ExactQuantumFactoring.FactorController.weight_prime line 53
lemma OAI.ExactQuantumFactoring.FactorController.weight_split line 57

def OAI.ExactQuantumFactoring.FactorController.run line 67

Source documentation

choose i m is the prospective divisor obtained at the i-th guarded controller step from its recorded classical transition outputs.

def run (choose : ℕ→ℕ→ℕ) : ℕ→ℕ→List ℕ→Option (List ℕ)
  | _, _, [] =>  some []
  | 0, _, _::_ =>  none
  | fuel+1, i, m::ms => 
    if m.Prime then (run choose fuel (i+1) ms).map (m::·)
    else let d := choose i m
…

theorem OAI.ExactQuantumFactoring.FactorController.run_sound line 77
Source documentation
On every output sequence, a successful result is a genuine complete factorization. Bad divisors cause an abort, not a false prime leaf.
```
theorem run_sound (choose : ℕ→ℕ→ℕ) {fuel i : ℕ} {ms ps : List ℕ}
    (h : run choose fuel i ms=some ps) :
    (∀ p∈ps, p.Prime) ∧ ps.prod=ms.prod := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorController.run
theorem OAI.ExactQuantumFactoring.FactorController.run_complete line 103
Source documentation
All-good divisors cannot exhaust the linear (in logarithmic input size) controller clock. This theorem controls arbitrary supplied good outputs.
```
theorem run_complete (choose : ℕ→ℕ→ℕ) {N fuel i : ℕ} {ms : List ℕ}
    (hgood : ∀ i m, 2 ≤ m → m ≤ N → ¬m.Prime → ProperDivisor m (choose i m))
    (hms : ∀ m∈ms, 2 ≤ m ∧ m ≤ N) (hw : weight ms ≤ fuel) :
    ∃ ps, run choose fuel i ms=some ps := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.FactorController.weight, OAI.ExactQuantumFactoring.FactorController.run
theorem OAI.ExactQuantumFactoring.FactorController.bounded_node_complete line 144
Source documentation
A 2n-step clock suffices for every bounded node. Its successful list is then sorted, padded and passed to the concrete verifier.
```
theorem bounded_node_complete {N n : ℕ} (hN : 2 ≤ N) (hb : N < 2^n)
    (choose : ℕ→ℕ→ℕ)
    (hgood : ∀ i m, 2 ≤ m → m ≤ N → ¬m.Prime → ProperDivisor m (choose i m)) :
    ∃ ps, run choose (2*n) 0 [N]=some ps ∧
      (∀ p∈ps, p.Prime) ∧ ps.prod=N ∧ ps.length < n := by
…
```
Mentions: OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.FactorController.run