OAI/Computability/QuantumFactoring/PhysicalTreeLaunch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalTree.startNet line 20
2. lemma OAI.ExactQuantumFactoring.PhysicalTree.startNet_eval line 22
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.startNet_nat line 26
4. abbrev OAI.ExactQuantumFactoring.PhysicalTree.steps line 29
5. abbrev OAI.ExactQuantumFactoring.PhysicalTree.width line 30
6. def OAI.ExactQuantumFactoring.PhysicalTree.initialNet line 31
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.initialNet_eval line 33
8. theorem OAI.ExactQuantumFactoring.PhysicalTree.launch line 39

   Source documentation

   Literal runtime-input initialization and physical chronological tree construction, coherently over all input words. No factors initialize the input.

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

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalTree.initialNet, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.steps, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.startNet, OAI.ExactQuantumFactoring.RecordedHistory.appendState

9. def OAI.ExactQuantumFactoring.PhysicalTree.rootResult line 56

   Source documentation

   Actual root readout from earlier retained wires, not a factor-table lookup.

   def rootResult (n t : ℕ) : BooleanNetwork ((machine n).width (t+1)) (tensorWidth n n) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.width, OAI.ExactQuantumFactoring.tensorWidth

10. lemma OAI.ExactQuantumFactoring.PhysicalTree.query_initial line 59
11. theorem OAI.ExactQuantumFactoring.PhysicalTree.root_correct line 64

    Source documentation

    Every flagged chronological raw history has the literal sorted and padded root encoding in the fixed root-output network. No other run supplies it.

    theorem root_correct {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n)
        (t : ℕ) (h : NodeMachine.Trace n (t+1))
        (hp : (machine n).passed (initialQueue n N) (t+1) h) :
        ∃ zs : List (Basis n), zs.length=n ∧ CorrectEncoding N n (SortedWords.numbers zs) ∧
          (rootResult n t).eval ((machine n).encoded (initialQueue n N) (t+1) h)=
            SortedWords.layout n n zs := by
    …

    Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.PhysicalTree.rootResult