OAI/Computability/QuantumFactoring/CompletedOrderSlots.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.Completion.dummy_passed_mass line 23

   Source documentation

   Dummy slots retain their internal preparation too. Only the constant output is visible to the controller; no branch-local normalization is performed.

   lemma dummy_passed_mass {α : Type*} [Fintype α] (ψ : α→ℂ) (n d : ℕ)
       (hn : 128 ≤ n) (hψ : ∑ x,Complex.normSq (ψ x)=1) (y₀ : Basis (transitionWidth n)) :
       outcomeMass (passed (fun _ => True) y₀ 1 (target n))
         (fresh ψ (transitionWidth n) (2*n) d)=(target n:ℝ) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.transitionWidth, OAI.ExactQuantumFactoring.Completion.passed, OAI.ExactQuantumFactoring.Completion.target, OAI.ExactQuantumFactoring.Completion.fresh

2. abbrev OAI.ExactQuantumFactoring.OrderSlots.sampleExponent line 44
3. lemma OAI.ExactQuantumFactoring.OrderSlots.sampleExponent_spec line 45
4. abbrev OAI.ExactQuantumFactoring.OrderSlots.Result line 52
5. instance OAI.ExactQuantumFactoring.OrderSlots.resultFintype line 55
6. def OAI.ExactQuantumFactoring.OrderSlots.fresh line 57
7. def OAI.ExactQuantumFactoring.OrderSlots.Usable line 61
8. def OAI.ExactQuantumFactoring.OrderSlots.unitOrder line 65
9. def OAI.ExactQuantumFactoring.OrderSlots.canonical line 69
10. def OAI.ExactQuantumFactoring.OrderSlots.ordinary line 72
11. def OAI.ExactQuantumFactoring.OrderSlots.passed line 78
12. def OAI.ExactQuantumFactoring.OrderSlots.output line 85
13. lemma OAI.ExactQuantumFactoring.OrderSlots.fresh_normalized line 88
14. lemma OAI.ExactQuantumFactoring.OrderSlots.unitOrder_lt line 92
15. lemma OAI.ExactQuantumFactoring.OrderSlots.passed_mass line 103
16. lemma OAI.ExactQuantumFactoring.OrderSlots.passed_output line 115
17. theorem OAI.ExactQuantumFactoring.OrderSlots.all_passed_mass line 131

    Source documentation

    Every supplied base has exactly z retained mass. Out-of-range entries and nonunits are dummy slots, not an assumption that a random list consists only of units.

    theorem all_passed_mass {n : ℕ} (hn : 128 ≤ n) (m : Basis n) (hm : 2 ≤ (bitsValue m).toNat)
        (as : Fin (n^5)→Basis n) :
        outcomeMass (fun r : Fin (n^5)→Result n => ∀ i,passed (as i) m (r i))
          (productState (fun i => fresh n (as i) m))=(Completion.target n:ℝ)^(n^5) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderSlots.Result, OAI.ExactQuantumFactoring.OrderSlots.passed, OAI.ExactQuantumFactoring.productState, OAI.ExactQuantumFactoring.OrderSlots.fresh, OAI.ExactQuantumFactoring.Completion.target