Oai227-A A Finite Stationary–Quench Certificate for Classical SK Heat-Bath Autocorrelations A seven-stage audit with a fully proved two-spin instance

We construct the finite certificate requested by the Family 227 audit plan without assuming its functional scaling-limit theorem. For critical zero-field Sherrington–Kirkpatrick heat-bath dynamics with rate-one clocks per spin, we freeze

where physical waiting time and lag are $2^{2/3}s$ and $2^{2/3}t$, and mean autocorrelations are multiplied by $2^{1/3}$. An exact four-state calculation proves, for every real coupling, that the rescaled stationary autocorrelation exceeds the rescaled uniform-quench autocorrelation by less than $1/65536$, uniformly on this compact. Consequently the same certificate holds with probability one under both Gaussian and Rademacher disorder, without truncating Gaussian couplings.

We distinguish this within-realization comparison from finite-size universality: at two spins the Rademacher autocorrelation functions are deterministic, whereas their Gaussian counterparts are nondegenerate. We also provide finite-state normalization checks, compact interpolation bounds, sampling and clock-history allowances, and a rate-perturbation ledger. The external stationary-edge, warming, entrance-selection, and functional replacement assertions are audited but not imported. Several ambiguities in the proposed plan are corrected, including the difference between a common limiting law and identical stationary and quench functions, and the existence of an implicit semigroup representation of the proposed limit. No thermodynamic-limit theorem, quantum SK theorem, QAOA identification, Page curve, or gravitational conclusion is proved.

The local submission claim is Theorem thm:finite-certificate: one specified finite-size, positive-time, uniform stationary–quench comparison.

The choice $n=2$ is explicit. It is the smallest interacting SK system, not a large-system approximation and not evidence for the claimed critical exponent. The finite-size powers $n^{1/3}$ and $n^{2/3}$ are retained exactly, but their use at one size proves no scaling law.

The requested identifier Oai227-A does not assign authorship to N. Cheung, assert registration in another series, or claim endorsement of this development.

common law is not equality of the two limiting functions. The external quench manuscript asserts convergence of a pair $(A_{n,J},B_{n,J})$ to a pair $(A_g,B_g)$, with one common pair law for the two disorders. It does not assert $B_g(s,t)=A_g(t)$ at every finite waiting time. Its relaxation assertion concerns $s\to \infty$ OAI227Quench (Section 1, thm:main).

{Convergence in $C_{\mathrm{loc}}$ is convergence in law.} Uniform-on-compacts is the topology of the random-function space in the external claim. Without a specified coupling, it is not a pathwise supremum comparison between a Gaussian sample and a Rademacher sample.

proposed limit has an implicit representation. The inspected source writes $B_g$ as a series involving an edge measure, its semigroup, and an entrance density. Thus “the theorem does not write $B_g$” is too strong. The correct distinction is between such a representation and an evaluated formula, a convergence rate, or a finite certificate OAI227Background,OAI227Entrance.

finite certificate does not verify the infinite theorem. Producing the requested finite comparison neither proves nor automatically opens verification of the external process limit. A necessary milestone must not be read as a sufficient verification criterion.

We certify the same statement separately under each disorder: for the same realization $J$, stationary and quench autocorrelations are close on the stated compact. Our proof is stronger in this particular finite model: it holds for every $J\in \mathbb{R}$.

We do not identify Gaussian and Rademacher finite-size autocorrelation laws. Proposition prop:finite-laws shows that those laws are different. A cross-disorder finite-law approximation would require its own chosen metric, tolerance, and theorem.

The inspected external quench manuscript is attributed to OpenAI and dated 5 October 2026. Its stationary companion has the same date OAI227Quench,OAI227Stationary.

The scope note lean/docs/227.md describes selected high-temperature, critical-mixing, and barrier statements; it does not describe a formalization of the functional autocorrelation limit Lean227. Moreover, the inspected Comparator targets SKRatio.lean and CriticalSKMixing.lean contain theorem bodies ending in sorry LeanSKRatio,LeanCriticalMixing. They are not presented here as completed executed proofs. No conclusion is drawn about uninspected artifacts.

The supplied Cheung passages are documentary comparisons. Their model-specific theorems are not assumptions of the finite SK calculation.

For $n\ge 2$, put

For a symmetric array $J$, with $J_{ii}=0$, define the classical energy

This is a real-valued function on a finite configuration space. It is not a quantum Hamiltonian.

At inverse temperature $\beta$, the Gibbs law is

Throughout the local certificate,

The two nominated disorder laws are

independently on the edges $i<j$. The normalized interaction matrix has off-diagonal entries $W_{ij}=J_{ij}/\sqrt{n}$.

These conventions are the zero-field SK normalization used in the external claim. The original SK model is classical SK1975,OAI227Quench.

Write ${\sigma }^{i,a}$ for the configuration obtained by setting coordinate $i$ to $a$. At criticality the local field is

The site heat-bath operator is

Every site has an independent rate-one Poisson clock. At a ring its spin is sampled from (eq:site), including the possibility that it keeps its value.

The generator and semigroup are

Thus one physical time unit contains $n$ update attempts on average.

Let $U_n$ denote the uniform law on ${\Omega }_n$, independent of $J$. This is the quench initialization. It is not replaced by a Gibbs sample.

For every finite $J$, (eq:generator) defines a nonexplosive irreducible continuous-time Markov chain. Its invariant law is $\pi$, and it is reversible.

If $K=n^{-1}{\sum }_i{K}_i$, then

In particular, $K$ counts uniformly chosen single-site attempts, whereas ${P_u}^J$ uses rate one at each site.

Proof. Each $K_i$ is a stochastic matrix. The exponential identity follows from $L_J=n(K-I)$. Its right-hand side is a Poisson mixture of stochastic matrices, so it defines the chain with rate-$n$ attempts and uniformly chosen sites. The number of attempts on a bounded interval is finite almost surely.

Each conditional spin probability is strictly positive when $J$ is finite. Single-coordinate changes connect the cube, which proves irreducibility. The operator $K_i$ is conditional expectation under $\pi$, given all coordinates except $i$. Therefore it is self-adjoint on $L^2(\pi )$, preserves $\pi$, and satisfies detailed balance. Summing gives reversibility of $L_J$ and ${P_u}^J$.

This is the usual finite-state heat-bath construction; standard Markov-chain conventions are discussed in LevinPeres (Chapters 3 and 20).

Let $f_i(\sigma )={\sigma }_i$. For physical waiting time $w\ge 0$ and lag $\ell \ge 0$, define

These are means of individual-spin autocorrelations, not autocorrelations of the total magnetization.

Put

and define

Initial spins, clocks, and heat-bath resampling are averaged in these functions. Disorder is not averaged. Consequently $A_{n,J}$ and $B_{n,J}$ are random functions only when $J$ is sampled.

The external claim is that

in

with the same limiting pair law for the two disorders. The stationary limiting law is not a point mass.

The quench starts from $U_n$. Its selected entrance family has positive-time probability densities ${h_s}^g$, satisfies a semigroup relation, and relaxes to equilibrium. In particular, the stated conclusion includes

in probability over $g$ as $s\to \infty$, for $0<a<b<\infty$ OAI227Quench,OAI227Stationary.

This record is not a premise of any local theorem below.

records. The family also records a high-temperature gap and cutoff, critical slowing, low-temperature barriers, and a critical mixing exponent. Their statements concern different quantities or temperature regimes Lean227,Catalogue. They are not premises of our finite certificate. This does not assert that the external quench manuscript has no dependencies on its companions: its own source explicitly cites stationary, spectral, and mixing inputs OAI227Background,OAI227Edge,OAI227Warming.

For real functions on the cube,

Also,

The invariant law and both initialized processes are invariant under global spin reversal; in particular their one-spin means are zero.

Proof. Each $K_i$ is an orthogonal conditional-expectation projection on $L^2(\pi )$. Hence

Only an update at site $i$ changes $f_i$, and its conditional new mean is $\tanh h_i$, proving (eq:spin-action). Both the energy and the update rule respect global reversal. So do $\pi$ and $U_n$.

Let $({\lambda }_{\alpha },{\psi }_{\alpha })$ be an orthonormal eigensystem of $-L_J$ on $L^2(\pi )$, with ${\lambda }_0=0$ and ${\psi }_0=1$. Then

The weights are nonnegative. The eigenvalues here are those of the heat-bath generator, not those of the $n$-by-$n$ interaction matrix.

Proof. Expand each $f_i$ in the reversible eigenbasis. Its constant coefficient vanishes by Lemma lem:dirichlet. Apply ${P_{T_{n}t}}^J$, take its inner product with $f_i$, and sum.

For any orthonormal basis $u_1,\dots ,u_n$ of ${\mathbb{R}}^n$, set

Then

If

then

Moreover $w_{s+t}={P_{t{T}_n}}^J{w}_s$.

Proof. The first identity is orthogonality. Apply it to the two configurations in a two-time pair and condition on the first. Since $\pi$ has full support, the density exists. Reversibility identifies the evolution of a density relative to $\pi$ with ${P_u}^J$, proving the last assertion.

This finite identity does not identify any limiting edge measure or establish tightness.

For Gaussian disorder the external route completes $W$ by an independent Gaussian diagonal. The added diagonal changes the spin energy by a configuration-independent constant, because ${{\sigma }_i}^2=1$. This completion can supply Gaussian orthogonal eigenframe structure without changing the finite heat-bath dynamics OAI227Background.

The audit must nevertheless keep three objects separate:

1. the spectral edge of $W$;

2. the projected spin coordinates in (eq:finite-entrance);

3. the spectrum and semigroup of the nonlinear heat-bath generator in (eq:dynamical-trace).

Equation (eq:spin-action) shows why diagonalizing $W$ does not generally diagonalize $L_J$.

The stationary edge law, its conditioned measure, convergence of finite-coordinate integrals, and the limiting energy form are substantive external inputs. Even if all of them are supplied, the extra factor $w_s$ in the quench trace still requires control. Stationary convergence is not the quench theorem.

The external Gaussian argument uses scales with $k_p=n{p}^3$, capped resolvents, and a saddle equation. A representative variance assertion is

on stated disorder events and scale ranges OAI227Edge (prop:edge-estimates).

A complete verification would have to check:

1. the saddle's existence, uniqueness, and positive denominators;

2. uniformity over every admitted field, function, and scale;

3. how a threshold depending on a requested disorder confidence is chosen;

4. the integrability of accumulated relative errors across scales;

5. the transfer between spherical and cube quantities with their stated reference measures.

A threshold sent to infinity after a limsup in $n$ is not automatically a fixed-threshold probability tending to one. Nor is a static resolvent estimate a heat-bath mixing theorem. These Gaussian estimates are not reproved or assumed here.

The external warming statement concerns positive-time Gibbs-relative densities, entropy, and heat kernels at times $s{T}_n$. Its constants are controlled on disorder events chosen to meet a prescribed confidence, and its stronger kernel bound begins beyond a deterministic rescaled time tending to zero OAI227Warming (thm:warming).

The audit must distinguish:

A bound by a finite function of $s$ does not itself prove that the distance to equilibrium tends to zero.

The time unit $T_n=n^{2/3}$ is dynamical bookkeeping. No positions, spatial propagation radius, or metric are specified by it.

The source's entrance-selection condition is stronger than merely requiring a zero-coordinate product-topology boundary. It includes local positive-time density bounds, the edge semigroup relation, and a sequential high-mode escape condition inherited from the uniform initial states OAI227Entrance (thm:entrance-selection).

The verification questions are:

1. Do all extracted Gaussian subsequences satisfy the stated escape condition?

2. Does uniqueness hold in the exact density class used?

3. Is the selected family measurable in the edge environment?

4. Are the trace tails controlled when the density and semigroup limits are inserted into the infinite sum?

A possible semigroup entrance is not enough; it must be the entrance selected by the finite uniform starts.

No conclusion at $\beta \ne 1$ is substituted for this selection.

Gaussian and Rademacher couplings match their first three moments. The fourth moments differ. In a fourth-order replacement calculation, normalization contributes $n^{-2}$ while the number of edges is of order $n^2$. These powers alone give only order one, not an error tending to zero.

The source therefore uses clock-history cutoffs, projected scores, derivative estimates including cutoff derivatives, and a functional tightness argument OAI227History,OAI227Scores,OAI227Replacement. The general replacement methodology has a separate literature Chatterjee.

A full audit must verify both removal of the cutoffs and control between time-grid points. Comparison of finitely many evaluations alone does not prove convergence in $C_{\mathrm{loc}}$.

Universality in the frozen statement concerns the two named disorders. It does not assert universality for every mean-zero disorder distribution.

For fixed $n,J$, define

Then ${\Vert G_{\ell }\Vert }_{\infty }\le 1$, and

Proof. The semigroup sends functions bounded by one to functions bounded by one. The two autocorrelations are $v_n$ times the expectation of $G_{T_{n}t}$ under the two displayed laws. The total-variation expectation bound gives the result.

At a fixed total-variation threshold such as $1/4$, the right-hand side of (eq:tv-comparison) grows as $n^{1/3}$. Thus a mixing-time bound at that threshold does not supply a rescaled correlation process limit. It also does not identify a nondegenerate limiting law.

For every $n,J$, the finite autocorrelation functions are smooth. Uniformly over their nonnegative time arguments,

For ${\Delta }_{n,J}(s,t)=A_{n,J}(t)-B_{n,J}(s,t)$,

Proof. Finite matrix exponentials are smooth. By (eq:spin-action), ${\Vert L_J{f}_i\Vert }_{\infty }\le 2$. Since the semigroup is a supremum-norm contraction and commutes with its generator, differentiating a lag contributes at most

For the waiting derivative use

Every $G_{\ell }$ is bounded by one, and ${\Vert L_J{G}_{\ell }\Vert }_{\infty }\le 2n$. Thus the derivative is at most $v_n{T}_{n}2n=2n^2$. Subtracting the two lag derivatives proves the final bounds.

This is a finite-$n$ modulus. It grows with $n$, so it does not by itself prove asymptotic equicontinuity.

Fix $n,J$, a finite time grid, and the intended initialization. At each grid point use independent repeated trajectories. For stationary data the initial law is $\pi$; for quench data it is $U_n$. Every attempted repetition is retained. Any implementation failure receives its predeclared score and flag. No successful-run conditioning is substituted.

For a two-time trajectory pair, its scaled score is

Suppose a compact rectangle has a finite grid $\Gamma$ of $M$ points such that each point of the rectangle has a grid point within $h$ in each coordinate. At each grid point estimate the stationary and quench quantities with $N$ repetitions as in Specification spec:sampling.

With probability at least

