% Oai279-A.tex % Self-contained source for pdfLaTeX. % % Suggested build commands (not executed here): % pdflatex -interaction=nonstopmode -halt-on-error Oai279-A.tex % pdflatex -interaction=nonstopmode -halt-on-error Oai279-A.tex % % Release: % A proved finite circuit certificate for N=12, with the stronger % guarantee that the same printed circuit handles every 2 <= N < 16. % % Boundary: % This independently constructed finite circuit is not identified with % an extracted instance of the external Family 279 circuit family. % The all-input uniform exact-factoring claim remains unverified here. % % The optional appendix checker is supplied as text, not executed. \documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage[margin=1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{array,booktabs,longtable,tabularx} \usepackage{enumitem} \usepackage{microtype} \usepackage{url} \usepackage[hidelinks]{hyperref} \setlength{\emergencystretch}{3em} \setlist[enumerate]{topsep=5pt,itemsep=3pt} \setlist[itemize]{topsep=5pt,itemsep=3pt} \Urlmuskip=0mu plus 1mu \allowdisplaybreaks \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{claimrecord}[theorem]{External claim record} \newtheorem{specification}[theorem]{Specification} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newtheorem{example}[theorem]{Example} \newcommand{\N}{\mathbb N} \newcommand{\Z}{\mathbb Z} \newcommand{\Q}{\mathbb Q} \newcommand{\R}{\mathbb R} \newcommand{\C}{\mathbb C} \newcommand{\Tr}{\operatorname{Tr}} \newcommand{\supp}{\operatorname{supp}} \newcommand{\ord}{\operatorname{ord}} \newcommand{\wt}{\operatorname{wt}} \newcommand{\enc}{\operatorname{enc}} \newcommand{\bit}{\operatorname{bit}} \newcommand{\id}{\operatorname{id}} \newcommand{\diag}{\operatorname{diag}} \newcommand{\ket}[1]{\lvert #1\rangle} \newcommand{\bra}[1]{\langle #1\rvert} \newcommand{\kb}[2]{\lvert #1\rangle\langle #2\rvert} \newcommand{\proj}[1]{\kb{#1}{#1}} \newcommand{\ddia}{d_{\diamond}} \newcommand{\Prob}{\mathbb P} \newcommand{\NOTCLOSED}{\texttt{NOT\_CLOSED}} \newcommand{\CX}{\operatorname{CX}} \newcommand{\CCX}{\operatorname{CCX}} \title{\textbf{Oai279-A}\\ An Explicit Finite Certificate for Exact Factoring\\[3pt] \large Fixed-gate circuit, complete output support, and an audit of Family 279} \author{Ngo Cheung} \date{14 October 2026} \begin{document} \maketitle \begin{abstract} We complete a finite-certificate task associated with the external Family 279 claim of uniform polynomial-size exact quantum factoring over a fixed gate set. The external all-input theorem is frozen and audited, not assumed. The local result is an explicitly specified circuit using only NOT, CNOT, and Toffoli gates. It contains exactly \(175\) gates, uses three clean scratch qubits, preserves its input, and outputs the complete nondecreasing prime list for every \(2\le N<16\). In particular, on the frozen input \(N=12\), its measured output is supported only on \((2,2,3)\), including multiplicities. With the external target's padded output convention, the allocated width is \(16391\) qubits. A named polynomial \[ P(t)=(t+128)^2+512 \] bounds the width and gate count of an explicitly defined uniform partial family containing this circuit. That partial family is not a factoring family for arbitrary input lengths. The audit distinguishes retained coherent history, an order candidate, a verified factorization, a known nonunit success probability, and probability-one output. It corrects two consequential shorthand statements: the bound \((1-2^{-n})^{n^{10}}>1/2\) requires the source's padding \(n\ge128\), and this probability is not the final probability-one conclusion. The source additionally engineers probability \(1/4\) before applying an exact amplification step. The inspected Lean Comparator endpoint contains \texttt{sorry}; no completed formal verification is inferred from that file. The finite construction is a transparent reversible lookup benchmark, not a new factoring speedup, an extracted instance of the external construction, a hardware demonstration, or a cryptographic break. No gravitational or recovery interpretation is supplied. \end{abstract} \tableofcontents \section{Scope and the precise completed task} \label{sec:scope} \subsection{What is proved} The main local result is Theorem~\ref{thm:finite}. It supplies: \begin{enumerate} \item one frozen integer, \(N_0=12\); \item a complete gate-list specification with no unspecified high-arity instruction; \item exact gate and qubit counts; \item a named resource polynomial; \item an algebraic proof that every measured output has the complete correct prime list. \end{enumerate} The proof actually covers all fourteen integers \(2,\ldots,15\) with the same circuit. Thus the circuit description does not depend on which four-bit input is supplied. This is an elementary finite benchmark. Its purpose is to meet the plan's certificate requirement without using the general Family 279 claim as a premise. Its construction is deliberately classical reversible computation inside the allowed quantum gate model. No quantum advantage is claimed. \subsection{What is not proved} The finite circuit is independently constructed below. It is \emph{not} identified with a circuit obtained by extracting the external proof's order trial, deferred filters, and amplification construction. There are therefore two different tasks: \begin{description}[style=nextline,leftmargin=1.8em] \item[Finite endpoint certificate.] A specified allowed circuit, on a specified input, has only correct outputs and has a specified finite resource ledger. This task is completed here. \item[Source-construction instance certificate.] A specified circuit is the output of the external construction's actual uniform generator, with all of that construction's subroutines and resource bounds checked. This stronger identification is not supplied. \item[All-input family verification.] One generator and one polynomial work for every input length and every integer of that length. This remains unverified in the present manuscript. \end{description} A finite certificate cannot, by itself, bridge the second or third gap. \subsection{Source and authorship discipline} The external manuscript is \emph{Exact quantum factoring over a fixed finite gate set}, attributed to OpenAI and dated 25 September 2026 \cite{OAI279,SourceIntro}. The requested identifier Oai279-A is used for this development. It is not an assertion of authorship by N.~Cheung, registration in another series, independent review, or journal acceptance. The supplied Cheung manuscripts are cited as scoped comparison sources, especially for reversible records, resource ledgers, complete channels, and the distinction between readout and quantum recovery. Their model-specific conclusions are not factoring subroutines. \section{Stage 0: freeze the mathematical claim and encoding} \label{sec:freeze} \subsection{Inputs and the fixed gate alphabet} For an integer \(N\ge2\), let \[ \ell(N)=\lfloor\log_2N\rfloor+1. \] Input bits are least significant first: \[ N=\sum_{j=0}^{\ell-1}2^j x_j. \] The source's padded parameter is \begin{equation} n(\ell)=\max\{128,\ell\}, \qquad B=2^{n(\ell)}. \label{eq:padding} \end{equation} This padding must not be silently replaced by \(\ell\) in numerical probability claims. The primitive gates are \[ X=\begin{pmatrix}0&1\\1&0\end{pmatrix}, \qquad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}, \qquad S=\diag(1,i), \] together with CNOT and Toffoli. The alphabet also contains their inverses and their singly controlled versions. Its maximum arity is four. The description has twenty gate names if inverse and control flags are counted separately; some names represent the same unitary. The gate alphabet is fixed once and for all. It does not contain an instruction specifying a rotation angle as part of the input. A conjunction of many controls must be synthesized into the allowed bounded-arity gates, rather than counted as one gate \cite{SourceModel,LeanTarget279}. \subsection{Complete prime-list encoding} For \(n=n(\ell)\), an output consists of \(n\) entries of \(n\) bits each. A correct output is \begin{equation} \enc_n(N)=(p_0,\ldots,p_{k-1},0,\ldots,0), \label{eq:encoding} \end{equation} where \[ 2\le p_0\le\cdots\le p_{k-1},\qquad p_j\text{ is prime},\qquad \prod_{j=0}^{k-1}p_j=N. \] Multiplicities are retained. Since \(N<2^n\) and every prime factor is at least two, \(k1\). Since \(p_i\ge i+1\), \[ \frac{\varphi(r)}r = \prod_{i=1}^k\left(1-\frac1{p_i}\right) \ge \prod_{i=1}^k\frac{i}{i+1} = \frac1{k+1} \ge\frac1{n+1}. \] The case \(r=1\) uses \(\varphi(1)=1\). Also \[ \frac1{2048r}\le\lambda(r)\le\frac1{1024r}, \qquad \varphi(r)\le r. \] Multiplying gives the assertions. \end{proof} \begin{example}[A candidate need not divide the input] Modulo \(12\), the unit \(5\) has order \(2\), since \(5\not\equiv1\pmod{12}\) and \(5^2\equiv1\pmod{12}\). The candidate \(d=10\) satisfies the order-multiple test, but \(10\nmid12\). For the true order the proposed mass is \[ \varphi(2)\lambda(2)=2^{-11}. \] This number does not appear as an input to the finite circuit below. \end{example} \subsection{Interface 3: verified data and bounded transitions} The source's process uses \[ K=n^5,\qquad L=n^{10},\qquad W=n(K+1). \] Its auxiliary data include recursively generated factorizations associated with \(p-1\). The process, its good-output predicates, and its retrospective transition probabilities are different objects from the root prime list. Its stated properties include a polynomial cap on every branch and completion of every all-good evolution \cite{SourceProcess}. A sound audit must therefore check: \begin{enumerate} \item acceptance means \emph{complete} data, not a valid fragment; \item all data needed retrospectively are generated and verified, not supplied as hidden advice; \item invalid outputs also obey the time and bit-length caps; \item a completed run is padded to exactly \(L\) slots; \item internal quantum work is counted separately from the \(W\)-bit transition output. \end{enumerate} A transition-output width is not a total workspace bound. \begin{lemma}[Sound verification of the root list] \label{lem:verifier} There is a deterministic polynomial-time verifier for \eqref{eq:encoding}. It accepts precisely the complete correctly ordered prime lists for \(N\), including the zero-padding convention. \end{lemma} \begin{proof} Check that the positive entries precede all zero entries, are at least two, and are nondecreasing. Check primality of every positive entry by a deterministic polynomial-time primality test \cite{AKS,AKSErratum}. Multiply the positive entries and compare with \(N\). There are at most \(n\) factors, each of at most \(n\) bits. Their product has at most \(n^2\) bits, including on invalid guesses. Schoolbook multiplication and all comparisons therefore have polynomial bit cost. Acceptance gives a prime product equal to \(N\), and unique factorization gives exactly the required list. The converse follows from the definition. \end{proof} This verifies a supplied root list. It does not generate that list, verify every auxiliary process invariant, or factor arbitrary \(N\). \subsection{Interface 4: completion, deferred filters, and exact output} The source's \texttt{lem:completion} concerns arithmetic equalization of passing masses. Its application depends on identifying deferred implemented tests with analytical tests on the same recorded runs. Conditioning on eventual completion instead of passing prefixes would be a different argument. There are two normalization levels in the source: first a known passing probability \[ p_*=(1-2^{-n})^L, \qquad L=n^{10}, \] then a further exact preparation with success probability \(1/4\). Only after that second step are sign reflections applied \cite{SourceExactness}. Thus ``completion fills the remaining mass'' must not be read as a classical rule that relabels every failure branch with the unknown factorization. \begin{lemma}[The padding needed for \(p_*>1/2\)] \label{lem:pstar} With the source convention \(n\ge128\) and \(L=n^{10}\), \[ 1-2^{-58}\le 1-n^{10}2^{-n}\le p_*<1. \] In particular \(p_*>1/2\). It is a dyadic rational with denominator exponent at most \(n^{11}\). \end{lemma} \begin{proof} Bernoulli's inequality gives \[ (1-2^{-n})^{n^{10}}\ge1-n^{10}2^{-n}. \] The sequence \(a_n=n^{10}2^{-n}\) decreases for \(n\ge128\): \[ \frac{a_{n+1}}{a_n} = \frac{(1+1/n)^{10}}2 \le \frac1{2(1-10/n)}<1. \] Here the middle inequality follows by bounding the finite binomial sum by the geometric series with ratio \(10/n<1\). At \(n=128\), \[ a_{128}=2^{70-128}=2^{-58}. \] The strict upper bound \(p_*<1\) is immediate. Finally, \[ p_*=\frac{(2^n-1)^{n^{10}}}{2^{n^{11}}}, \] which proves the denominator bound. \end{proof} Without padding the claimed inequality is false: at \(n=2\), \[ (1-2^{-2})^{2^{10}} = (3/4)^{1024} \le(3/4)^3<1/2. \] This is a correction to the abbreviated plan, not a contradiction of the padded source. The following standard calculation isolates the remaining quantum interface. \begin{lemma}[Exact amplification requires the correct probability] \label{lem:amplification} Let \(\psi\) be a unit vector, let \(\Pi\) be a success projector, and put \[ g=\Pi\psi,\qquad b=(I-\Pi)\psi,\qquad p=\|g\|^2. \] Then \begin{equation} (2\proj{\psi}-I)(I-2\Pi)\psi = (3-4p)g+(1-4p)b. \label{eq:amplification} \end{equation} For \(p=1/4\), the result is \(2g\), a unit vector wholly supported in the success subspace. \end{lemma} \begin{proof} The first sign flip gives \(-g+b\), whose inner product with \(\psi=g+b\) is \(1-2p\). Apply the second reflection: \[ 2(1-2p)(g+b)-(-g+b) = (3-4p)g+(1-4p)b. \] If \(p=1/4\), the bad component vanishes and \(\|2g\|^2=4p=1\). \end{proof} This is the one-step special case of amplitude amplification \cite{BHMT,MoscaZalka}. Knowing merely that \(p>1/2\) is not enough: its bad-output probability after this step would be \[ (1-p)(1-4p)^2, \] which is nonzero for \(1/20\). If \(\ell\ge128\), the difference is \(255\ell+16893>0\). Its gate count is either zero or \(175\), also at most \(P(\ell)\). The partial family is length-uniform: compute \(n(\ell)\) and its width, and print the one fixed gate list precisely when \(\ell=4\). No input integer or factorization is consulted. This does not evade the all-input issue by changing quantifiers: the partial family explicitly \emph{fails} the general factoring endpoint at other lengths. \subsection{The one completed next theorem} \begin{theorem}[Oai279-A finite exact-output certificate] \label{thm:finite} The circuit specified in Section~\ref{sec:finite} satisfies: \begin{enumerate} \item It uses only the frozen gate alphabet, with exactly \(175\) gates and allocated width \(16391\). \item Its input register is preserved and its three scratch qubits are restored to zero. \item For every \(2\le N<16\), \begin{equation} U_4\ket{N}_I\ket{0^{16384}}_Y\ket{000}_{uvf} = \ket{N}_I\ket{\enc_{128}(N)}_Y\ket{000}_{uvf}. \label{eq:finite-action} \end{equation} \item In particular, for the frozen \(N_0=12\), \[ \Prob\bigl\{Y=(2,2,3,0^{125})\bigr\}=1, \] and the probability of every other output word is zero. \item The named polynomial \eqref{eq:resource-polynomial} bounds the gates and width of the length-uniform partial family just defined. At the frozen length, \[ 175\le P(4)=17936, \qquad 16391\le P(4)=17936. \] \end{enumerate} No order-trial law, value of \(p_*\), general primality algorithm, or external Family 279 theorem is assumed. \end{theorem} \begin{proof} For a fixed input \(N\), Lemma~\ref{lem:row} shows that all rows except row \(N\) leave the output unchanged. Row \(N\) writes exactly the word with one positions \(T_N\). All later row blocks have a false equality predicate and all scratch starts and ends zero. The table and Lemma~\ref{lem:table} identify this output word with \(\enc_{128}(N)\). This proves \eqref{eq:finite-action}. The gates are permutations on computational basis states, so the right side is exactly one basis vector of amplitude one, with no unlisted branch. For \(N=12\), the complete final basis vector has one positions \begin{equation} \{2,3,5,133,260,261\}. \label{eq:final-bits} \end{equation} The first two are the preserved input bits. The remaining four encode the three prime entries \(2,2,3\). Thus its output marginal is \[ \proj{\enc_{128}(12)}, \] which proves the probability-one support assertion. The gate and width ledgers are Lemma~\ref{lem:gatecount} and the register allocation. The polynomial inequalities and the generator were established above. \end{proof} \begin{remark}[What this theorem deliberately does not exercise] The circuit is a finite reversible lookup, not the source's order-finding or completion circuit. Its transparent exactness does not test the hardest interfaces of that construction. This is not disguised as a new asymptotic result. Scaling the same lookup method to all \(\ell\)-bit inputs introduces exponentially many rows. Polynomial bounds on this partial family do not turn that exponential construction into a general factoring algorithm. \end{remark} \subsection{Arithmetic support values at the frozen input} At \(\ell_0=4\), the source's padding still gives \(n=128\). Consequently, \[ K=2^{35},\qquad L=2^{70},\qquad W=2^{42}+128, \] and the prescribed known probability would be \begin{equation} p_*= \frac{(2^{128}-1)^{2^{70}}}{2^{2^{77}}}, \qquad 1-2^{-58}\le p_*<1. \label{eq:frozen-pstar} \end{equation} These are exact arithmetic identities, not the resource ledger or success probability of \(U_4\). The finite certificate does not claim to have allocated the source process's \(L\) transition records or evaluated its huge numerator. Similarly, the order example \(a=5\) modulo \(12\) supplies \(\varphi(2)\lambda(2)=2^{-11}\) only as arithmetic support for understanding the proposed order-trial statement. The circuit \(U_4\) does not call that trial. \section{Stage 2: price the comparisons, not a missing algorithm} \label{sec:pricing} \subsection{Finite reversible synthesis and its scaling boundary} The local construction uses ordinary reversible compute--copy--uncompute. Cheung's VIII-C includes a different finite-dictionary permutation-completion lemma with an explicit gate count proportional to the dictionary size \cite[{\texttt{lem:completion}}]{CheungVIIIC}. It is a relevant comparison, but it is not the source's \emph{dyadic probability completion}. The two uses of the word ``completion'' have different types: \[ \begin{array}{ll} \text{permutation completion:}& \text{extend an injective finite update to a reversible permutation};\\[2pt] \text{dyadic completion:}& \text{engineer a specified exact passing probability}. \end{array} \] Neither supplies the other. A dictionary may have \(2^\ell\) entries even when each entry has only polynomially many bits. \subsection{A record of primes is a classical output} For a measured register \(Q\), define its destructive record channel by \[ \mathcal M(X) = \sum_z \kb zz_R\otimes (\bra z_Q\otimes I)X(\ket z_Q\otimes I). \] Expansion in the measured basis gives \begin{equation} \Tr_R\mathcal M(X)=\Tr_QX. \label{eq:readout-drop} \end{equation} The same identity holds with any untouched reference. This is a complete readout-and-drop identity. It is not probability-one factoring. To obtain a prime list, the preceding circuit must first satisfy the arithmetic support condition. If only a classical record is available for recovering an unknown quantum state, any subsequent quantum-output decoder is measure-and-prepare. On half of an entangled input it produces a separable state, whereas the identity preserves the entanglement. Thus record-only quantum recovery and computation of a classical function are different tasks \cite{Watrous,CheungVIIIB,CheungHawk04B}. Landmark I concerns the declared destructive-readout semantics \cite{CheungI}. The coherent simulation in Lemma~\ref{lem:records-local} is not an invocation of Enter in the middle of an interference computation. \subsection{One-shot instrument dimension is not circuit size} En02-A's one-shot instrument ledger prices a specified dilation and readout through its branch Choi ranks \cite[{\texttt{thm:Dprime}}]{CheungEn02A}. That ledger does not provide: \begin{itemize} \item a length-uniform generator; \item a decomposition into the frozen exact gate set; \item a worst-case time bound for a controller; \item an order-finding procedure. \end{itemize} A general Stinespring unitary is not automatically an exact finite word over the frozen alphabet. For the certificate here, the ledger is explicit instead: \(16384\) initialized output qubits, three initialized scratch qubits, four input qubits, and \(175\) listed gates. No hidden environmental register is required to implement this permutation. En02-B's certificate discipline requires the actual programme, complete maps, and live-register accounting \cite[{\texttt{thm:B1}}]{CheungEn02B}. It does not construct the order trial by serving as a template. \subsection{Finite samples cannot prove exact support} \begin{proposition}[No zero-error conclusion from finitely many successes] \label{prop:statistics} Fix a circuit input and suppose independent attempted runs have failure probability \(\varepsilon\). For every finite \(M\) and every \(0<\varepsilon<1\), the probability of observing no failures in \(M\) runs is \[ (1-\varepsilon)^M>0. \] Therefore an observation of finitely many successes cannot alone distinguish exact zero failure from every positive failure probability. \end{proposition} \begin{proof} Independence multiplies the \(M\) success probabilities. The resulting product is strictly positive. \end{proof} En01-B and En01-C price statistical statements under declared record and sampling assumptions \cite{CheungEn01B,CheungEn01C}. Such coverage can be useful for a device, but it is not the algebraic zero statement \eqref{eq:exact-support}. Likewise, Em03-G's supplied \texttt{thm:lower} gives a strictly positive obstruction at each finite model parameter \cite{CheungEm03G}. The compatibility of such a bound with vanishing error along a growing-resource family does not turn the error into zero at any finite resource. \subsection{A small implementation budget is not exactness} \begin{proposition}[Arbitrarily small noise can destroy the certificate] \label{prop:noise} For every \(0<\varepsilon<1\), there is a CPTP implementation perturbation of the finite circuit at half-diamond distance at most \(\varepsilon\) whose output on \(N_0=12\) is incorrect with probability exactly \(\varepsilon\). \end{proposition} \begin{proof} After the ideal circuit, apply \[ \mathcal E_\varepsilon = (1-\varepsilon)\id+\varepsilon\operatorname{Ad}_{X_5}, \] where \(X_5\) flips output wire \(5\). The two branches are CPTP. The half-diamond distance from the identity is at most \(\varepsilon\), by convexity and the maximum channel distance one \cite{Watrous}. In the ideal output, wire \(5\) is the only one bit of the first prime entry \(2\). Flipping it changes that entry to zero while leaving the later entries \(2,3\) positive. The resulting word is not a valid zero-padded prime list for \(12\). Thus exactly the perturbed branch is wrong, with probability \(\varepsilon\). \end{proof} A constant-error synthesis or diamond-distance certificate may bound failure. It does not prove it is zero. No implementation claim about an existing device is made. \subsection{Debugged comparison table} \begin{longtable}{@{}p{.23\linewidth}p{.35\linewidth}p{.34\linewidth}@{}} \toprule Template & Legitimate role & What it does not supply\\ \midrule \endfirsthead \toprule Template & Legitimate role & What it does not supply\\ \midrule \endhead \bottomrule \endfoot Landmark I & Declared destructive readout and classical records. & A factoring controller or exact order trial.\\[5pt] VIII-B, \texttt{prop:classical-recovery} & The supplied sharp record-only quantum-recovery obstruction. & An obstruction to computing a classical prime list.\\[5pt] En07-A & Complete outputs, recovery criteria, and separately stated readout-and-drop conventions. & Probability-one factoring. Its supplied \texttt{thm:exact} is a recovery criterion, not \eqref{eq:readout-drop}'s factoring proof.\\[5pt] Hawk04-B & Typed classical readout versus full quantum recovery. & A decomposition into the present gate set. An unsupplied \texttt{cor:gravity} is not invented.\\[5pt] En02-A, \texttt{thm:Dprime} & One-shot pure-environment and instrument dimension accounting. & Uniform generation or exact gate synthesis.\\[5pt] En02-B, \texttt{thm:B1} & Soundness and live-name accounting of a supplied programme. & Order finding or a missing circuit.\\[5pt] En01-B/C & Finite-sample statements for complete declared records. & A proof that every wrong-output amplitude is zero.\\[5pt] Em03-G, \texttt{thm:lower} & A finite-parameter positive error lower bound. & A theorem that a limiting error is already zero.\\[5pt] Oai272-A comparison & A nominated secret-bit protocol comparison in the supplied dossier. & Integer factorization or an independently verified external Family 272 theorem.\\[5pt] Oai265-A, \texttt{thm:separation} & Separation of selected records, spectra, recovery, and histories. & A prime list or a factoring circuit.\\[5pt] Oai283-A comparison & A nominated constant-error oracle-synthesis comparison. & Probability-one factoring; its unnamed implementation is not imported.\\[5pt] Family 274 context & A catalogue claim concerning constant-depth parity. & An all-depth obstruction to polynomial-size factoring. Its lower-bound proof is not a premise here.\\ \end{longtable} The Cheung references are restricted to the supplied manuscript versions and passages \cite{CheungI,CheungVIIIB,CheungVIIIC,CheungEn07A, CheungHawk04B,CheungEn02A,CheungEn02B,CheungEn01B, CheungEn01C,CheungEm03G,CheungOai265A}. The other nominated comparisons are retained as dossier descriptions, not reconstructed theorems \cite{Dossier}. \section{Stage 3: an existence theorem, a generator, and one circuit} \label{sec:existence} \subsection{The quantifiers matter} For any fixed \(N\), a circuit that writes its already known factorization is easy to specify. That establishes only a statement with the weak quantifier pattern \[ \forall N\ \exists C_N. \] It does not establish a polynomial-time length generator whose output handles every \(N\) of that length. Similarly, any finite collection of factorizations can be compiled into a finite reversible lookup table. Its gate count depends on the number of rows. Treating that row count as a constant while claiming an unbounded-input theorem would change the resource model. The local circuit avoids a vacuous single-answer demonstration by handling every \(2\le N<16\), but it does not pretend that this finite improvement proves the stronger uniform quantifier. \subsection{An unnamed polynomial is not automatically an error} An existence theorem may legitimately assert \(\exists P\) without displaying coefficients in its statement. A fully specified algorithm and a proof of a polynomial bound can establish that assertion. The plan's demand is narrower and more concrete: the finite certificate should name the polynomial used in its ledger. Equation~\eqref{eq:resource-polynomial} does so for the independently defined partial family. It is not advertised as the resource polynomial of the external general construction. To certify an extracted source instance, one would need its actual generator, gate expansion, denominator bounds, controlled arithmetic circuits, and inverse-work ledger. Naming a large polynomial without establishing those inequalities would not fill that gap. \subsection{The exact completion is not a file name} The inspected Comparator defines a target proposition and contains a placeholder at its main endpoint. Its mere existence is neither an executable circuit nor a completed formal proof \cite{LeanTarget279}. Conversely, a mathematical proof need not print every gate at every length to be a valid proof of uniformity. What it must supply is a well-defined generator, its correctness, and its resource bound. This manuscript neither denies that possibility nor treats an unverified scope description as its accomplishment. \section{Stage 4: alter one hypothesis at a time} \label{sec:weaken} \subsection{Bounded error and exact output} Shor supplies a foundational polynomial-time quantum factoring algorithm with a randomized success guarantee \cite{Shor}. That is a cited precursor, not a proof of the frozen fixed-alphabet probability-one claim. If an independent trial succeeds with probability \(s<1\), \(M\) independent repetitions still all fail with probability \[ (1-s)^M>0 \] at every finite \(M\). A retry-until-success strategy may halt almost surely and have finite expected time, while having no finite worst-case bound. These are different claims. Exact algorithms in other models also require their gate and input assumptions to be matched; computed-angle exact Fourier transforms do not automatically give an exact circuit over the frozen alphabet \cite{MoscaZalka}. \subsection{One divisor and the complete list} A divisor certificate checks \[ 1