OAI/Computability/QuantumFactoring/CircuitEncodingSize.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.natWord_length line 16
2. lemma OAI.ExactQuantumFactoring.Gate.arity_le line 19
3. lemma OAI.ExactQuantumFactoring.Primitive.code_le line 22
4. lemma OAI.ExactQuantumFactoring.flatMap_length_bound line 25
5. lemma OAI.ExactQuantumFactoring.Instruction.encode_length line 37

   Source documentation

   Addresses are unary in the frozen interface; bounded gate arity ensures this encoding itself has only polynomial overhead in width and gate count.

   lemma Instruction.encode_length {q : ℕ} (o : Instruction q) :
       o.encode.length≤7+4*q := by
   …

   Mentions: OAI.ExactQuantumFactoring.Instruction

6. lemma OAI.ExactQuantumFactoring.Circuit.encode_length line 50