all the two types of mean estimates have errors at most $r$. On this event,

A certified score-expectation bias $b$ for each of the two protocols adds $2b$. A calibration-failure probability $\eta$ adds $\eta$ to the total failure probability.

Proof. A score has range length $2v_n$. Hoeffding's inequality gives

Apply a union bound to $2M$ estimates. Their difference has error at most $2r$. Lemma lem:modulus extends the bound from the grid to the rectangle. Add the deterministic biases and calibration failure by the triangle inequality and a union bound Hoeffding.

The independence is across repetitions, not across the spins within one trajectory. Correlated spin coordinates have not been counted as independent samples.

This is the legitimate comparison with Cheung's bounded, complete-record statistical certificates CheungEn01B,CheungEn01C. A confidence interval alone does not give functional convergence. Equation (eq:grid-certificate) obtains finite-compact coverage only because a deterministic modulus has also been proved.

For an observation up to physical time $u$, the attempted update count is Poisson with mean $nu$. For the quench pair $(s,t)$, that mean is

Clock attempts include updates that leave the spin unchanged. Counting flips instead would change the history law.

In the final certificate, $n=2$, $s+t\le 7$, and

Hence the maximum quench history has mean less than

For the frozen compact used in Theorem thm:finite-certificate, the probability that a trajectory needs at least $144$ update attempts is less than $2^{-144}$, uniformly over every coupling.

If such a history is flagged and assigned score zero, rather than deleted, the absolute bias of either scaled mean score is at most $2^{1/3}{2}^{-144}$.

Proof. If $N$ is Poisson with mean $\mu$, then

Also

so $m!\ge (m/e{)}^m$. For $m=144$, $\mu <112/5$, and $e<3$,

This proves the tail bound. On the flagged event, changing a score to zero changes it by at most $2^{1/3}$. Take expectations.

The proof is a clock ledger, not a sample execution. Exact draws from a real Gaussian law are mathematical inputs; no finite-bit exact Gaussian sampler or machine running time is claimed.

Let $Q,\hat{Q}$ be Markov generators on the same finite state space, and suppose

If initial laws have total-variation distance at most $\eta$, their one-time laws at time $u$ differ by at most $\eta +u\delta$.

Their joint laws at times $w,w+\ell$ differ by at most

A score in $[-v_n,v_n]$ consequently has expectation difference at most

or the trivial bound $2v_n$, whichever is smaller.

Proof. Duhamel's formula expresses the semigroup difference as the integral of

Stochastic multiplication contracts the total variation of signed measures, while multiplication by $Q-\hat{Q}$ costs at most $\delta$ for a probability input. Integration and the initial-law comparison give the first bound.

For a two-time joint law, first compare the law at time $w$, then the conditional transition over the remaining lag. The two allowances add. The bounded-score expectation inequality gives the final assertion.

A nominated quantum-channel distance budget cannot specify the classical generator by itself. Proposition prop:perturbation states the actual classical comparison interface needed here.

Sample $J$ once, and conditionally on $J$ sample $N$ independent scores $Y_1,\dots ,Y_N$ with conditional mean $m(J)$. Then

Proof. Apply conditional independence and the law of total variance.

Increasing the number of trajectories removes the first contribution, not sample-to-sample disorder variation. Resampling disorder on each repetition instead estimates an annealed quantity and changes the experiment.

The Cheung citations support these scoped comparisons, not premise transfers CheungEm04A,CheungHawk02D,CheungHawk02E, CheungEn07C,CheungI,CheungVIIIB,CheungEm03G,CheungOai265A. The Oai272-A and Oai283-A nominations remain dossier-level comparisons Dossier.

The inspected source describes a conditioned edge measure ${\Pi }_g$, a Markov semigroup ${S_t}^g$, and entrance densities ${h_s}^g$. In that notation it represents the proposed quench limit by

and the stationary function by the corresponding expression with density one OAI227Background,OAI227Entrance.

This is a substantive representation, not an absent formula. However, evaluating it requires the edge environment, the conditioned measure, the semigroup, the selected entrance, and control of its infinite tail. A representation of this kind is not:

• a closed elementary formula for the random function;

• a computable error bound at a chosen finite $n$;

• a convergence rate in the random-function topology;

• a finite comparison of stationary and quench curves.

The local theorem in Section sec:certificate supplies the last item for one small finite system. It supplies none of the missing infinite-system verification.

Fix any finite set of system sizes. Two sequences of continuous functions can agree at every one of those sizes, while one converges and the other alternates forever between the constant functions zero and one at later sizes. Thus even an exact finite certificate cannot logically verify a claimed limiting law without additional uniform estimates.

The family's high-temperature cutoff and low-temperature barrier claims are retained as external records, not proved by the present calculation Lean227,Catalogue. Neither regime is substituted for $\beta =1$.

Changing from rate-one-per-site clocks to a single total rate-one clock divides the generator by $n$. The same physical evolution would then require $n$ times as many time units. At the critical scaling this changes $n^{2/3}$ physical units into $n^{5/3}$ single-attempt units.

