Coordinator targeted audit of the exact native full candidate, after a native source/resource audit timed out without a claim. This is a verification supplement, not a second discovery or an altered frozen theorem.

All constants below depend only on fixed integer tau>=max(1,T). Put b=tau+1/4, B=b^2/2, h=1/4. The proof's two-time bound G(x)>=h^2/pi^2 on[-6,6] implies G>=g0=1/160, using pi^2<10. Define
 M=b/g0,
 D1=b^2/(2g0)+b^4/g0^2,
 D2raw=b^3/(3g0)+(13/6)b^5/g0^2+2b^7/g0^3,
 D2=12(D2raw+2D1+4M).
Indeed |F|<=b, |F'|<=b^2/2, |F''|<=b^3/3; |G'|<=b^3 and |G''|<=7b^4/6. Twice differentiating conjugate(F)/G yields the displayed D2raw bound. The quintic cutoff used in the proof has |chi'|<=15/16<1, |chi''|<=15/4<4, support length12. Thus ||(chi R)''||_1<=D2.

For period16 the nonzero Fourier coefficients have |c_k|<=4D2/(pi^2 k^2). The full absolute sum is at most M+4D2/3, since |c0|<=M and sum_{k!=0}k^-2=pi^2/3. Choose a rational integer S>M+2D2+2. For any rho in(0,1], choose an integer D>=32D2/rho. Then the tail is at most8D2/(pi^2D)<=rho/4 (a deliberately loose rational bound). Compute real rational Fourier coefficients whose total error is at most rho/8. The initial polynomial has uniform error at most3rho/8, hence its value at0 differs from rational kappa_j=2t_j/(t_1^2+t_2^2) by at most3rho/8. Adjust its constant coefficient to kappa_j exactly. Final uniform error is at most3rho/4<rho, and absolute coefficient sum remains below S. Add cancelling identity terms to reach S exactly. This proves simultaneous approximation, constant normalization and exact identity preservation with rational data.

This computation is effective and polynomial in1/rho for fixed tau. For |k|<=D, derivative bounds for the coefficient integrand are polynomial in D with fixed-tau constants. A uniform quadrature mesh O_tau(rho/D^2) controls total coefficient error. Trigonometric/exponential and rational arithmetic need only polynomially many bits in log(D/rho). Real coefficients follow from f(-x)=conjugate f(x); paired interval evaluations can enforce real values before rational rounding. No spectrum of H0 is computed.

For the signed estimator, expand conjugate(y_I)y_P using y_I=k_j+e_I, y_P=-ir d_P/S+e_P, |e_I|<=k_j Bq^2 and ||e||<=E=Bq^2+rho bq/S, q=r eta. The absolute bias is at most
 S E/r + Bq^2 Mb eta + S Bq^2 E/r
 <=eta[(SBq+b rho)(1+Bq^2)+BM b q^2].
For q,rho<=1 this is bounded by C0 eta(q+rho) with rational
 C0=SB(1+B)+BM b+b(1+B).
Put k_min=min_j(kappa_j/S)>0 and C1=S/(2k_min).
Choose integer K>=max{1,128SB,128C0}, rational c<=min{1,1/(128b),1/(128C0)}, and a=1/(Km). With eta<=a/2, r=floor(a/eta), rho=c/m and zeta=eta/(16m), one has a/2<=q<=a and
 E/q <= [B/K+bc/S]/m <=1/(64mS),
 C0(q+rho)<=1/(64m).
Consequently each heavy residual label has unconditional probability at least
 (3q/(64mS))^2 >= c2/m^4, c2=(3/(128KS))^2.
The statistical estimator's range is C1/r and r zeta>=1/(32Km^2). These are exactly the polynomial discovery and estimation conditions of the original frozen proof, with explicit simultaneous constants.

