OAI/Computability/QuantumFactoring/EmissionBoundedRecursion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.Emits.recursionCode line 14
  2. def OAI.ExactQuantumFactoring.BitStackProgram.Emits.recursionNext line 16
  3. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.recursionNext_iterate line 18
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.boundedRecursion line 39

    Source documentation

    A charged finite-stack loop over an explicitly implemented next-stage construction. The size invariant is a bound on actual intermediate encodings, not an assumption that an arbitrary bounded function is computable.

    lemma boundedRecursion (K : α→ℕ) (f : α→ℕ→β)
    (hK : Emits ea unaryCode K) (h0 : Emits ea eb (fun x=>f x 0))
    (hs : Emits (recursionCode (ea:=ea) (eb:=eb) K f) eb
…

    Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Emits, OAI.ExactQuantumFactoring.BitStackProgram.unaryCode, OAI.ExactQuantumFactoring.BitStackProgram.Emits.recursionCode