OAI/Computability/QuantumFactoring/TrialRawPreparation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.parallelProgram_entry line 17
2. def OAI.ExactQuantumFactoring.productLayout line 24
3. lemma OAI.ExactQuantumFactoring.productLayout_apply line 26
4. abbrev OAI.ExactQuantumFactoring.OrderTrial.guessWidth line 31
5. def OAI.ExactQuantumFactoring.OrderTrial.guessLayout line 32
6. def OAI.ExactQuantumFactoring.OrderTrial.guessProgram line 35
7. def OAI.ExactQuantumFactoring.OrderTrial.guessZero line 38
8. lemma OAI.ExactQuantumFactoring.OrderTrial.guessProgram_entry line 40
9. lemma OAI.ExactQuantumFactoring.OrderTrial.guessProgram_length line 46
10. abbrev OAI.ExactQuantumFactoring.OrderTrial.Raw line 50
11. abbrev OAI.ExactQuantumFactoring.OrderTrial.rawWidth line 51
12. def OAI.ExactQuantumFactoring.OrderTrial.rawLayout line 52
13. def OAI.ExactQuantumFactoring.OrderTrial.rawProgram line 54
14. def OAI.ExactQuantumFactoring.OrderTrial.rawZero line 57
15. def OAI.ExactQuantumFactoring.OrderTrial.rawState line 59
16. lemma OAI.ExactQuantumFactoring.OrderTrial.rawProgram_entry line 62
17. lemma OAI.ExactQuantumFactoring.OrderTrial.rawProgram_state line 69
18. lemma OAI.ExactQuantumFactoring.OrderTrial.raw_normalized line 76
19. lemma OAI.ExactQuantumFactoring.OrderTrial.rawProgram_mass line 86

    Source documentation

    A physical Born event equals the corresponding retained-history event. This layout is bijective; no outcome amplitudes are discarded.

    lemma rawProgram_mass {w : ℕ} (s n : ℕ) (a m : Basis w) (P : Raw w s n→Prop) :
        outcomeMass (P ∘ (rawLayout w s n).symm)
          ((programMatrix (rawProgram w s n)).mulVec (basisVector (rawLayout w s n (rawZero s n a m))))=
          outcomeMass P (rawState s n a m) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderTrial.Raw, OAI.ExactQuantumFactoring.OrderTrial.rawLayout, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderTrial.rawProgram, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.OrderTrial.rawZero, OAI.ExactQuantumFactoring.OrderTrial.rawState