Holding at an attempted update is part of the heat-bath model. It is not silently removed.

A diagonal quantum cost operator built from the classical energy is

It commutes with each $Z_i$. Consequently unitary evolution under this operator leaves every $Z_i$ unchanged.

By contrast,

The strict inequality holds for every finite coupling array. Thus even this elementary diagonal quantum evolution is not the heat-bath dynamics.

QAOA adds prescribed unitary mixing layers and optimizes an energy expectation as a function of its parameters and depth. It does not install independent heat-bath clocks FarhiEtAl. The dossier's Family 281 order-of-limits energy statement is therefore only a catalogue comparison Catalogue,Dossier.

Likewise, a Haldane quantum spectral gap, Anderson localization, and an area-law theorem concern different operators and questions. None identifies the present Markov generator.

A classical probability law $p(\sigma )$ can be embedded diagonally as

This is a convex combination of product states and is therefore separable across every spin partition. Classical spin correlations do not by themselves certify quantum entanglement.

A record-only quantum channel is measure-and-prepare and has the corresponding entanglement-breaking limitation CheungVIIIB,CheungHawk04B. That fact does not prevent a classical spin process from having long temporal correlations. It is a statement about unknown-state quantum recovery, not about the value of (eq:physical-correlation).

Our probability model uses classical trajectory observations. It does not insert a destructive quantum measurement into the heat-bath generator. If an implementation uses Enter for quantum-encoded records, its stated consumption rules remain unchanged; no surviving measured quantum wire is inferred CheungI.

The clock normalization specifies attempted updates per unit time. The SK coupling graph is all-to-all and has no independently declared spatial embedding here.

Even the invariant law does not determine time normalization: $L_J$ and $c{L}_J$, $c>0$, have the same Gibbs law but different autocorrelation functions at the same numerical time. A static record therefore cannot supply a temporal process without further data. This is the appropriate methodological comparison with Oai265-A CheungOai265A.

Scheduled ancestry, operational influence, and a separately supplied geometric causal relation also remain different objects CheungXXIIA. No geometric propagation law is derived from $T_n=n^{2/3}$.

The present model specifies a finite configuration space, a classical Gibbs law, and stochastic update rates. It does not specify a spacetime metric, horizon, radiation algebra, evaporation dynamics, gravitational mediator, or island extremization problem.

Accordingly, neither a stationary autocorrelation nor a uniform-quench two-time correlation is a Page curve, an island, a horizon, or Hawking radiation. No gravity-generated entanglement or exclusion of classical gravity follows.

The external thermal and residual-recovery comparisons explicitly require their own model identifications CheungEn07C,CheungHawk02D,CheungHawk02E. They supply no such identification for classical SK.

We choose

The single coupling $J=J_{12}$ is arbitrary in $\mathbb{R}$. Write

In particular, $-1<a<1$.

In the ordered state space

the heat-bath generator and invariant row vector are

For $z(\sigma )={\sigma }_1{\sigma }_2$,

Proof. A flip at either site has rate

It is $b$ in aligned states and $c$ in anti-aligned states, which gives $Q_a$. The Gibbs weights are $e^{\kappa }$ in aligned states and $e^{-\kappa }$ otherwise. Dividing by $4\cosh \kappa$ gives ${\pi }_a$.

The spin actions follow from (eq:spin-action) because $\tanh (\kappa {\sigma }_j)=a{\sigma }_j$. At an update of site one, the conditional mean of the new product is $a$, and the same holds at site two. Therefore $Lz=2(a-z)$.

For physical waiting time $w\ge 0$ and lag $\ell \ge 0$,

Consequently,

Proof. The first two equations in (eq:two-actions) form a closed two-dimensional linear system. Thus

with the indices interchanged for $P_{\ell }{f}_2$.

Under the uniform start, $m(w)=\mathbb{E}[z(\sigma (w))]$ solves

Hence $m(w)=a(1-e^{-2w})$. Under the invariant law, ${\pi }_a[z]=a$.

Condition on the configuration at waiting time $w$, multiply the displayed semigroup formula by the corresponding initial spin, and average. Both coordinates give the same answer. This proves (eq:two-stat) and (eq:two-quench). Insert $w=Ts$, $\ell =Tt$, multiply by $v$, and subtract.

For the data in (eq:certificate-data), every real coupling $J$ satisfies

In particular,

The two functions are explicitly given by (eq:two-stat)–(eq:two-quench) in the frozen units. Under each of the Gaussian and Rademacher coupling laws, the displayed uniform comparison holds with probability one. No exceptional-disorder event, asymptotic theorem, numerical optimization, or empirical sample is used.

For every $J\ne 0$ and positive $s,t$, the difference is strictly positive. Thus the theorem certifies a tolerance, not exact finite-waiting-time stationarity.

Proof. Since $a\sinh (a\ell )\ge 0$, the difference is nonnegative. For $\ell \ge 0$,

Equation (eq:exact-difference) therefore gives, on $s\ge 4$,

All remaining comparisons have finite elementary certificates. Cubing positive quantities gives

because $T^3=4>27/8$ and $v^3=2<64/27$. The positive exponential series gives

Consequently,

The same strict upper bound applies to the supremum because it is a single bound independent of $J,s,t$.

The disorder conclusions follow from the statement for every real $J$. If $J\ne 0$, then $a\ne 0$, and $a\sinh (aTt)>0$ for $t>0$, proving strict positivity.

This manifest, the four-state generator, and the proof above are the finite certificate. No unexecuted numerical assertion is needed to establish its inequalities.

Extend the stationary function to the compact by

For either disorder law, sample the same $J$ for ${\tilde{A}}_{2,J}$ and $B_{2,J}$. This is an explicit coupling of their laws on $C(\mathcal{K})$, with

Thus the within-disorder function laws admit a coupling with this uniform error.

This restates the finite theorem. It is not a coupling between Gaussian and Rademacher environments.

At $n=2$, both autocorrelation functions are deterministic under Rademacher disorder. Under Gaussian disorder, the stationary function has a non-point law. In fact, for every fixed positive lag $t$, the Gaussian and Rademacher laws of $A_{2,J}(t)$ have total-variation distance one.

Proof. The functions in (eq:two-stat)–(eq:two-quench) are even in $a$, hence even in $J$. Rademacher disorder has $|J|=1$ almost surely, so its function pair is deterministic.

For fixed physical lag $\ell >0$, put

For $z>0$,

Thus $F_{\ell }$ is strictly increasing on $[0,1)$. The map $|J|\mapsto |\tanh (J/\sqrt{2})|$ is also strictly increasing. A Gaussian $|J|$ has a continuous distribution. Its autocorrelation value is therefore non-atomic.

The Rademacher value is the value corresponding to $|J|=1$. The singleton containing that value has Rademacher probability one and Gaussian probability zero. This proves the total-variation assertion.

This does not contradict a common large-$n$ weak limit. It shows why the finite certificate must not be mislabeled as equality of the two disorder laws.

For the two-spin chain, the eigenvalues of $-L$ are

Its spectral gap is $1-|a|$, which can be arbitrarily small as $|J|\to \infty$. Nevertheless Theorem thm:finite-certificate is uniform in $J$.

Proof. The four independent eigenfunctions can be taken as

Their eigenvalues follow from (eq:two-actions). Since $a\to \pm 1$ as $J\to \pm \infty$, the gap tends to zero.

The uniform-start product expectation relaxes at rate two, as used in Lemma lem:two-functions. The finite certificate depends on that initialized observable, not on a disorder-uniform lower bound for the full gap.

This is a concrete demonstration that a stationary–quench observable comparison and worst-start mixing are different claims.

For a stationary sample, draw an independent fair sign $S$ and a product sign $Z$ with

Set

This gives ${\pi }_a$ exactly. A quench sample instead uses two independent fair signs.

Thereafter, at a site-one ring, sample the new spin with mean $a{\sigma }_2$; at a site-two ring, sample with mean $a{\sigma }_1$. This writes the finite stochastic mechanism without appealing to Em04-A, Hawk02-E, or En07-C for the couplings or clocks.

These are ideal mathematical sampling instructions. Finite-precision implementations require their own rate and initialization allowances, as in Proposition prop:perturbation.

The local result is

The following remain outside this certificate:

1. verification of the external Family 227-01 process limit;

2. construction or independent verification of its limiting edge diffusion and selected entrance;

3. an asymptotic convergence rate or large-$n$ error certificate;

4. a Lean formalization of the functional autocorrelation theorem;

5. a quantum SK theorem or identification with QAOA;

6. a closed evaluated formula for the infinite random process;

7. a Page curve, island, horizon, Hawking-radiation statement, gravity-generated entanglement, or classical-gravity exclusion.

Completion of the finite theorem does not discharge any of these separately quantified problems. No further next theorem is opened by this manuscript.

The certificate's numerical inequality uses no approximation to $\tanh (J/\sqrt{2})$. Its only size-dependent algebraic comparisons are

The exponential comparison uses

Finally,

The proof is therefore a finite analytic certificate with explicit rational comparisons. No floating-point agreement, numerical root finder, or simulation is used as a substitute for an inequality.

The supplied dossier also contains detailed XIV–XV–XVI material about reconstructed distributions and a missing joint characteristic composition. Those objects have no identification with ${\Omega }_n$, $Q_a$, or the finite correlation scores.

The supplied source relationship remains:

• XIV-I constructs its named internal amplitude at I2 but does not construct the complete joint map at I3;

• XIV-J gives reconstruction descent and a supported-sector off-characteristic reference, while the full map remains unresolved at J2;

• its subsequent section, transverse, contact, output, and admission requirements are not discharged by a finite SK calculation;

• the supplied XV-B revision develops abstract lifting and extension interfaces without constructing the inherited full graph-specific map.

These are documentary boundaries, not theorem premises CheungXIVI,CheungXIVJ,CheungXVB.

In particular, this manuscript neither constructs those missing maps nor proves that no possible map exists.

release. The main local theorem is the explicit two-spin uniform stationary–quench certificate. Its supporting finite-state, sampling, perturbation, and separation results are proved on their stated interfaces.

status. The universal non-point functional limit remains an external claim. This manuscript does not assert that it is false, and does not assert that it has been independently verified.

and computation. No successful Lean execution, removal of a Comparator placeholder, simulation run, finite-precision implementation, independent referee verification, or successful pdflatex execution is asserted. The displayed analytic proof does not depend on such execution.

use. The supplied Cheung manuscripts are cited by available identifier, version, section, and label. Incomplete excerpts do not license claims about the full corpus or uninspected proof dependencies. No source registration is asserted.

scope. The model is classical statistical mechanics. Its stochastic generator is not identified with a quantum Hamiltonian, Lindblad generator, QAOA circuit, spacetime metric, or gravitational dynamics.

programme boundaries. In the separate programme described in the dossier,

This does not deny the existence of technical continuation manuscripts or replace their version-specific conclusions by a universal nonexistence assertion.

SK1975

D. Sherrington and S. Kirkpatrick. Solvable model of a spin-glass. Physical Review Letters 35 (1975), 1792–1796. doi:10.1103/PhysRevLett.35.1792.

LevinPeres

D. A. Levin and Y. Peres, with contributions by E. L. Wilmer. Markov Chains and Mixing Times. Second edition, American Mathematical Society, 2017. Finite heat-bath chains, reversibility, mixing conventions, and continuous time. https://pages.uoregon.edu/dlevin/MARKOV/mcmt2e.pdf

Hoeffding

W. Hoeffding. Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association 58 (1963), 13–30. doi:10.1080/01621459.1963.10500830.

Chatterjee

S. Chatterjee. A generalization of the Lindeberg principle. Annals of Probability 34 (2006), 2061–2076. doi:10.1214/009117906000000575. https://arxiv.org/abs/math/0508519

FarhiEtAl

E. Farhi, J. Goldstone, S. Gutmann, and L. Zhou. The quantum approximate optimization algorithm and the Sherrington–Kirkpatrick model at infinite size. Quantum 6 (2022), 759. doi:10.22331/q-2022-07-07-759. Cited for the quantum-circuit and energy-expectation interface, not for identification with heat-bath dynamics. https://quantum-journal.org/papers/q-2022-07-07-759/

OAI227Quench

OpenAI. Universality of critical quench autocorrelations in the Sherrington–Kirkpatrick model. External Family 227-01 manuscript, dated 5 October 2026. Relevant source: Section 1, especially thm:main. Documentary claim record, not a premise of the finite theorem. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/01-introduction.tex

OAI227Stationary

OpenAI. Functional universality of critical SK autocorrelations. External stationary companion, dated 5 October 2026. Non-point stationary limit is recorded, not independently verified here. https://github.com/openai/math/blob/main/preprints/Functional-universality-of-critical-SK-autocorrelations-October-5-2026/build/main.tex

OAI227Background

OpenAI. The stationary edge input. Section 2 of the external critical-quench manuscript. Finite forms, replica coordinates, conditioned edge inputs, and relaxed-energy interface. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/02-background.tex

OAI227Edge

OpenAI. Gaussian estimates at the bottom edge scales. Section 3 of the external critical-quench manuscript. Relevant source label: prop:edge-estimates. Audited without importing its estimates. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/03-edge-estimates.tex

OAI227Warming

OpenAI. Warming at the critical scale. Section 4 of the external critical-quench manuscript. Relevant source label: thm:warming. Audited without importing its positive-time estimates. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/04-warming.tex

OAI227Entrance

OpenAI. Selection of the entrance law. Section 6 of the external critical-quench manuscript. Relevant source label: thm:entrance-selection. Audited without importing its uniqueness or existence theorem. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/06-entrance-selection.tex

OAI227History

OpenAI. Clock-history cutoffs. Section 7 of the external critical-quench manuscript. Documentary replacement interface. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/07-history-cutoffs.tex

OAI227Scores

OpenAI. Clock scores. Section 8 of the external critical-quench manuscript. Documentary score-projection interface. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/08-clock-scores.tex

OAI227Replacement

OpenAI. Replacement. Section 9 of the external critical-quench manuscript. Documentary disorder-comparison and functional-tightness interface, not a locally verified universality theorem. https://github.com/openai/math/blob/main/preprints/Universality-of-critical-quench-autocorrelations-in-the-Sherrington-Kirkpatrick-model-October-5-2026/build/sections/09-replacement.tex

Lean227

OpenAI. Critical SK autocorrelation processes and dynamics across the temperature transition. Repository scope note lean/docs/227.md. Consulted 14 October 2026. A scope description is distinguished from an executed proof. https://github.com/openai/math/blob/main/lean/docs/227.md

LeanSKRatio

