BooleanOracle.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.BoolNet.program_eval_range line 15

Source documentation

Only the actual trace, not unrelated output registers, must start at zero.

lemma program_eval_range {n k q : ℕ} (p : BoolNet n k) (h : k ≤ q) (x : Basis q)
    (hfresh : ∀ i : Fin q, n ≤ i.val → i.val < k → x i = false) :
    (∀ i : Fin k, (BooleanProgram.eval (p.program h) x) (i.castLE h) =
      p.eval (fun j => x (j.castLE (p.input_le.trans h))) i) ∧
    (∀ i : Fin q, k ≤ i.val → (BooleanProgram.eval (p.program h) x) i = x i) := by
…

Mentions: OAI.ExactQuantumFactoring.BoolNet, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BooleanProgram.eval

def OAI.ExactQuantumFactoring.BooleanNetwork.copyPrefix line 59

Source documentation

Copy disjoint source wires into a separate target register, by XOR.

def copyPrefix {k m : ℕ} (source : Fin m → Fin k) : (t : ℕ) → t ≤ m → BooleanProgram (k+m)
  | 0, _ => []
  | t+1, h => copyPrefix source t (by omega) ++
    [⟨Fin.natAdd k ⟨t, by omega⟩, .copy ((source ⟨t, by omega⟩).castAdd m)
      (by intro he; have hh := congrArg Fin.val he; simp at hh; omega)⟩]

Mentions: OAI.ExactQuantumFactoring.BooleanProgram

lemma OAI.ExactQuantumFactoring.BooleanNetwork.copyPrefix_length line 65
lemma OAI.ExactQuantumFactoring.BooleanNetwork.copyPrefix_eval line 71
def OAI.ExactQuantumFactoring.BooleanNetwork.oracle line 99
Source documentation
Actual fixed-gate compute/copy/uncompute, with all trace wires restored.
```
def oracle {n m : ℕ} (c : BooleanNetwork n m) : List (Instruction (c.width+m)) :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction
lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracle_length line 104
def OAI.ExactQuantumFactoring.BooleanNetwork.oracleOutput line 114
Source documentation
The basis-state whose trace is zero and whose target is toggled by c(x).
```
def oracleOutput {n m : ℕ} (c : BooleanNetwork n m) (x : Basis (c.width+m)) : Basis (c.width+m) :=
…
```
Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis
lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracle_basis line 119