OAI/Computability/QuantumFactoring/CleanTranslation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.ControlledTranslation.circuit line 16

   Source documentation

   The clean finite-gate controlled-shift implementation derived from its forward and inverse verified combinational networks.

   def circuit {p b : ℕ} (δ : BooleanNetwork p b) :
       List (Instruction ((p+b)+(p+b)+(δ.net.count+158*b+6))) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction

2. lemma OAI.ExactQuantumFactoring.ControlledTranslation.circuit_basis line 21
3. lemma OAI.ExactQuantumFactoring.ControlledTranslation.circuit_length line 28