OpenAI. SKRatio.lean. Repository Comparator target. The inspected ratio_cutoff theorem body contains sorry. Consulted 14 October 2026. https://github.com/openai/math/blob/main/lean/ComparatorChallenges/SKRatio.lean

LeanCriticalMixing

OpenAI. CriticalSKMixing.lean. Repository Comparator target. The inspected critical_mixing_bounds theorem body contains sorry. Consulted 14 October 2026. https://github.com/openai/math/blob/main/lean/ComparatorChallenges/CriticalSKMixing.lean

Catalogue

OpenAI. External mathematics catalogue, repository overview.tex. Family identifiers and their nominated comparisons are documentary records, not theorem premises. https://github.com/openai/math/blob/main/overview.tex

CheungEm04A

N. Cheung. Em04-A, version 2. Supplied manuscript Em04-A-v2.tex, section “Physicality and exact reduction.” Relevant label: thm:reduction. A specified zero-temperature XY-chain reduction; not a classical SK heat-bath generator. Enter Calculus Companion.

CheungHawk02D

N. Cheung. Hawk02-D, version 1. Supplied manuscript Hawk02-D.tex, section “Actual complete-residual recovery.” Relevant labels: thm:main and cor:window. A specified quadratic fermionic model and its complete residual, not the present classical spin chain. Enter Calculus Companion.

CheungHawk02E

N. Cheung. Hawk02-E, version 1. Supplied manuscript Hawk02-E.tex, section “Gravitational correspondence and a common validity interval,” subsection “Audit of the proposed auxiliary mathematics.” Explicitly separates classical SK gap estimates from quantum SYK dilation estimates. Enter Calculus Companion.

CheungEn07C

N. Cheung. En07-C, version 1. Supplied manuscript En07-C.tex. Relevant supplied labels: thm:exact and thm:release. Complete-complement recovery and external thermal inputs, not an identification of SK inverse temperature. Enter Calculus Companion.

CheungI

N. Cheung. Landmark I, version 2. Supplied manuscript I.tex. Relevant label: thm:main. Finite Born probabilities and destructive projective residuals within a stated strategy class. Enter Calculus Companion.

CheungVIIIB

N. Cheung. Landmark VIII-B, version 3. Supplied manuscript VIII-B-v3.tex, section “Classical table decoding is not quantum recovery.” Relevant label: prop:classical-recovery. Record-only quantum recovery obstruction, not a classical autocorrelation theorem. Enter Calculus Companion.

CheungHawk04B

N. Cheung. Hawk04-B, version 2. Supplied manuscript Hawk04-B.tex. Complete-complement recovery, typed destructive readout, and record-only recovery distinctions. Enter Calculus Companion.

CheungEn01B

N. Cheung. En01-B, version 2. Supplied manuscript En01-B-v2.tex. The supplied dossier's bounded-statistic and calibration coverage comparison is used only as a methodological template. No collapse-model generator is imported. Enter Calculus Companion.

CheungEn01C

N. Cheung. En01-C, version 1. Supplied manuscript En01-C.tex. Relevant comparison: thm:certificate, bounded complete-record finite-sample coverage. Its named physical statistic is not an SK autocorrelation. Enter Calculus Companion.

CheungEm03G

N. Cheung. Em03-G, version 1. Supplied manuscript Em03-G-v1.tex. Relevant labels: thm:lower, thm:compacttransmission, and prop:Fobstruction. Fixed finite-resource lower bounds and growing-resource transmission are kept separate. Enter Calculus Companion.

CheungOai265A

N. Cheung. Oai265-A, supplied version 1. Relevant labels: def:determination and thm:separation. Static-record, complete-channel, and temporal-history separations. Enter Calculus Companion.

CheungXXIIA

N. Cheung. XXII-A, version 1. Supplied manuscript XXII-A.tex. Relevant label: thm:separation. Scheduled ancestry, operational influence, and a separately supplied causal relation. Enter Calculus Companion.

CheungXIVI

N. Cheung. Landmark XIV-I, version 1. Supplied manuscript XIV-I.tex. Relevant labels: thm:I2, thm:I3, and thm:release. Internal amplitude construction and the distinct unresolved joint characteristic map. Documentary boundary only.

CheungXIVJ

N. Cheung. Landmark XIV-J, version 1. Supplied manuscript XIV-J.tex. Relevant labels: prop:descent, thm:reference, thm:J2, and cor:noadmission. Supported-sector references do not constitute the full joint characteristic construction. Documentary boundary only.

CheungXVB

N. Cheung. Landmark XV-B, supplied version 2. Relevant labels: thm:lifting and thm:release. Abstract reconstruction-lifting and extension interfaces; the supplied graph-specific construction remains unresolved. Documentary boundary only.

Dossier

User-supplied Oai227-A plan and comparative source dossier. Includes version-specific Cheung excerpts, family catalogue descriptions, and nominations of Oai272-A and Oai283-A. Supplied retrieval label: 178f233f (retrieval-3). Not an exhaustive corpus scan or independent proof verification.