OAI/Computability/QuantumFactoring/BitStackComposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_empty line 16
2. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_singleton line 21
3. def OAI.ExactQuantumFactoring.BitStackProgram.moveWord line 28

   Source documentation

   Move an entire word without reversing its order. Each symbol is pushed and popped twice; this is not an atomic bulk-copy instruction.

   def moveWord (a b t : K) : Program K := .seq (reverseMove a t) (reverseMove t b)

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Program, OAI.ExactQuantumFactoring.BitStackProgram.reverseMove

4. lemma OAI.ExactQuantumFactoring.BitStackProgram.moveWord_runs line 29
5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.joinLeft line 47
6. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.joinRight line 48
7. lemma OAI.ExactQuantumFactoring.BitStackProgram.Procedure.eval_nat_mono line 51
8. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.comp line 60

   Source documentation

   Checked composition for actual finite Boolean-stack procedures. This constructs the combined program and accounts for the intermediate-word copy; it does NOT invoke Mathlib's unproved TM2 polytime-composition declaration.

   noncomputable def comp (q : Procedure eb ec g) (p : Procedure ea eb f) :
       Procedure ea ec (g ∘ f) where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure