Oai279-A An Explicit Finite Certificate for Exact Factoring Fixed-gate circuit, complete output support, and an audit of Family 279

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

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\ge 128$, 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 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.

The main local result is Theorem thm:finite. It supplies:

1. one frozen integer, $N_0=12$;

2. a complete gate-list specification with no unspecified high-arity instruction;

3. exact gate and qubit counts;

4. a named resource polynomial;

5. an algebraic proof that every measured output has the complete correct prime list.

The proof actually covers all fourteen integers $2,\dots ,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.

The finite circuit is independently constructed below. It is 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:

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.

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.

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.

A finite certificate cannot, by itself, bridge the second or third gap.

The external manuscript is Exact quantum factoring over a fixed finite gate set, attributed to OpenAI and dated 25 September 2026 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.

For an integer $N\ge 2$, let

Input bits are least significant first:

The source's padded parameter is

This padding must not be silently replaced by $\ell$ in numerical probability claims.

The primitive gates are

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 SourceModel,LeanTarget279.

For $n=n(\ell )$, an output consists of $n$ entries of $n$ bits each. A correct output is

where

Multiplicities are retained. Since $N<2^n$ and every prime factor is at least two, $k<n$. Every entry fits in $n$ bits. Unique factorization makes ${\mathrm{enc}}_n(N)$ unique.

The output wire for bit $j$ of entry $a$ is

This agrees with the inspected Comparator's convention LeanTarget279. Zero padding is not a prime entry.

Let $U$ be a circuit on an input register $I$, an output register $Y$, and work registers $W$. All registers except $I$ start in zero. For a basis input $N$, write

Let ${\Pi }_{\mathrm{bad},N}$ project onto basis states whose output register does not encode the complete prime factorization of $N$. The circuit is exact on $N$ if

Because the circuit is unitary, (eq:exact-support) is equivalent to correct measured output with probability one. It does not require the work register to be zero. It also does not require every intermediate trial to succeed.

A circuit family is length-uniform if one deterministic classical algorithm receives only $1^{\ell }$ and prints the circuit for all $\ell$-bit inputs in time polynomial in $\ell$. Polynomial resources mean that one fixed polynomial $P$ bounds both its gate count and its allocated qubit count for every $\ell$.

The generator does not receive the factorization as advice. Nor may it perform an unpriced, input-specific factoring computation before printing a constant-output circuit.

Family 279-01 asserts that there exists a length-uniform polynomial-resource circuit family over the frozen alphabet which, for every $N\ge 2$, outputs ${\mathrm{enc}}_{n(\ell (N))}(N)$ with probability one OAI279,SourceIntro.

Record rec:main is not a hypothesis of Theorem thm:finite.

The note lean/docs/279.md describes the intended endpoint as a uniform polynomial-resource family with probability-one complete factorization LeanScope279. That is a scope statement.

In the inspected lean/ComparatorChallenges/ExactQuantumFactoring.lean, the endpoint is

theorem exact_quantum_factoring : MainTheorem := by sorry

LeanTarget279. Consequently, that file's endpoint is not a completed proof of its theorem body. This observation does not classify uninspected files or assert that no other proof artifact can exist. No Lean execution or completed formalization is claimed here.

A coherent record and a destructive measurement are different operations. A CNOT applied to a basis label copies that label; on an unknown superposition it may create entanglement. It is not a record-free measurement rule.

Suppose a hybrid procedure has polynomial worst-case time, polynomial workspace, computational-basis measurements, and a polynomial-time classical controller. Its quantum instructions come from the frozen alphabet. Then its classical-output distribution has a polynomial-size unitary implementation which retains polynomially many history and work qubits. The inverse is obtained by reversing the gate list and inverting the gates.

Proof. Replace a computational-basis measurement by CNOT copies into fresh history wires. A branch with history $h$ has the form

Distinct recorded histories are orthogonal. Controlled subsequent operations preserve the same branch squared norms and classical output distributions as the measured procedure. A reset is implemented by retaining the old factor and using a fresh zero wire.

Simulate the classical controller reversibly: compute intermediate Boolean values into fresh wires, retain the necessary configuration history, and use a halted flag after termination. AND is implemented by Toffoli, and XOR and copying by CNOT. No exponentially large decision tree needs to be printed. This is the compute–retain–reverse discipline of reversible computation Bennett,Toffoli.

Addressed quantum instructions can be compiled by enumerating ordered distinct tuples of physical wire addresses. There are at most $w^4$ tuples when the workspace has width $w$. For each tuple, reversibly compute the selection predicate, apply the selected controlled gate, and uncompute the predicate.

