OAI/Computability/QuantumFactoring/PhysicalNodeLaunch.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalNode.startNet line 21

   Source documentation

   The node's initial pending stack contains only the runtime modulus, enlarged by one bit. Emission and error registers are zero. No factor data is supplied.

   def startNet (n : ℕ) : BooleanNetwork n (configWidth n (2*n)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalNode.configWidth

2. lemma OAI.ExactQuantumFactoring.PhysicalNode.startNet_eval line 26
3. abbrev OAI.ExactQuantumFactoring.PhysicalNode.runWidth line 44
4. def OAI.ExactQuantumFactoring.PhysicalNode.runInitial line 45
5. lemma OAI.ExactQuantumFactoring.PhysicalNode.runInitial_eval line 48
6. theorem OAI.ExactQuantumFactoring.PhysicalNode.launch line 56

   Source documentation

   Coherent launch of a complete node computation, including all literal fresh split trials and the deterministic bounded-stack controller. Earlier entangled histories are retained; this is not a truth-table preparation.

   theorem launch {n p r : ℕ} {α : Type*} [Fintype α] (e : α→Basis p) (ψ : α→ℂ)
       (query : BooleanNetwork p n) (hc : (query.comp (runInitial n)).net.count≤r) :
       (programMatrix (preparedOracle (query.comp (runInitial n)) hc
         ((machine n (2*n)).program (2*n)))).mulVec
         (encodeState (fun a=>packed r (e a) (fun _=>false)) ψ)=
       encodeState (fun ar : α×SplitMachine.Trace n (2*n)=>packed r (e ar.1)
         ((machine n (2*n)).encoded ((startNet n).eval (query.eval (e ar.1))) (2*n) ar.2))
         (RecordedHistory.appendState ψ (fun a=>(machine n (2*n)).state
           ((startNet n).eval (query.eval (e a))) (2*n))) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.PhysicalNode.query, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalNode.runInitial, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.PhysicalNode.machine, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.PhysicalNode.startNet, OAI.ExactQuantumFactoring.RecordedHistory.appendState