OAI/Computability/QuantumFactoring/BitStackChoice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.leftPublic line 13
2. def OAI.ExactQuantumFactoring.BitStackProgram.rightPublic line 17
3. abbrev OAI.ExactQuantumFactoring.BitStackProgram.Procedure.shared line 24

   Source documentation

   A same-wire interface, even when the input and output word encodings differ.

   noncomputable abbrev shared (p : Procedure ea eb f) : Procedure ea eb f where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure

4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.precompose line 49

   Source documentation

   Reinterpret the domain, with its entire previous encoding still on tape.

   def precompose (p : Procedure ea eb f) (h : γ→α) :
       Procedure (fun a=>ea (h a)) eb (fun a=>f (h a)) where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure

5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.congrEncoding line 60
6. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.result line 72

   Source documentation

   Change the mathematical output only when its actual encoded word agrees.

   def result (p : Procedure ea eb f) {ec : γ→List Bool} {h : α→γ}
       (hr : ∀a,eb (f a)=ec (h a)) : Procedure ea ec h where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure

7. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.unprefix line 83
8. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.chooseBit line 100
9. abbrev OAI.ExactQuantumFactoring.BitStackProgram.Procedure.boolCode line 147
10. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.choose line 148