If the selected instruction already has an extra control, combine that control with the selection bit into a temporary conjunction before applying the singly controlled primitive. This avoids adding an unauthorized higher-arity gate to the alphabet.

The number of time steps, tuples, controller operations, measurement bits, and retained configurations is polynomial. Their gate-list generation is polynomial as well. Reversing that list gives the inverse.

The source's lem:records has this role SourceModel. The record discipline also has a scoped analogue in Cheung's En01-A branch normal form and En02-B programme soundness CheungEn01A,CheungEn02B. Those manuscripts do not construct the factoring controller.

History is retained during the preparation so that its branch probabilities are represented correctly. A later inverse circuit may act on and uncompute that history. Permanently measuring or discarding it before amplitude amplification can destroy the required inverse. Retaining history does not mean forbidding its later coherent use.

For a unit $a$ modulo $m$, define

The frozen order-trial claim is

with output either no candidate or $1\le d<B$ satisfying $r\mid d$. The trial receives $m,a$, not $r$ or a factorization.

The source uses an interpolated phase construction, actual unnormalized ancillary success probabilities, and exact correction branches SourceOrder,SourceDyadic. The audit must check:

1. the actual fixed-gate implementation, not an ideal Fourier transform substituted afterwards;

2. the uniqueness and efficient recovery of candidate labels;

3. the exact mass identity (eq:order-law), including $r=1$;

4. polynomial evaluation of correction totals without summing an exponential number of residues;

5. no use of an unknown order in the implementation.

None of these is discharged merely by quoting Shor's algorithm.

Two elementary consequences can nevertheless be proved directly.

If $a$ is a unit modulo $m$, then

For $1\le r<2^n$, the right-hand side of (eq:order-law) satisfies

These are arithmetic statements about the proposed law, not a construction of a trial realizing it.

Proof. Divide $d=qr+s$, with $0\le s<r$. If $a^d=1$, then $a^s=1$, so minimality of $r$ forces $s=0$. The converse is immediate.

Let $p_1<\cdots <p_k$ be the distinct prime divisors of $r>1$. Since $p_i\ge i+1$,

The case $r=1$ uses $\phi (1)=1$. Also

Multiplying gives the assertions.

Modulo $12$, the unit $5$ has order $2$, since $5\not\equiv 1(\mathrm{mod}12)$ and $5^2\equiv 1(\mathrm{mod}12)$. The candidate $d=10$ satisfies the order-multiple test, but $10\nmid 12$. For the true order the proposed mass is

This number does not appear as an input to the finite circuit below.

The source's process uses

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 SourceProcess.

A sound audit must therefore check:

1. acceptance means complete data, not a valid fragment;

2. all data needed retrospectively are generated and verified, not supplied as hidden advice;

3. invalid outputs also obey the time and bit-length caps;

4. a completed run is padded to exactly $L$ slots;

5. internal quantum work is counted separately from the $W$-bit transition output.

A transition-output width is not a total workspace bound.

There is a deterministic polynomial-time verifier for (eq:encoding). It accepts precisely the complete correctly ordered prime lists for $N$, including the zero-padding convention.

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 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.

This verifies a supplied root list. It does not generate that list, verify every auxiliary process invariant, or factor arbitrary $N$.

The source's 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

then a further exact preparation with success probability $1/4$. Only after that second step are sign reflections applied SourceExactness. Thus “completion fills the remaining mass” must not be read as a classical rule that relabels every failure branch with the unknown factorization.

With the source convention $n\ge 128$ and $L=n^{10}$,

In particular $p_{\ast }>1/2$. It is a dyadic rational with denominator exponent at most $n^{11}$.

Proof. Bernoulli's inequality gives

The sequence $a_n=n^{10}{2}^{-n}$ decreases for $n\ge 128$:

Here the middle inequality follows by bounding the finite binomial sum by the geometric series with ratio $10/n<1$. At $n=128$,

The strict upper bound $p_{\ast }<1$ is immediate. Finally,

which proves the denominator bound.

Without padding the claimed inequality is false: at $n=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.

Let $\psi$ be a unit vector, let $\Pi$ be a success projector, and put

Then

For $p=1/4$, the result is $2g$, a unit vector wholly supported in the success subspace.

Proof. The first sign flip gives $-g+b$, whose inner product with $\psi =g+b$ is $1-2p$. Apply the second reflection:

If $p=1/4$, the bad component vanishes and $\Vert 2g{\Vert }^2=4p=1$.

This is the one-step special case of amplitude amplification BHMT,MoscaZalka. Knowing merely that $p>1/2$ is not enough: its bad-output probability after this step would be

which is nonzero for $1/2<p<1$.

