OAI/Computability/QuantumFactoring/FixedSplit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.FixedSplit.Raw line 21
2. instance OAI.ExactQuantumFactoring.FixedSplit.rawFintype line 24
3. def OAI.ExactQuantumFactoring.FixedSplit.bases line 26
4. def OAI.ExactQuantumFactoring.FixedSplit.fresh line 31

   Source documentation

   Actual next fresh registers depend only on the completed list output, including its rare guessing branch. Previous outcomes remain in the record.

   noncomputable def fresh {n : ℕ} (m : Basis n) : Raw n→ℂ :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.FixedSplit.Raw

5. def OAI.ExactQuantumFactoring.FixedSplit.passed line 35
6. def OAI.ExactQuantumFactoring.FixedSplit.pairs line 40
7. def OAI.ExactQuantumFactoring.FixedSplit.divisor line 44
8. lemma OAI.ExactQuantumFactoring.FixedSplit.fresh_normalized line 47
9. theorem OAI.ExactQuantumFactoring.FixedSplit.passed_mass line 55

   Source documentation

   One list transition followed by the K order/dummy transitions has exactly z^(K+1) retained mass, unconditioned on the successful factor-data computation.

   theorem passed_mass {n : ℕ} (hn : 128 ≤ n) (m : Basis n) (hm : 2 ≤ (bitsValue m).toNat)
       (hodd : Odd (bitsValue m).toNat) (p₀ p₁ : Component (bitsValue m).toNat) (hne : p₁≠p₀) :
       outcomeMass (passed m (by omega) p₀) (fresh m)=(Completion.target n:ℝ)^(n^5+1) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FixedSplit.passed, OAI.ExactQuantumFactoring.FixedSplit.fresh, OAI.ExactQuantumFactoring.Completion.target

10. lemma OAI.ExactQuantumFactoring.FixedSplit.passed_pair line 66
11. theorem OAI.ExactQuantumFactoring.FixedSplit.passed_divisor line 83

    Source documentation

    The output is the actual guarded even/root/order divisor scan, not a chosen mathematical divisor. Both ordinary and guessed good list outputs are covered.

    theorem passed_divisor {n : ℕ} (hn : 128 ≤ n) (m : Basis n) (hm : 2 ≤ (bitsValue m).toNat)
        (hc : ¬(bitsValue m).toNat.Prime) (hodd : Odd (bitsValue m).toNat)
        (p₀ p₁ : Component (bitsValue m).toNat) (hne : p₁≠p₀)
        (r : Raw n) (hp : passed m (by omega) p₀ r) :
        FactorController.ProperDivisor (bitsValue m).toNat (divisor m r) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.FixedSplit.Raw, OAI.ExactQuantumFactoring.FixedSplit.passed, OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.FixedSplit.divisor