BitStackIteration.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.inplace line 16
Source documentation
Return the result to one fixed public register. Both word movements are implemented by two reversals; no output-to-input renaming is a TM operation.
```
noncomputable def inplace (p : Procedure ea ea f) : Procedure ea ea f where
…
```
Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure
lemma OAI.ExactQuantumFactoring.BitStackProgram.Procedure.inplace_register line 40
lemma OAI.ExactQuantumFactoring.BitStackProgram.Procedure.iterate_loop_runs line 44
Source documentation
Literal repetition of an in-place subroutine by a unary counter. Each iteration consumes one control token; the bound charges every subroutine step.
```
lemma iterate_loop_runs {L : Type} [DecidableEq L] (p : Procedure ea ea f)
    (he : p.output=p.input) (k : L) (n : ℕ) (a : α) (B : ℕ)
    (hm : ∀ i≤n,(ea ((f^[i]) a)).length≤B) (s : Store L)
    (hs : s k=List.replicate n true) :
    ∃ c,c≤n*(p.bound.eval B+1)+1 ∧
      Runs (.loop (Sum.inr k) (p.program.relabel Sum.inl) (p.program.relabel Sum.inl))
        (sumStore (singletonStore p.input (ea a)) s)
        (sumStore (singletonStore p.input (ea ((f^[n]) a))) (Function.update s k [])) c := by
…
```
Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.Procedure.length, OAI.ExactQuantumFactoring.BitStackProgram.Store, OAI.ExactQuantumFactoring.BitStackProgram.Runs, OAI.ExactQuantumFactoring.BitStackProgram.sumStore, OAI.ExactQuantumFactoring.BitStackProgram.singletonStore
def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.iterate line 87
Source documentation
Input-length-bounded iteration. The extra hypothesis is solely a size invariant along the already implemented iteration, not a computability oracle.
```
noncomputable def iterate (p : Procedure ea ea f) (q : Polynomial ℕ)
    (hgrowth : ∀ n a i,i≤n→(ea ((f^[i]) a)).length≤q.eval (n+(ea a).length)) :
    Procedure (prodCode (fun n=>List.replicate n true) ea) ea (fun x=>(f^[x.1]) x.2) where
…
```
Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.Procedure.length, OAI.ExactQuantumFactoring.BitStackProgram.prodCode