Suppose a unitary preparation $V$, preserving a classical input, uses $g_V$ frozen-alphabet gates on $w\ge 1$ workspace qubits, and has a success flag of probability exactly $1/4$. Suppose every successful basis output is correct. Then one amplification step gives probability-one correct output using at most

gates and at most $w-1$ extra clean scratch qubits.

Proof. The success sign is $S^2$ on its flag, costing two gates. The reflection about $V|0⟩$ is implemented, up to a global minus sign, by $V$, a sign flip on the all-zero workspace, and $V^{-1}$.

For the zero test, negate all $w$ workspace bits, compute their conjunction by a Toffoli chain, apply $S^2$, uncompute, and undo the negations. For $w\ge 2$, this costs

gates and $w-1$ clean scratch qubits. For $w=1$, use $X{S}^{2}X$, also of cost four. All scratch returns to zero.

Counting the initial preparation and the two preparations in the reflection gives three uses of $V$ or $V^{-1}$. Lemma lem:amplification proves correctness. No input-dependent rotation is used.

The hypothesis supplying $V$ is substantial. This lemma does not construct the source's quarter-success preparation or certify its uniform resource bounds.

Agrawal–Kayal–Saxena gives deterministic polynomial-time primality testing AKS,AKSErratum. The source's appendix presents its own polynomial-congruence primality argument SourcePrimality. These are distinct proof objects.

For the local finite circuit, neither general primality algorithm is needed: all primes which occur are at most $13$, and their primality is checked directly below. Consequently, the finite certificate does not import or verify the source appendix.

A certificate for an integer $N_0$ consists of:

1. the input, output, work, and initialization conventions;

2. a finite gate list, or a finite rule that expands uniquely to that list without an oracle;

3. allowed-gate and distinct-wire checks;

4. an exact allocated-width and gate-count ledger;

5. a named resource bound, with its scope stated;

6. a proof of the support identity (eq:exact-support).

A list of observed outputs, however large, is not item 6.

A finite rule is allowed here only when its expansion is specified completely. “Apply the factoring subroutine” is not such a rule.

Let

Every entry of every frozen gate lies in $\mathcal{R}$, including controlled gates and inverses. Therefore a circuit state on a basis input has amplitudes in $\mathcal{R}$.

Every element of $\mathcal{R}$ has a representation

Such an element is zero precisely when $a=b=c=d=0$. Accordingly, a finite circuit's bad-output amplitudes admit exact symbolic zero checks.

Proof. The displayed form is closed under addition, multiplication, conjugation, and the generators of $\mathcal{R}$, after enlarging the denominator when necessary. If $\alpha =0$, its real and imaginary parts vanish. Irrationality of $\sqrt{2}$ gives $a=b=0$ and $c=d=0$. The converse is immediate.

This is an exact arithmetic interface, not an efficient general simulation theorem: enumerating all basis amplitudes can take exponential time. The circuit below is a basis permutation, so its certificate needs only its reversible Boolean action.

On two qubits initially $|00⟩$, apply $H$ to the first, then controlled-$H$ from the first to the second, then $H$ to the first. The amplitude of $|00⟩$ is

and its probability is

Thus exact dyadic sampling is a designed subroutine, not a universal property of every circuit over the frozen alphabet.

Freeze

The register allocation is:

Only the input is nonzero initially. Idle output wires count in the allocation; they are not free because the source uses a wide padded encoding.

We write $\mathrm{CCX}(a,b;c)$ for the Toffoli gate with control wires $a,b$ and target $c$, and $\mathrm{CX}(a;c)$ for CNOT. The symbols $u,v,f$ denote the actual scratch addresses in the table, not additional unspecified registers.

For $2\le m<16$, let $\mathcal{F}(m)$ be the complete sorted prime list. The following table supplies $\mathcal{F}(m)$, the set $Z_m$ of input bit positions where $m$ has a zero, and the set $T_m$ of output wires to be toggled.

The output addresses follow (eq:output-address). For example, the first three entries begin at wires $4,132,260$. Their low-bit encodings of $(2,2,3)$ have ones at $5,133,260,261$.

Every displayed $\mathcal{F}(m)$ is the complete nondecreasing prime list for $m$.

Proof. The primes occurring are

The primality of $2,3$ is immediate. For $5,7$, only a divisor $2$ needs checking below their square roots. For $11,13$, only $2,3$ need checking. The respective remainders are nonzero.

The composite rows use the identities

Every list is sorted and its product is its row label. Unique factorization proves completeness, including multiplicities.

For each row $m=2,3,\dots ,15$, perform the following block, in the displayed order:

1. Apply $X_j$ for $j\in Z_m$, in increasing order.

2. Apply

   $$\mathrm{CCX}(0,1;u),\mathrm{CCX}(u,2;v),\mathrm{CCX}(v,3;f).$$