For finite compilation choose rational c3<=min{1,c2/2,1/(256KC1)} and per-experiment trace distance nu=c3/m^4. A label probability changes by at most nu and retains at least c2/(2m^4). Signed-score means change by at most2nu; the scaled coefficient change is at most2C1nu/r. Relative to zeta it is at most64KC1c3/m^2<=1/4. Thus compilation uses at most the final zeta/4 of the original error budget. The compensator precision O(nu/r), repeated r times, and remaining circuit precision O(nu) are attainable by known-Pauli product formulas and finite gate synthesis with polynomial cost in n,m,r. This polynomial may have degree greater than one in1/epsilon; the ORIGINAL permits that for known operations. Only unknown evolution time must scale as1/epsilon.

Bad histories: the algorithm aborts whenever any retained coefficient exceeds2 in magnitude. Thus every continued H0 has at most m terms and Pauli l1 norm<=2m. Good histories additionally have ||H0||<=2, as required for the spectral accuracy proof. On bad histories that spectral promise can fail, but the same finite LCU circuit and predetermined D,S still exist and have polynomial cost: sums of known-Pauli product formulas use the l1 bound, not a computed spectrum. The number of stages, samples, retained labels and bit precision is predetermined polynomially. Measurement scores are rational because S,kappa_j,r are rational/integer, so coefficient updates can be carried out exactly as rational sums with bit length polynomial in the number of rounds and sample-count bits; optional rounding can instead be charged a separate stated accuracy. The norm test ||H0||<=2 is never computed and is not needed to bound runtime. Failure on a bad history is already included in the conditional union bound.

Initialization: all derivatives of normalized Pauli traces have modulus<=1. L=ceil(max(4e^2(tau+1)^2,log2(4/z))) can be replaced by any explicitly computable integer upper bound. Its interpolation weight sum is poly_tau(1/z). For z=1/(8Km^2), all discovery samples and candidate lists are polynomial in m for fixed tau; at most one label is added per shot, and there is no4^n enumeration. The two-copy estimator controls only a known Pauli times SWAP. All oracle durations are tau+j/L or tau,tau+z/2 in initialization and tau,tau+1/4 in refinement. Their gaps may be small, but no individual oracle interval is belowT. This distinction is essential.

Source comparison (retrieved full primary sources and exact excerpts in hamiltonian-source-comparison):
- Shin--Lee--Oh2604.27838v1 Theorem1 uses4^m and is efficient for logarithmic sparsity; Theorem2 hasm^(K+2) at T=Theta(m^-1/K), becoming quasipolynomial at constantT. Its post-theorem discussion explicitly leaves arbitrary polynomial sparsity and fixedT open. This is the nearest inherited residual-learning architecture; attribution must be retained.
- Hu et al2502.11900v2 Theorem1 gives ansatz-free Heisenberg scaling, but its reshaping circuit Eq9 interleaves short unknown evolutions. Eq10's O(tau^2) and the O(M^2 t^2/r_2) simulation bound are not a fixed-minimum-time theorem. The candidate inherits sparse bootstrap ideas rather than claiming them as new.
-2606.05690v1 establishes generic local identification up to scale/sign under isolation hypotheses. It does not imply a worst-case absolute-coefficient theorem for arbitrary sparse, potentially nonlocal Pauli support.
-2606.19486v1's in-situ control-free method has standard-quantum-limit1/epsilon^2 time, which misses the original required scaling.
- Shin--Tong2609.26596v1 formal Theorem7 Eq35 has tau=Theta(1/[Lambda(1+log(Lambda/epsilon))]), explicitly shrinking with accuracy. Theorem9's sparse learning also assumes fixed locality k; Theorem12 removes locality for a specified coefficient but imports Theorem7 and presupposes the label. None of these displayed interfaces gives the original arbitrary-support fixedT guarantee. This September22 paper was found during verification, after the candidate was generated, and must be cited in any later manuscript.

No covering theorem was found among these sources or targeted title/phrase searches. This is a documented comparison, not exhaustive historical novelty clearance. Algebraic/numerical controls, native PASS and frozen PASS come from the same model family and coordinator; no external expert confirmation is claimed. The interrupted native audit supplies no completed verification judgment.
