OAI/Computability/QuantumFactoring/BitStackFold.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.scanStep line 14
2. def OAI.ExactQuantumFactoring.BitStackProgram.bitAction line 18
3. lemma OAI.ExactQuantumFactoring.BitStackProgram.scanStep_iterate line 20
4. lemma OAI.ExactQuantumFactoring.BitStackProgram.foldl_measure line 30
5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.scan line 43
6. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.foldBits line 57

   Source documentation

   Fold a variable Boolean word. The bound covers every actual intermediate state; all pairing, data movement and loop iterations are charged.

   noncomputable def foldBits (p : Procedure ea ea f) (q : Procedure ea ea g)
       (bound : Polynomial ℕ)
       (hsize : ∀ (xs : List Bool) a i,(ea ((xs.take i).foldl (bitAction f g) a)).length≤
         bound.eval (xs.length+(ea a).length)) :
       Procedure (prodCode id ea) ea (fun x=>x.1.foldl (bitAction f g) x.2) := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.bitAction, OAI.ExactQuantumFactoring.BitStackProgram.Procedure.length, OAI.ExactQuantumFactoring.BitStackProgram.prodCode

7. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.foldBitsLinear line 80