3. Apply $\mathrm{CX}(f;t)$ for $t\in T_m$, in increasing order.

4. Apply

   $$\mathrm{CCX}(v,3;f),\mathrm{CCX}(u,2;v),\mathrm{CCX}(0,1;u).$$

5. Apply $X_j$ for $j\in Z_m$, in decreasing order.

Concatenate all fourteen blocks in increasing $m$. This defines $U_4$.

Every instruction is now determined by a finite table and a fixed expansion rule. There is no instruction of the form “compare four bits” counted as one gate; the comparison is the explicit three-Toffoli conjunction chain. Every gate acts on distinct appropriate wires.

On scratch-zero inputs, row $m$ acts as

where $e_m$ is the output word whose one positions are $T_m$. The statement holds for arbitrary output word $y$.

Proof. After the initial NOT gates, input bit $j$ equals one exactly when its original value matches bit $j$ of $m$. The three scratch computations therefore give

The CNOTs XOR $e_m$ into $y$ exactly when this predicate is one. The reversed conjunction chain restores $f,v,u$ to zero, since no input bit changed during the target operations. The final NOTs restore the original input.

All these are identities on basis vectors, with no relative phase. Linearity extends the identity to their superpositions.

The circuit $U_4$ contains exactly

Its total gate count is $175$, with no intermediate measurements, no retries, and three scratch qubits returned to zero.

Proof. Each row uses $2|Z_m|$ NOTs, six Toffolis, and $|T_m|$ CNOTs. The table gives

Thus the total is

Scratch restoration follows from Lemma lem:row. The gate list has fixed length, independent of the input.

Define

To make the resource claim nonvacuous, define a partial family ${\mathcal{C}}_{\ell }$ as follows:

• its allocated width is

  $$q_{\ell }=\ell +n(\ell {)}^2+3;$$

• if $\ell =4$, its gate list is the expansion defining $U_4$;

• otherwise, its gate list is empty.

At other lengths this family is not asserted to factor anything.

For every $\ell \ge 0$,

If $\ell \le 128$, subtracting $q_{\ell }$ from $P(\ell )$ gives ${\ell }^2+255\ell +509>0$. If $\ell \ge 128$, 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 fails the general factoring endpoint at other lengths.

The circuit specified in Section sec:finite satisfies:

1. It uses only the frozen gate alphabet, with exactly $175$ gates and allocated width $16391$.

2. Its input register is preserved and its three scratch qubits are restored to zero.

3. For every $2\le N<16$,

   $$U_4|N{⟩}_I|0^{16384}{⟩}_Y|000{⟩}_{uvf}=|N{⟩}_I|{\mathrm{enc}}_{128}(N){⟩}_Y|000{⟩}_{uvf}.$$

4. In particular, for the frozen $N_0=12$,

   $$\mathbb{P}\{Y=(2,2,3,0^{125})\}=1,$$

   and the probability of every other output word is zero.

