OAI/Computability/QuantumFactoring/TreeQuarterPhysical.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.hadamards_zero_encoded line 19
2. def OAI.ExactQuantumFactoring.Completion.extendEncoding line 29

   Source documentation

   The actual four-register completion, when the ordinary preparation has retained and injectively encoded its full history.

   def extendEncoding {α : Type*} {q : ℕ} (e : α→Basis q) (W t d : ℕ) :
       Raw α W t d→Basis (t+(q+(W+coinBits W t d))) :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.Raw, OAI.ExactQuantumFactoring.Completion.coinBits

3. lemma OAI.ExactQuantumFactoring.Completion.extendEncoding_injective line 33
4. lemma OAI.ExactQuantumFactoring.Completion.program_encoded_state line 49
5. abbrev OAI.ExactQuantumFactoring.PhysicalTree.quarterWidth line 76
6. def OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram line 77
7. def OAI.ExactQuantumFactoring.PhysicalTree.quarterZero line 79
8. def OAI.ExactQuantumFactoring.PhysicalTree.quarterEncoding line 82
9. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram_state line 85
10. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterEncoding_injective line 89
11. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram_length line 91