OAI/Computability/QuantumFactoring/CompletedSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderSlots.unitOrder_eq line 22
2. lemma OAI.ExactQuantumFactoring.OrderSlots.passed_value line 34
3. lemma OAI.ExactQuantumFactoring.OrderSlots.passed_order line 39
4. abbrev OAI.ExactQuantumFactoring.CompletedSplit.Raw line 50
5. instance OAI.ExactQuantumFactoring.CompletedSplit.rawFintype line 53
6. def OAI.ExactQuantumFactoring.CompletedSplit.bases line 55
7. def OAI.ExactQuantumFactoring.CompletedSplit.fresh line 60

   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 m→ℂ :=
   …

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

8. def OAI.ExactQuantumFactoring.CompletedSplit.passed line 64
9. def OAI.ExactQuantumFactoring.CompletedSplit.pairs line 69
10. def OAI.ExactQuantumFactoring.CompletedSplit.divisor line 73
11. lemma OAI.ExactQuantumFactoring.CompletedSplit.fresh_normalized line 76
12. theorem OAI.ExactQuantumFactoring.CompletedSplit.passed_mass line 84

    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.CompletedSplit.passed, OAI.ExactQuantumFactoring.CompletedSplit.fresh, OAI.ExactQuantumFactoring.Completion.target

13. lemma OAI.ExactQuantumFactoring.CompletedSplit.passed_pair line 95
14. theorem OAI.ExactQuantumFactoring.CompletedSplit.passed_divisor line 112

    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 m) (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.CompletedSplit.Raw, OAI.ExactQuantumFactoring.CompletedSplit.passed, OAI.ExactQuantumFactoring.FactorController.ProperDivisor, OAI.ExactQuantumFactoring.CompletedSplit.divisor