OAI/Computability/QuantumFactoring/BooleanVector.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BooleanNetwork.vector line 14

    Source documentation

    Assemble an arbitrary vector of single-bit combinational outputs, retaining separate traces. This is a finite circuit construction, not a truth table.

    def vector {n : ℕ} : {m : ℕ} → (Fin m → BooleanNetwork n 1) → BooleanNetwork n m
  | 0, _ => select Fin.elim0
  | m+1, f => (vector (fun i => f i.castSucc)).pair (f (Fin.last m))

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BooleanNetwork.select, OAI.ExactQuantumFactoring.BooleanNetwork.pair

  2. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_vector line 18
  3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_vector line 29
  4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_vector_le line 35
  5. def OAI.ExactQuantumFactoring.BooleanNetwork.padRight line 44

    Source documentation

    Add explicit zero slots, with <=m nodes. Duplicate outputs may share zero, but the simple linear upper bound is sufficient for the compiler.

    def padRight (n m : ℕ) : BooleanNetwork n (n+m) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  6. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_padRight line 47
  7. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_padRight line 55