MachineInitialization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.SplitMachine.initialNet line 17
Source documentation
Literal clean initialization: retain the runtime controller word and create only zero history/output/scratch fields. No query result is precomputed.
```
def initialNet : (t : ℕ) → BooleanNetwork c (M.width t)
  | 0 => select id
  | t+1 => packNet M.updateWork
      (packNet M.initWork (initialNet t) (Completion.zeros c (FixedSplit.width n)))
      (Completion.zeros c c)
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Completion.zeros, OAI.ExactQuantumFactoring.FixedSplit.width
lemma OAI.ExactQuantumFactoring.SplitMachine.initialNet_eval line 23
lemma OAI.ExactQuantumFactoring.SplitMachine.initialNet_count line 31

theorem OAI.ExactQuantumFactoring.SplitMachine.launch_on_history line 41

Source documentation

A whole fixed-period machine can itself be launched coherently from a Boolean-computed runtime controller state, retaining earlier history exactly.

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

Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.RecordedHistory.appendState