5. The named polynomial (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,16391\le P(4)=17936.$$

No order-trial law, value of $p_{\ast }$, general primality algorithm, or external Family 279 theorem is assumed.

Proof. For a fixed input $N$, Lemma 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 lem:table identify this output word with ${\mathrm{enc}}_{128}(N)$. This proves (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

The first two are the preserved input bits. The remaining four encode the three prime entries $2,2,3$. Thus its output marginal is

which proves the probability-one support assertion.

The gate and width ledgers are Lemma lem:gatecount and the register allocation. The polynomial inequalities and the generator were established above.

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.

At ${\ell }_0=4$, the source's padding still gives $n=128$. Consequently,

and the prescribed known probability would be

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 $\phi (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.

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 CheungVIIIC ({lem:completion}). It is a relevant comparison, but it is not the source's dyadic probability completion.

The two uses of the word “completion” have different types:

Neither supplies the other. A dictionary may have $2^{\ell }$ entries even when each entry has only polynomially many bits.

For a measured register $Q$, define its destructive record channel by

Expansion in the measured basis gives

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 Watrous,CheungVIIIB,CheungHawk04B.

Landmark I concerns the declared destructive-readout semantics CheungI. The coherent simulation in Lemma lem:records-local is not an invocation of Enter in the middle of an interference computation.

En02-A's one-shot instrument ledger prices a specified dilation and readout through its branch Choi ranks CheungEn02A ({thm:Dprime}). That ledger does not provide:

• a length-uniform generator;

• a decomposition into the frozen exact gate set;

• a worst-case time bound for a controller;

• an order-finding procedure.

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 CheungEn02B ({thm:B1}). It does not construct the order trial by serving as a template.

Fix a circuit input and suppose independent attempted runs have failure probability $\epsilon$. For every finite $M$ and every $0<\epsilon <1$, the probability of observing no failures in $M$ runs is

Therefore an observation of finitely many successes cannot alone distinguish exact zero failure from every positive failure probability.

Proof. Independence multiplies the $M$ success probabilities. The resulting product is strictly positive.

En01-B and En01-C price statistical statements under declared record and sampling assumptions CheungEn01B,CheungEn01C. Such coverage can be useful for a device, but it is not the algebraic zero statement (eq:exact-support).

Likewise, Em03-G's supplied thm:lower gives a strictly positive obstruction at each finite model parameter 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.

For every $0<\epsilon <1$, there is a CPTP implementation perturbation of the finite circuit at half-diamond distance at most $\epsilon$ whose output on $N_0=12$ is incorrect with probability exactly $\epsilon$.

Proof. After the ideal circuit, apply

where $X_5$ flips output wire $5$. The two branches are CPTP. The half-diamond distance from the identity is at most $\epsilon$, by convexity and the maximum channel distance one 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 $\epsilon$.

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.

The Cheung references are restricted to the supplied manuscript versions and passages CheungI,CheungVIIIB,CheungVIIIC,CheungEn07A, CheungHawk04B,CheungEn02A,CheungEn02B,CheungEn01B, CheungEn01C,CheungEm03G,CheungOai265A. The other nominated comparisons are retained as dossier descriptions, not reconstructed theorems Dossier.

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

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.

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 (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.

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 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.

Shor supplies a foundational polynomial-time quantum factoring algorithm with a randomized success guarantee 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

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 MoscaZalka.

A divisor certificate checks

It does not certify that either $d$ or $N/d$ is prime. The root-list verifier in Lemma lem:verifier adds primality, ordering, complete product, and padding checks.

A bounded factoring recursion also needs its own worst-case control. Repeated successful splits have at most $\ell (N)$ prime leaves, but this does not bound the number of failed attempts unless those attempts are separately capped.

Every finite circuit has a numerical depth. A constant-depth family claim requires a single depth bound for an unbounded input domain, with a specified gate and ancilla model.

Family 274 is a separate catalogue entry concerning ${\mathrm{QAC}}^0$ parity Scope274. Its claimed obstruction does not by itself obstruct a growing-depth polynomial-size circuit. No reduction from that parity question is established here.

In particular, the $175$-gate finite benchmark is not evidence for constant-depth factoring on arbitrary inputs.

Dropping uniformity permits circuit descriptions not generated by the required single efficient classical machine. That changes the theorem. Dropping the polynomial-size restriction as well permits exhaustive finite tables at every length.

Our partial family's uniformity is elementary because the only nonempty gate list is fixed at $\ell =4$. Its failure to solve the general problem is explicit, not hidden behind advice terminology.

The certified object consists of finite registers, a gate list, initial states, a measured output, and an arithmetic decoder of that output. Its proof uses Boolean identities and elementary arithmetic.

It specifies no spacetime metric, gravitational mediator, horizon, radiation algebra, evaporation dynamics, generalized entropy, or island extremization. The prime output is a classical list, not a metric or a time-indexed radiation-entropy history.

The same finite circuit can be regarded solely as an abstract reversible Boolean network. Consequently its exact factorization identity does not determine any of those additional physical objects.

Equation (eq:readout-drop) is destructive readout with a retained classical record. It is compatible with exact evaluation of a classical function. It is not a reference-preserving quantum recovery channel.

This is the appropriate scope of the readout and recovery comparisons in Cheung's I, VIII-B, En07-A, and Hawk04-B CheungI,CheungVIIIB,CheungEn07A,CheungHawk04B. A typed output interface cannot supply an unconstructed arithmetic algorithm, and an arithmetic output cannot supply a gravitational dictionary.

An abstract factoring theorem can be relevant to cryptographic assumptions. A finite benchmark for $12$, however, provides no implementation of a large-key attack, no fault-tolerant device, no runtime estimate for a deployed key, and no operational breach.

The statement “existing devices factor” is not a conclusion of this manuscript. Neither is the broader assertion that factoring would have no cryptographic consequences. The absent claim is a demonstrated cryptographic break from this certificate.

The supplied XIV–XV–XVI excerpts concern distributions, characteristic compositions, reconstruction identities, and quantum-coefficient admission. Their domains and unresolved obligations are not circuit wires or Boolean arithmetic.

In particular, this finite circuit constructs no joint characteristic map, joint section, transverse estimate, contact compatibility theorem, output wavefront bound, or admitted quantum coefficient. Cheung's XIV-J and XV-B explicitly separate those interfaces CheungXIVJ,CheungXVB. The present proof does not enter that analytic chain.

The exact completed numerical ledger is

The following remain unverified or outside scope:

1. the full Family 279-01 construction and its uniform all-input correctness;

2. an extraction linking $U_4$ to that source construction;

3. a completed proof of the inspected Comparator endpoint;

4. a general constant-depth factoring theorem;

5. a hardware implementation or practical cryptographic break;

6. a Page curve, island, horizon, Hawking-radiation derivation, gravity-generated entanglement, or exclusion of classical gravity.

The finite certificate is complete. It does not create a logical requirement that all other research must wait for this particular benchmark. Rather, it removes one finite deliverable while leaving the stronger verification tasks visible.

The following program expands the literal gate specification and checks its Boolean action on every four-bit basis input. It also checks the gate ledger and padded output decoding. It uses no random sampling, floating-point arithmetic, order-finding oracle, or supplied factorization routine.

Its execution is not asserted. The mathematical proof is Lemma lem:row and Theorem thm:finite.

# Optional exact checker for Oai279-A. # This program is supplied, not reported as executed.

ell = 4 n = 128 q = ell + n*n + 3 u, v, f = q-3, q-2, q-1

# Rows: (input integer, zero-control positions, output targets). rows = [ (2, (0,2,3), (5,)), (3, (2,3), (4,5)), (4, (0,1,3), (5,133)), (5, (1,3), (4,6)), (6, (0,3), (5,132,133)), (7, (3,), (4,5,6)), (8, (0,1,2), (5,133,261)), (9, (1,2), (4,5,132,133)), (10, (0,2), (5,132,134)), (11, (2,), (4,5,7)), (12, (0,1), (5,133,260,261)), (13, (1,), (4,6,7)), (14, (0,), (5,132,133,134)), (15, (), (4,5,132,134)), ]

gates = [] compute = [ ("CCX", 0, 1, u), ("CCX", u, 2, v), ("CCX", v, 3, f), ]

for m, zeros, targets in rows: assert zeros == tuple( j for j in range(ell) if ((m >> j) & 1) == 0 ) gates.extend(("X", j) for j in zeros) gates.extend(compute) gates.extend(("CX", f, t) for t in targets) gates.extend(reversed(compute)) gates.extend(("X", j) for j in reversed(zeros))

assert len(gates) == 175 assert sum(g[0] == "X" for g in gates) == 50 assert sum(g[0] == "CX" for g in gates) == 41 assert sum(g[0] == "CCX" for g in gates) == 84

for gate in gates: wires = gate[1:] assert len(wires) == len(set(wires)) assert all(0 <= j < q for j in wires)

def apply_gate(state, gate): kind = gate[0] if kind == "X": return state ^ (1 << gate[1]) if kind == "CX": _, a, t = gate return state ^ ((((state >> a) & 1)) << t) if kind == "CCX": _, a, b, t = gate control = ((state >> a) & 1) & ((state >> b) & 1) return state ^ (control << t) raise ValueError("Unauthorized gate")

def run(value): state = value for gate in gates: state = apply_gate(state, gate) return state

def decode_output(state): mask = (1 << n)-1 return tuple( (state >> (ell + a*n)) & mask for a in range(n) )

def elementary_factor_list(value): assert value >= 2 result = [] divisor = 2 while value > 1: while value result.append(divisor) value //= divisor divisor += 1 return result

for value in range(16): final = run(value) assert (final & 15) == value assert ((final >> u) & 7) == 0

factors = elementary_factor_list(value) if value >= 2 else [] expected = tuple(factors + [0]*(n-len(factors))) assert decode_output(final) == expected

assert q == 16391 assert run(12) == sum(1 << j for j in (2,3,5,133,260,261))

def P(t): return (t+128)**2 + 512

assert P(4) == 17936 assert len(gates) <= P(4) assert q <= P(4)

The loop in elementary_factor_list is used only to independently check sixteen finite inputs. It is not claimed to be polynomial-time factoring in the bit length of arbitrary integers.

1. The symbol $n$ in the source probability formula is the padded quantity $\max \{128,\ell \}$, not always the literal bit length.

2. The probability $p_{\ast }$ is an intermediate preparation probability. The exact probability $1/4$ used in Lemma lem:amplification is a further interface.

3. En07-A's supplied thm:exact is a complete-complement recovery criterion. It is not a theorem that a circuit factors with probability one.

4. The supplied sharp quantitative prop:classical-recovery passage is explicitly in VIII-B, version 3. A similarly named nomination for Landmark I does not justify moving the passage between manuscripts.

5. Em03-G's supplied thm:lower is a positive finite-parameter lower bound. The growing-resource transmission statement is separate.

6. VIII-C's lem:completion is a finite permutation extension statement. Family 279's lem:completion is a probability-engineering statement. The labels do not identify their mathematical objects.

7. The Oai272-A and Oai283-A nominations in the dossier do not supply independently inspected full articles or factoring subroutines. No missing title, theorem body, or authorship is invented for them.

release. The main completed result is the explicit finite support and resource certificate in Theorem thm:finite. The general factoring endpoint remains an external claim record.

. The inspected Comparator endpoint contains sorry. No successful Lean run or completed formalization is asserted.

and execution. This is a single-file pdfLaTeX manuscript. No successful pdfLaTeX build, execution of the appendix checker, quantum-device run, independent referee review, or journal acceptance is asserted.

discipline. Cheung manuscripts are cited by supplied identifier and version. They are comparisons, not unacknowledged premises for the order trial or dyadic completion. The supplied dossier is not an exhaustive corpus scan.

boundaries. No Page curve, island, horizon, gravity-generated entanglement, exclusion of classical gravity, spacetime emergence, or hardware factoring claim is made. For the separate programme described in the supplied dossier,

These statements preserve the stated boundaries. They do not deny the existence of technical continuation manuscripts or promote an unconstructed object to a universal nonexistence theorem.

OAI279

OpenAI. Exact quantum factoring over a fixed finite gate set. OpenAI Math Release preprint, 25 September 2026. External Family 279-01 claim, not independently verified here. Repository directory: preprints/Exact-quantum-factoring-over-a-fixed-finite- gate-set-September-25-2026.

SourceIntro

OpenAI. Introduction. Source section build/sections/01-introduction.tex of OAI279. Relevant source label: thm:main. Cited for the exact gate-model and all-input claim.

SourceModel

OpenAI. Exact circuits and classical records. Source section build/sections/02-model.tex of OAI279. Relevant labels: lem:dyadic and lem:records. Includes the padding $n=\max \{128,\ell \}$.

SourceOrder

OpenAI. An order trial with prescribed success probability. Source section build/sections/03-order-transform.tex of OAI279. Relevant labels: prop:order-trial, lem:transform, and lem:bins. The order-trial construction is audited, not imported.

SourceDyadic

OpenAI. A dyadic majorant with an exact sum; three modes with a prescribed mass. Source section build/sections/04-dyadic-order.tex of OAI279. Relevant source label: lem:majorant. Completes the source's order-trial probability argument.

SourceProcess

OpenAI. Factoring with verifiable auxiliary data. Source section build/sections/05-factor-process.tex of OAI279. Relevant source label: prop:process. Transition caps, auxiliary data, and retrospective probabilities.

SourceExactness

OpenAI. From verified runs to certain output. Source section build/sections/06-exactness.tex of OAI279. Relevant labels: lem:completion, prop:known-probability, and lem:quarter. The deferred-event identification is an external verification obligation here.

SourcePrimality

OpenAI. Primality appendix. Source file build/sections/appendix-primality.tex of OAI279. Relevant source label: lem:primality. Not used to verify the finite table.

LeanScope279

OpenAI. Exact quantum factoring over a fixed finite gate set: Lean scope note. Repository file lean/docs/279.md, consulted 14 October 2026. https://github.com/openai/math/blob/main/lean/docs/279.md

LeanTarget279

OpenAI. ExactQuantumFactoring.lean. Repository file lean/ComparatorChallenges/ExactQuantumFactoring.lean, consulted 14 October 2026. The inspected endpoint exact_quantum_factoring has a sorry body. https://github.com/openai/math/blob/main/lean/ComparatorChallenges/ExactQuantumFactoring.lean

Scope274

OpenAI. {Parity is not in QAC${}^0$: Lean scope note}. Repository file lean/docs/274.md. Cited as catalogue context, not as an independently verified premise for the present circuit. https://github.com/openai/math/blob/main/lean/docs/274.md

Shor

P. W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing 26 (1997), no. 5, 1484–1509. doi:10.1137/S0097539795293172. arXiv:quant-ph/9508027.

AKS

M. Agrawal, N. Kayal, and N. Saxena. PRIMES is in P. Annals of Mathematics 160 (2004), no. 2, 781–793. doi:10.4007/annals.2004.160.781.

AKSErratum

M. Agrawal, N. Kayal, and N. Saxena. Errata: PRIMES is in P. Annals of Mathematics 189 (2019), no. 1, 317–318. Cited with the original article when invoking deterministic polynomial-time primality testing.

Bennett

C. H. Bennett. Logical reversibility of computation. IBM Journal of Research and Development 17 (1973), no. 6, 525–532. doi:10.1147/rd.176.0525.

Toffoli

T. Toffoli. Reversible computing. In Automata, Languages and Programming, Lecture Notes in Computer Science 85, Springer, 1980, 632–644. Also circulated as MIT/LCS/TM-151.

BHMT

G. Brassard, P. Høyer, M. Mosca, and A. Tapp. Quantum amplitude amplification and estimation. Contemporary Mathematics 305 (2002), 53–74. doi:10.1090/conm/305/05215. arXiv:quant-ph/0005055.

MoscaZalka

M. Mosca and C. Zalka. Exact quantum Fourier transforms and discrete logarithm algorithms. Preprint, 2003. arXiv:quant-ph/0301093. Cited with its gate-parameter and input assumptions retained.

Watrous

J. Watrous. The Theory of Quantum Information. Cambridge University Press, 2018. Finite-dimensional channels, measurements, and complete norms.

CheungI

N. Cheung. Landmark I, version 2. Supplied manuscript I.tex. Relevant supplied item: thm:main, the characterization under its declared structural requirements. Destructive-readout semantics are a comparison, not a factoring algorithm. Enter Calculus Companion.

CheungVIIIB

N. Cheung. Landmark VIII-B, version 3. Supplied manuscript VIII-B-v3.tex. Relevant label: prop:classical-recovery. Sharp record-only quantum-recovery obstruction, not a classical function-computation obstruction. Enter Calculus Companion.

CheungVIIIC

N. Cheung. Landmark VIII-C, version 3. Supplied manuscript VIII-C-v3.tex. Relevant label: lem:completion. Finite forward-domain permutation completion with explicit dictionary-dependent synthesis bounds. Enter Calculus Companion.

CheungEn01A

N. Cheung. En01-A, version 1. Supplied manuscript En01-A.tex. Relevant label: thm:bnf. Orthogonal branch records in a specified compiled circuit class. Enter Calculus Companion.

CheungEn02A

N. Cheung. En02-A, version 1. Supplied manuscript En02-A-v1.tex. Relevant label: thm:Dprime. One-shot environment dimension and its distinction from adaptive instantaneous memory. Enter Calculus Companion.

CheungEn02B

N. Cheung. En02-B, version 1. Supplied manuscript En02-B-v1.tex. Relevant label: thm:B1. Resource-certified programme soundness on complete interfaces. Enter Calculus Companion.

CheungEn07A

N. Cheung. En07-A, version 1. Supplied manuscript En07-A.tex. Relevant supplied labels: thm:exact and thm:release. Complete-complement recovery and separately stated readout-and-drop conventions. Enter Calculus Companion.

CheungHawk04B

N. Cheung. Hawk04-B, version 2. Supplied manuscript Hawk04-B.tex. Relevant supplied items: thm:exact, typed destructive readout, and classical-record recovery limitations. No gravitational conclusion is imported. Enter Calculus Companion.

CheungEn01B

N. Cheung. En01-B, version 2. Supplied manuscript En01-B-v2.tex. The dossier describes thm:bounded as a bounded-statistic finite-sample result in a declared model family. Not probability-one circuit correctness. Enter Calculus Companion.

CheungEn01C

N. Cheung. En01-C, version 1. Supplied manuscript En01-C.tex. The dossier describes thm:certificate as a clipped complete-record statistical certificate. Not an exact-support theorem for factoring. Enter Calculus Companion.

CheungEm03G

N. Cheung. Em03-G, version 1. Supplied manuscript Em03-G-v1.tex. Relevant supplied label: thm:lower. A positive recovery-error lower bound at finite source parameters; growing-resource transmission is a separate statement. Enter Calculus Companion.

CheungOai265A

N. Cheung. Oai265-A, supplied version 1. Relevant labels: def:determination and thm:separation. Static records, selected spectra, complete channels, and histories are distinct interfaces. Enter Calculus Companion.

CheungXIVJ

N. Cheung. Landmark XIV-J, version 1. Supplied manuscript XIV-J.tex. Relevant labels: thm:J2, thm:release, and cor:noadmission. The full characteristic map and quantum admission remain outside the supplied partial constructions. Enter Calculus Companion.

CheungXVB

N. Cheung. Landmark XV-B, version 2. Supplied manuscript XV-B.tex. Relevant labels: thm:lifting, thm:jetnull, and thm:release. Relative-lifting and extension interfaces do not supply the unconstructed full characteristic coefficient. Enter Calculus Companion.

Dossier

User-supplied Oai279-A plan and comparative manuscript dossier. Supplied retrieval identifier: 178f233f (retrieval-3). Includes version-specific Cheung passages and catalogue comparisons with Families 265, 272, 274, 276, and 283. Not an exhaustive source scan or proof verification. Companion site: https://enter.grok.me.