OAI.ExactQuantumFactoring.exact_quantum_factoring
OpenThe theorem states that the defined proposition MainTheorem holds, i.e. there is a family of quantum circuits indexed by input bit length ℓ with three properties. Circuits are lists of instructions on q qubits, each applying one of 20 named gates (the primitives NOT, CNOT, Toffoli, Hadamard and phase, each optionally inverted and optionally given one extra control) to distinct wires; the output state is obtained by applying the instructions in order to the basis state holding the binary digits of N, least significant bit first, on the first ℓ wires, with all other wires zero. First, the family is uniform: a single Turing machine (TM2) with finite stack alphabets computes in polynomial time the encoding of the ℓth circuit from the unary string of length ℓ, where the encoding writes the qubit count, instruction count and each instruction's gate code, inverse and control flags and wire indices in unary. Second, the numbers of qubits and of instructions of the ℓth circuit are both bounded by one fixed polynomial in ℓ with natural-number coefficients. Third, for every ℓ and every integer N ≥ 2 whose binary length is exactly ℓ, the circuit has at least ℓ + n² qubits, where n = max(128, ℓ), and the total squared amplitude on basis states whose output is correct equals exactly 1. A basis state is correct if reading n consecutive blocks of n bits after the input wires, each block as a binary number, gives the nondecreasing list of prime factors of N with multiplicity, padded with zeros to length n.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/ExactQuantumFactoring.lean; bytes 5939..5998 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_ExactQuantumFactoring namespace OAI namespace ExactQuantumFactoring open scoped BigOperators
theorem exact_quantum_factoring : MainTheorem := by sorry end ExactQuantumFactoring end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.