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

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.