OAI/Computability/QuantumFactoring/InitialOrderState.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.encodeState_comp line 14
2. def OAI.ExactQuantumFactoring.Triangular.dataRegister line 25
3. lemma OAI.ExactQuantumFactoring.Triangular.encode_data line 30
4. lemma OAI.ExactQuantumFactoring.Triangular.encode_outside_data line 35
5. lemma OAI.ExactQuantumFactoring.Triangular.encode_replace_data line 50
6. def OAI.ExactQuantumFactoring.Triangular.uniformPreparation line 61
7. lemma OAI.ExactQuantumFactoring.Triangular.uniformPreparation_length line 64
8. lemma OAI.ExactQuantumFactoring.Triangular.uniformPreparation_zero line 67
9. def OAI.ExactQuantumFactoring.OrderSample.initial line 80
10. lemma OAI.ExactQuantumFactoring.OrderSample.initial_length line 83
11. lemma OAI.ExactQuantumFactoring.OrderSample.initial_zero line 86
12. def OAI.ExactQuantumFactoring.OrderSample.completeSampler line 93
13. lemma OAI.ExactQuantumFactoring.OrderSample.completeSampler_length line 96
14. theorem OAI.ExactQuantumFactoring.OrderSample.completeSampler_amplitude line 104

    Source documentation

    Physical sampler starts from a computational basis vector, not an assumed uniform state. Its selected entry is the exact residue-class interference sum.

    theorem completeSampler_amplitude {w s : ℕ} (a m : Basis w) (y : Basis (s+2)) (u : Basis w)
        (hm : 2 ≤ (bitsValue m).toNat) :
        (programMatrix (completeSampler w s)).mulVec
          (basisVector (word a m (fun _ => false) (fun _ => false))) (word a m y u) =
          ((2^(s+2):ℕ):ℂ)⁻¹ * ∑ x ∈ Finset.range (2^(s+2)),
            if (bitsValue a).toNat^x % (bitsValue m).toNat=(bitsValue u).toNat
            then OrderTrial.phase ((Triangular.outputNumber y:ℝ)*x/(2^(s+2):ℕ)) else 0 := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderSample.completeSampler, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.OrderSample.word, OAI.ExactQuantumFactoring.OrderTrial.phase, OAI.ExactQuantumFactoring.Triangular.outputNumber