Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Complete source main theorem for the retained concrete physical family.

theorem OAI.ExactQuantumFactoring.exact_quantum_factoring line 17
Source documentation
Source Theorem 1.1 (thm:main): exact factoring over the fixed gate set, with a single finite-alphabet polynomial-time length-uniform generator and polynomial worst-case gate and qubit counts.
Distinct definitions of this name: ComparatorChallenges/ExactQuantumFactoring.lean:149 (same statement text; different proof or body). Qualify references as OAI.ExactQuantumFactoring.exact_quantum_factoring@path.
```
theorem exact_quantum_factoring : MainTheorem := by
…
```
Mentions: OAI.ExactQuantumFactoring.MainTheorem