OAI/Computability/QuantumFactoring/NetworkRecursionEmission.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.boundedStages line 18

   Source documentation

   Saturation makes the loop's intermediate-state bound valid for every possible invocation, not merely for the one starting at stage zero.

   lemma boundedStages (hK : Emits ea unaryCode K)
       (h0 : NetEmits ea (fun x=>f x 0))
       (hs : NetEmits
         (fun x:Σa,Fin (K a)=>prodCode ea (prodCode unaryCode packCode)
           (x.1,(x.2.val,erasePack (f x.1 x.2.val))))
         (fun x=>f x.1 (x.2.val+1)))
       (hn : PolyAt (fun x:Σa,Fin (K a+1)=>(ea x.1).length) (fun x=>n x.1 x.2.val))
       (hm : PolyAt (fun x:Σa,Fin (K a+1)=>(ea x.1).length) (fun x=>m x.1 x.2.val))
       (hc : NetworkAt (fun x:Σa,Fin (K a+1)=>(ea x.1).length) (fun x=>f x.1 x.2.val)) :
       NetEmits ea (fun x=>f x (K x)):=by
   …

   Mentions: OAI.ExactQuantumFactoring.NetworkEmission.NetEmits, OAI.ExactQuantumFactoring.NetworkEmission.packCode, OAI.ExactQuantumFactoring.NetworkEmission.erasePack, OAI.ExactQuantumFactoring.PolyAt, OAI.ExactQuantumFactoring.NetworkAt