OAI/Computability/QuantumFactoring/BooleanNetwork.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ExactQuantumFactoring.BoolNode line 12

   Source documentation

   A bounded-fan-in Boolean node, with no hidden arithmetic operation.

   inductive BoolNode (n : ℕ) where
   …

2. def OAI.ExactQuantumFactoring.BoolNode.eval line 20
3. def OAI.ExactQuantumFactoring.BoolNode.map line 26
4. lemma OAI.ExactQuantumFactoring.BoolNode.eval_map line 32
5. def OAI.ExactQuantumFactoring.BoolNode.compileOp line 36

   Source documentation

   The new wire is distinct from every preexisting wire.

   def compileOp {n q : ℕ} (h : n + 1 ≤ q) (o : BoolNode n) :
       BooleanOp q ⟨n, by omega⟩ :=
   …

   Mentions: OAI.ExactQuantumFactoring.BoolNode, OAI.ExactQuantumFactoring.BooleanOp

6. lemma OAI.ExactQuantumFactoring.BoolNode.compileOp_value line 46
7. inductive OAI.ExactQuantumFactoring.BoolNet line 54

   Source documentation

   Straight-line Boolean computation retaining its whole trace. Width increases by exactly one per node, so there is no truth-table synthesis overhead.

   inductive BoolNet (n : ℕ) : ℕ → Type
     | input : BoolNet n n
     | add {k : ℕ} (p : BoolNet n k) (o : BoolNode k) : BoolNet n (k+1)
   
   namespace BoolNet

   Mentions: OAI.ExactQuantumFactoring.BoolNode

8. def OAI.ExactQuantumFactoring.BoolNet.count line 60
9. lemma OAI.ExactQuantumFactoring.BoolNet.width_eq line 64
10. lemma OAI.ExactQuantumFactoring.BoolNet.input_le line 69
11. def OAI.ExactQuantumFactoring.BoolNet.eval line 71
12. lemma OAI.ExactQuantumFactoring.BoolNet.eval_add_castSucc line 75
13. lemma OAI.ExactQuantumFactoring.BoolNet.eval_add_last line 79
14. lemma OAI.ExactQuantumFactoring.BoolNet.eval_input line 83
15. def OAI.ExactQuantumFactoring.BoolNet.program line 91
16. lemma OAI.ExactQuantumFactoring.BoolNet.program_length line 96
17. lemma OAI.ExactQuantumFactoring.BoolNet.compile_length line 102
18. def OAI.ExactQuantumFactoring.BoolNet.attach line 108

    Source documentation

    Append a network whose inputs are arbitrary already-computed wires. Repeated input sources are permitted and do not cause duplicated computation.

    def attach {n k m l : ℕ} (a : BoolNet n k) (ρ : Fin m → Fin k) (b : BoolNet m l) :
        (j : ℕ) × BoolNet n j × (Fin l → Fin j) :=
    …

    Mentions: OAI.ExactQuantumFactoring.BoolNet

19. lemma OAI.ExactQuantumFactoring.BoolNet.attach_count line 116
20. lemma OAI.ExactQuantumFactoring.BoolNet.attach_eval line 122
21. lemma OAI.ExactQuantumFactoring.BoolNet.attach_width line 135
22. lemma OAI.ExactQuantumFactoring.BoolNet.attach_le line 141
23. lemma OAI.ExactQuantumFactoring.BoolNet.attach_preserve line 144
24. lemma OAI.ExactQuantumFactoring.BoolNet.program_eval line 156

    Source documentation

    On fresh ancillas the compiled program realizes the network exactly, including preservation of all unused wires.

    lemma program_eval {n k q : ℕ} (p : BoolNet n k) (h : k ≤ q) (x : Basis q)
        (hfresh : ∀ i : Fin q, n ≤ i.val → 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 = false) := by
    …

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

25. structure OAI.ExactQuantumFactoring.BooleanNetwork line 197

    Source documentation

    Typed interfaces for network composition, with explicitly retained workspace.

    structure BooleanNetwork (n m : ℕ) where
    …