OAI/Computability/QuantumFactoring/AdaptivePrepared.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.preparedOracle_encode line 21

   Source documentation

   A coherent fresh launch on an encoded old history. The local law refers only to the actually computed Boolean initializer, never to a selected outcome.

   lemma preparedOracle_encode {α β : Type*} [Fintype α] [Fintype β] {p q r : ℕ}
       (e : α→Basis p) (f : β→Basis q) (ψ : α→ℂ) (F : α→β→ℂ)
       (c : BooleanNetwork p q) (hc : c.net.count ≤ r) (ops : List (Instruction q))
       (hlocal : ∀ a,(programMatrix ops).mulVec (basisVector (c.eval (e a)))=encodeState f (F a)) :
       (programMatrix (preparedOracle c hc ops)).mulVec
         (encodeState (fun a=>packed r (e a) (fun _=>false)) ψ)=
       encodeState (fun ab : α×β=>packed r (e ab.1) (f ab.2)) (RecordedHistory.appendState ψ F) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.RecordedHistory.appendState

2. def OAI.ExactQuantumFactoring.appendPrepared line 40
3. lemma OAI.ExactQuantumFactoring.appendPrepared_length line 44
4. lemma OAI.ExactQuantumFactoring.appendPrepared_state line 51