OAI/Computability/QuantumFactoring/FinalUniformity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTreeEmission.paddedFlag line 13
2. lemma OAI.ExactQuantumFactoring.PhysicalTreeEmission.quarterFlag line 16
3. theorem OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit_uniform line 25

   Source documentation

   A single finite Boolean-stack TM2 generates the literal family in polynomial unary-input time, including all compile-time expression and primality decisions.

   theorem finalCircuit_uniform : Uniform finalCircuit:=by
   …

   Mentions: OAI.ExactQuantumFactoring.Uniform, OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit