OAI/Computability/QuantumFactoring/PhysicalSplitLaunch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.preparedOracle_encode_dependent line 18
2. def OAI.ExactQuantumFactoring.FixedSplit.initialNet line 41
3. lemma OAI.ExactQuantumFactoring.FixedSplit.initialNet_eval line 45
4. lemma OAI.ExactQuantumFactoring.FixedSplit.initialNet_count line 47
5. abbrev OAI.ExactQuantumFactoring.FixedSplit.launchWork line 53

   Source documentation

   Runtime-modulus launch of the entire raw split. The circuit description contains n only, never the input integer, its prime factors, or true orders.

   abbrev launchWork (n : ℕ) := (initialNet n).net.count

   Mentions: OAI.ExactQuantumFactoring.FixedSplit.initialNet

6. abbrev OAI.ExactQuantumFactoring.FixedSplit.launchWidth line 54
7. def OAI.ExactQuantumFactoring.FixedSplit.launch line 55
8. def OAI.ExactQuantumFactoring.FixedSplit.launchEncoding line 57
9. theorem OAI.ExactQuantumFactoring.FixedSplit.launch_state line 60
10. theorem OAI.ExactQuantumFactoring.FixedSplit.launch_on_history line 68

    Source documentation

    Coherent correctness on an arbitrary retained history. A parameter-dependent encoder keeps this run's actual modulus and all of its actual scratch registers.

    theorem launch_on_history {α : Type*} [Fintype α] {p n r : ℕ}
        (e : α→Basis p) (ψ : α→ℂ) (m : BooleanNetwork p n)
        (hc : (m.comp (initialNet n)).net.count≤r) :
        (programMatrix (preparedOracle (m.comp (initialNet n)) hc (program n))).mulVec
          (encodeState (fun a=>packed r (e a) (fun _=>false)) ψ)=
          encodeState (fun ar : α×Raw n=>packed r (e ar.1) (encoding (m.eval (e ar.1)) ar.2))
            (RecordedHistory.appendState ψ (fun a=>fresh (m.eval (e a)))) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.FixedSplit.initialNet, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.FixedSplit.program, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.FixedSplit.Raw, OAI.ExactQuantumFactoring.FixedSplit.encoding, OAI.ExactQuantumFactoring.RecordedHistory.appendState, OAI.ExactQuantumFactoring.FixedSplit.fresh

11. lemma OAI.ExactQuantumFactoring.FixedSplit.launch_length line 80