OAI/Computability/QuantumFactoring/MinimumCandidateCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.OrderTrial.minNonzero line 17
  2. lemma OAI.ExactQuantumFactoring.OrderTrial.minNonzero_options line 18
  3. def OAI.ExactQuantumFactoring.OrderTrial.minimumChoice line 31
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumChoice_value line 36
  5. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumChoice_count line 49
  6. def OAI.ExactQuantumFactoring.OrderTrial.minimumNet line 59

    Source documentation

    Pair costly subnets ONCE before comparing; the recursive minimum is not copied into each arm of the mux. This gives a linear, not exponential, scan.

    def minimumNet {k w : ℕ} : {K : ℕ} → (Fin K → BooleanNetwork k w) → BooleanNetwork k w
  | 0,_ => wordConstant (BitVec.ofNat w 0)
  | _+1,f => ((f 0).pair (minimumNet (fun i => f i.succ))).comp (minimumChoice w)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderTrial.minimumChoice

  7. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumNet_value line 62
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumNet_count line 78