The model and the result

Fix an exclusion distance \(a>0\). On the flat torus \(\Lambda_L=(\mathbb R/L\mathbb Z)^3\), let \(d_L\) denote Euclidean torus distance and set \[\Omega_{N,L,a} =\{(x_1,\ldots,x_N)\in\Lambda_L^N: d_L(x_i,x_j)>a\text{ whenever }i\ne j\}.\] In units \(\hbar^2/(2m)=k_B=1\), the hard-sphere Hamiltonian \(H_{N,L,a}\) is the self-adjoint operator associated with \[q[f]=\sum_{i=1}^N\int_{\Omega_{N,L,a}}|\nabla_i f|^2, \qquad f\in H^1_0(\Omega_{N,L,a})\text{ symmetric}.\] For \(T>0\), its canonical state and one-particle density matrix are \[\Gamma_{N,L,T}= \frac{e^{-H_{N,L,a}/T}}{\mathop{\mathrm{Tr}}e^{-H_{N,L,a}/T}},\qquad \gamma^{(1)}_{N,L,T}=N\mathop{\mathrm{Tr}}_{2,\ldots,N}\Gamma_{N,L,T}.\] We use zero extension from the allowed configuration set when taking partial traces. Thus \(\gamma^{(1)}_{N,L,T}\) acts on \(L^2(\Lambda_L)\) and has trace \(N\). The constant orbital is \(u_{0,L}=L^{-3/2}\). Macroscopic occupation of this orbital means that \(N^{-1}\langle u_{0,L},\gamma^{(1)}_{N,L,T}u_{0,L}\rangle\) has a positive lower limit as \(L\to\infty\) with \(N/L^3\) tending to a fixed density. Translation invariance makes the constant orbital an eigenvector of the density matrix, so this gives condensation in the sense of Penrose and Onsager (1956).

The conclusion concerns the exact canonical Gibbs state. The temperature obtained by the proof is small and is not intended to locate the phase transition. Its role is to provide a strictly positive temperature at every sufficiently small fixed gas parameter \(\rho a^3\).

Historical context and related methods

The statistical origin of Bose–Einstein condensation is Bose’s counting of light quanta and Einstein’s extension to material particles (Bose 1924; Einstein 1924, 1925). For interacting particles, Penrose and Onsager formulated condensation through a macroscopic eigenvalue of the one-particle density matrix (Penrose and Onsager 1956). In a translation-invariant gas, the constant orbital is the natural candidate. Bogoliubov’s theory expands about its macroscopic occupation to obtain the low-energy excitation spectrum (Bogoliubov 1947); the hard-sphere calculation of Lee, Huang and Yang predicts the leading energy correction and depletion (Lee et al. 1957). Establishing the occupation for the exact equilibrium state is a separate mathematical question from deriving these expansions.

For hard spheres, rigorous energy bounds began with Dyson (Dyson 1957), and Lieb and Yngvason obtained the leading dilute asymptotics (Lieb and Yngvason 1998). Fournais and Solovej proved the Lee–Huang–Yang lower bound for interactions including hard cores (Fournais and Solovej 2023); Basti, Brooks, Cenatiempo, Olgiati and Schlein proved the matching upper bound for hard spheres and then for general nonnegative short-range interactions (Basti et al. 2026b, 2026a). At positive temperature, Fournais, Junge, Girardot, Morin, Olivieri and Triay obtained a low-temperature free-energy lower bound that includes hard cores (Fournais et al. 2026). These results control thermodynamic energies. They do not by themselves give a volume-uniform lower bound on a single orbital’s occupation: the one-particle kinetic gap tends to zero as the box grows.

Rigorous continuum condensation has been established in several scaling regimes. Lieb and Seiringer proved complete ground-state condensation in the trapped Gross–Pitaevskii limit (Lieb and Seiringer 2002). At positive temperature, Deuchert, Seiringer and Yngvason treated a trapped gas in a combined thermodynamic and Gross–Pitaevskii limit (Deuchert et al. 2019), and Deuchert and Seiringer treated the homogeneous canonical gas in Gross–Pitaevskii scaling (Deuchert and Seiringer 2020). The latter theorem allows hard cores, but their scattering length is proportional to \(L/N\) and therefore vanishes at fixed density as \(N\) grows. Further results of Fournais, Chong, Liang and Nam, and Junge allow increasing box sizes coupled to increasing dilution (Fournais 2021; Chong et al. 2026; Junge 2026). Such coupled limits do not permit unrestricted volume growth at a fixed positive gas parameter. Deuchert and Seiringer also established positive-temperature condensation in a combined semiclassical and mean-field limit for a trapped gas (Deuchert and Seiringer 2021).

Fixed-parameter thermodynamic condensation also has precedents with different interactions and state formulations. Aizenman, Lieb, Seiringer, Solovej and Yngvason proved low-temperature condensation for a hard-core lattice gas at half filling (Aizenman et al. 2004). Sütő’s continuum theorem assumes both the potential and its Fourier transform to be nonnegative, with integrability and regularity hypotheses that exclude a literal hard core (Sütő 2023, Theorem 1.2). Galanda and Pinamonti construct algebraic equilibrium states for smooth interactions in coupled weak-interaction limits and, after renormalization, in Gross–Pitaevskii scaling with vanishing temperature (Galanda and Pinamonti 2025, 2026). The present theorem concerns the exact canonical hard-sphere state with the exclusion distance, positive density, and positive temperature all fixed before the volume grows. It gives a positive condensate fraction at sufficiently low temperature; it does not determine the transition temperature or the leading depletion.

Two companion articles provide the immediate starting point. Ground-state condensation in the dilute hard-sphere gas (OpenAI 2026b) treats the fixed-parameter ground-state problem and develops hard-core bridge replacements, movable groups of particles, routes avoiding unusable cells, and cancellation of conditional normalizers. A density-uniform condensate bound for dilute Bose gases (OpenAI 2026a) treats bounded finite-range repulsive potentials at positive temperature and supplies localization and short-slab trajectory estimates, as well as the underlying lattice-path construction. We reproduce the arguments needed here. The additional issue is to obtain joint spatial and trajectory estimates for the hard-core canonical Gibbs state, and to make the short-path comparison control its one-particle density matrix.

The local analysis builds on established tools. The hard-core ray estimate belongs to the Dyson local-energy method, and the subdivision and two-particle bounds are related to the work of Lieb and Yngvason and of Lundholm, Portmann and Solovej (Dyson 1957; Lieb and Yngvason 1998; Lundholm et al. 2015). Particle insertion has antecedents in the nearest-neighbor trial states of Dyson and Lieb, Seiringer and Yngvason (Dyson 1957; Lieb et al. 2000). Localization into two particle species uses the Fock-space localization formalism of Dereziński and Gérard, its many-body development by Lewin, and its thermal application by Deuchert, Seiringer and Yngvason (Dereziński and Gérard 1999; Lewin 2011; Deuchert et al. 2019). Strong subadditivity and monotonicity of relative entropy provide the entropy comparisons (Lieb and Ruskai 1973; Lindblad 1975). The use of positive imaginary-time paths goes back to Feynman’s formulation (Feynman 1953); Ueltschi’s account distinguishes cycle information from one-particle off-diagonal order (Ueltschi 2006). Here the overlap identity addresses the one-particle occupation directly.

The long-distance comparison has a separate probabilistic ancestry. Benjamini, Pemantle and Peres constructed paths with exponential intersection tails (Benjamini et al. 1998); Häggström and Mossel developed a construction using random biases on blocks at several scales (Häggström and Mossel 1998). The finite-endpoint averaging method of Abbe, Massoulié, Montanari, Sly and Srivastava, and its adaptation by Garban and Spencer, turn intersection control into long-range information or order (Abbe et al. 2018; Garban and Spencer 2022). Averaging path likelihoods before taking their second moments also appears in trail detection and in the point-reassignment argument of Peres and Sly (Arias-Castro et al. 2008; Berger and Peres 2013; Peres and Sly 2014). Our lattice construction follows the explicit skeleton in OpenAI (2026a, sec. 8.1) and the obstacle detours in OpenAI (2026b, sec. 7), using Timár’s boundary-connectivity theorem (Timár 2013, Theorem 4). The hard-core comparison retains the exact interaction normalizers; after averaging two route changes, their cost is controlled by mutual encounters rather than by the length of either route.

The argument

The starting point is the short-path comparison developed for the hard-sphere ground state in OpenAI (2026b). Its use at positive temperature requires two changes. First, the local hypotheses must hold jointly for arbitrarily many prescribed cells under a thermal path measure. Second, the path comparison must control the one-particle density matrix of a mixed state. We prove the needed thermal estimates and retain the deterministic comparison mechanism. The bridge, lattice, and measure comparison arguments used below are included with proofs.

To identify the overlap we must bound, let \(\Phi(X,W')\) be the nonnegative integral kernel of \(\Gamma_{N,L,T}^{1/2}\), with \(X,W'\in\Lambda_L^N\). Write \(X=(x,X')\), where \(X'\) is the ordered configuration of the other \(N-1\) particles, called the bath. Factoring the Gibbs kernel through its square root gives \[\frac{\langle u_{0,L},\gamma^{(1)}_{N,L,T}u_{0,L}\rangle}{N} =\frac1{L^3}\int \Phi(x,X',W')\Phi(y,X',W')\, \,\mathrm dx\,\,\mathrm dy\,\,\mathrm dX'\,\,\mathrm dW'.\] Thus the two factors have the same bath \(X'\) and retained configuration \(W'\), while the distinguished particle moves from \(x\) to \(y\). Section 5 realizes \(\Phi(X,W')^2\) as the joint law of the midpoint configuration and \(W'\) on a short Brownian time interval. Once the interval endpoints and \(W'\) are fixed, the conditional law is a product of Brownian bridge laws conditioned on hard avoidance. This representation lets us analyze local changes against deterministic obstacle paths while retaining the mixed-state overlap above.

The estimates are made in the scaled units of Section 2, in which a unit cell contains \(D\gg1\) particles and the core radius is \(\alpha/D\), with \(\alpha\) in a fixed interval. Sections 3 and 4 give joint bounds for low cell counts and excessively close neighbors. These estimates use entropy as well as energy: a relative-entropy inequality controls a diagonal change of density, and a family of normalized insertion maps with a uniform frame bound controls the free-energy cost of adding a particle, even in bounded attractive fields.

The remaining local conditions concern whole trajectories. Section 5 marks paths that violate a condition, assigns auxiliary particle species to the marks, and removes their hard-core constraints in an upper bound. A trace estimate for a heat semigroup between two Lipschitz multipliers converts the marked path moments into free-energy estimates; exterior powers permit control of every positive trace power. These arguments adapt the thermal methods of OpenAI (2026a) to Dirichlet hard-core domains. They yield an exponential bound in the number of prescribed defective cells. This joint bound will control obstructing clusters when routes are drawn through the remaining cells.

The local bridge estimates of Section 6 show that most cells contain many labels whose paths can be moved through any adjacent cell with uniformly positive success probability. Section 7 splits these labels into groups and exposes all paths outside one group. The usable cells are then determined by this exposed environment. Section 8 constructs random routes between many pairs of cells, with a bounded exponential moment for the encounters of two independently drawn routes in the same environment.

Section 9 uses one such route to construct two path configurations with shifted midpoint assignments. Removing a different tagged particle from each leaves the same bath midpoints and the same \(W'\), as required by the overlap identity. To compare the resulting measure with the two original midpoint laws, we average over routes before taking the second moment of its density. Conditional normalizers cancel away from encounters between two routes, so the cost is controlled by their encounters rather than by their lengths. The lattice estimate bounds that cost, and a common-measure inequality gives positive overlap for a positive fraction of all cell pairs.

The order of the choices is essential. The path duration and the group size are fixed before the density threshold, and all are fixed before the volume tends to infinity. Section 10 returns to physical units and verifies directly that the resulting temperature is independent of that volume.

Positive kernels and retained particles

Let \(H_j^{\rm lab}\) be the labelled Dirichlet operator on \(\Omega_j\), let \(K_s^{(j)}\) be its heat kernel, and let \(P_j\) be the orthogonal projection onto symmetric functions. When \(j=N\), denote the kernel of \(e^{-sH_N^{\rm lab}}P_N\) by \(B_s^{\rm sym}\). This operator is the bosonic semigroup extended by zero on the orthogonal complement of the symmetric subspace. Explicitly it is the average of \(K_s^{(N)}\) over permutations of one endpoint. It is nonnegative and obeys the semigroup law with integration over ordered configurations, without any additional factorial.

The labelled kernel is the free Brownian kernel, with generator \(\Delta\), restricted to paths whose pair distances stay strictly above \(r\). One way to establish this exact boundary convention is to exhaust \(\Omega_j\) by relatively compact smooth open sets. Their Dirichlet forms increase in domain to \(H^1_0(\Omega_j)\), giving strong semigroup convergence. A continuous path that stays in \(\Omega_j\) on a compact time interval has compact image there and is captured by the exhaustion. Monotone convergence of killed path measures proves the representation. The same reasoning, or bounded-potential Feynman–Kac, treats the fields above. This is the open-domain argument used in OpenAI (2026b, sec. 4).

Heat traces are finite: the zero-extension form embedding and the min–max principle compare the Dirichlet eigenvalues to those of the free torus operator. Kernel identities are needed only almost everywhere. Splitting a semigroup at positive times justifies diagonal trace formulas without selecting values of a general kernel on a null set.

Partial traces preserve the remaining hard-core conditions and the kinetic expectations of the retained coordinates. The form-domain justification is given with the entropy estimates in Section 3, before these marginals are used to compare particle numbers.

The estimate to be proved

Let \(\Gamma_N=Z_N^{-1}e^{-\beta H_N}\), let \(\gamma_N^{(1)}=N\mathop{\mathrm{Tr}}_{2,\ldots,N}\Gamma_N\), and let \(u_0=V^{-1/2}\). The occupation fraction is \[B_{\rm occ}=N^{-1}\langle u_0,\gamma_N^{(1)}u_0\rangle.\]

Sections 3 and 4 establish free-energy estimates and joint bounds on the position counts. Section 5 extends those bounds to a short interval of particle paths. The remaining sections compare configurations by moving selected labels along paths of usable cells. This yields Theorem 2 in Section 9; the final change of units proves Theorem 1.

Two local consequences of the hard core

The following arguments reproduce the local estimates of OpenAI (2026b, sec. 3, “Two local kinetic inequalities”). Their ingredients are the two-particle coercivity used in local exclusion estimates (Lundholm et al. 2015, Proposition 10) and Neumann subdivision (Lieb and Yngvason 1998).

Entropy and admissible marginals

We shall apply kinetic inequalities to mixed states, to their marginals, and to states confined to a spatial region. The following estimate is the ideal Bose entropy bound used in OpenAI (2026a, sec. 3, “An entropy bound”).

We record a domain fact used repeatedly below. A marginal obtained by retaining some particle coordinates of a finite-energy hard-core state still has finite kinetic energy and satisfies the hard-core Dirichlet condition among the retained coordinates. Indeed, first approximate a form vector by smooth functions compactly supported in the allowed configuration set. Slicing in the discarded variables places it in the retained form domain with values in the \(L^2\) space of the other variables. Expansion in an orthonormal basis of that space shows that the squared form norms of its coefficient functions sum to the integrated form norm. Passing to the limit and then to a spectral decomposition of the state proves the assertion for partial traces. The kinetic expectation in the retained variables is unchanged. Symmetry of a bosonic state places each such marginal on the corresponding symmetric subspace.

Insertion without changing the old marginal

The nearest-neighbor trial construction goes back to Lieb et al. (2000, sec. 3.2). We use the configurationwise normalization of OpenAI (2026b, sec. 3, “Normalized insertion”), because it preserves the old marginal exactly.

Localization and diagonal tilting

A local penalty and density control in a field

For a nonempty set of sites \(A\subset\mathcal L_K\), define, for a configuration of any particle number \(J\le N\), \[\begin{align*} s_0&=bD^{-1/3},\qquad 0<b<1,\tag{18}\\ f_A(X)&=\sum_{i=1}^J e^{-d(x_i,A)},\tag{19}\\ k_A(X)&=\#\{i:d(x_i,A)\le6,\ d_i\le2s_0\}. \tag{20}\end{align*}\] The parameter \(b\) will be chosen small after the low-count threshold has been fixed. We always increase \(D\) so that \(r<s_0<1/2\).

The mean estimate will control the effect of small fields on partition functions. To produce many movable particles, we need the stronger joint statements proved next.

Simultaneous shortages are exponentially unlikely

Simultaneous failures of separation

Fix from now on \(\theta>0\) so that \(3\theta<\ell/2\). For a site \(v\), define \[ C_v(X)=\#\{i:d(x_i,v)\le5,\ d_i\le s_0\}. \tag{27}\] The enlarged radius allows this count to control endpoint defects of particles starting in neighboring cells.

The spatial choices have a fixed order: first \(\alpha_0\) large and \(\ell\) small, then \(\theta\) with \(3\theta<\ell/2\), then \(b\) small, and finally \(D\) large. These estimates provide simultaneous endpoint control for arbitrarily many prescribed cells. The next section extends that control to every path visiting a cell during a short imaginary-time interval.

The path law and its purification

Fix \(0<t\le1\), set \(\delta=2t\), and require \(\beta>\delta\). The time \(t\) will be fixed before the lower threshold on \(D\). Let \(\nu_N\) be the measure of \(N\) independent torus Brownian motions with generator \(\Delta\) on \([0,\delta]\), with Lebesgue initial measure. Write \[X(s)=(\omega_1(s),\ldots,\omega_N(s)),\qquad Y=X(0),\qquad Z=X(\delta).\] In addition to these labelled paths, introduce a configuration \(W'\in\Lambda_K^N\). With the symmetric heat-kernel convention of Section 2, define \[ \,\mathrm d\mathcal R(\omega,W')= \frac{B_{\beta/2-t}^{\rm sym}(W',Y) B_{\beta/2-t}^{\rm sym}(Z,W')}{Z_N} \mathbf 1_{\{d(\omega_i(s),\omega_j(s))>r\ \forall s,\ i<j\}} \,\mathrm d\nu_N(\omega)\,\,\mathrm dW'. \tag{30}\] All path spaces carry their Borel sigma fields. Continuous torus paths have continuous Euclidean lifts, unique after specifying the initial lift; lifted increments and diameters are independent of that choice.

The extra variable \(W'\) is what permits a mixed Gibbs state to be treated by a nonnegative squared density. It will be held fixed in the later path changes. No ground-state eigenfunction enters Equation (30).

Regular trajectories and certificates

Recall \(s_0=bD^{-1/3}\) and the fixed parameters \(\ell,\theta,b\) from the spatial estimates, with \(3\theta<\ell/2\). Put \[ h_0=D^{-1},\qquad \gamma=\frac1{12},\qquad m_t=\lceil t/r^2\rceil,\qquad \tau=t/m_t. \tag{33}\] Take \(D\) large enough that \(h_0<t\) and \(r^2/2\le\tau\le r^2\). Divide each half of the slab into \(m_t\) equal intervals, denoted together by \(I_1,\ldots,I_{2m_t}\). For a lifted path define \[A_j(\omega)=r^{-1}\mathop{\mathrm{diam}}\bigl(\widetilde\omega(I_j)\bigr).\] The following definition is the one used in OpenAI (2026b, Section “A stationary sample of hard-core paths,” definition of a regular path).

We will use both the free-motion and the bridge forms of the next estimate. The latter supplies the individual regularity tests for the replacement paths in Section 6.

Write \(C_v(X)\) for the close count from Proposition 13, namely \[C_v(X)=\#\{i:d(X_i,v)\le5,\ d_i(X)\le s_0\}.\] A certificate at \(v\) consists of the following conditions on the full path sample:

1. \(n_v(Y)\ge\ell D\) and \(C_v(Y),C_v(Z)<\theta D\);

2. at most \(H_1D\) paths visit the radius-\(12\) ball about \(v\), every visiting path is regular, and fewer than \(\theta D\) visiting paths have lifted diameter greater than one.

These are precisely the spatial and trajectory conditions needed for the deterministic bridge estimates. In particular, the certificate is an event of the full sample; it is not information on which we will condition the paths to be changed.

The endpoint parts already follow from Propositions 12 and 13. The issue is to control many path failures jointly under \(\mathcal R\). We establish that estimate next, and prove Proposition 17 at the end of the section.

A localized kernel for one marked path

For a nonempty set \(A\) of sites let \(J_A(\omega)\) be the number of sites in \(A\) whose radius-\(12\) balls the path visits. Consider the following three single-path events: \[E_{\rm all}=\{\text{all paths}\},\qquad E_{\rm diam}=\{\mathop{\mathrm{diam}}\widetilde\omega>1\},\qquad E_{\rm irr}=\{\omega\text{ is not regular}\}.\] For \(E\) equal to one of these events and \(\lambda>0\), we will bound \[ \begin{split} \mathfrak M &=\mathbb E_{\mathcal R}\exp\left( \lambda\sum_{i=1}^N J_A(\omega_i)\mathbf 1_E(\omega_i)\right)\\ &=\mathbb E_{\mathcal R}\prod_{i=1}^N \left[1+\bigl(e^{\lambda J_A(\omega_i)}-1\bigr) \mathbf 1_E(\omega_i)\right]. \end{split} \tag{36}\] Expanding this product selects subsets of marked labels, each carrying weight \((e^{\lambda J_A(\omega)}-1)\mathbf 1_E(\omega)\). We first bound the free-path kernel for one such marked label.

We partition paths by a nonnegative integer \(n\). On the first half, mark the first exit from the unit ball about the starting point, then the first exit from the unit ball about that exit point, and continue up to time \(t\). On the second half make the same construction backwards from the terminal point. Denote the total number of completed exits on the two halves by \(n(\omega)\), and write \(n\) for its value on a fixed bin. Continuity and uniform continuity on the compact time interval make this number finite for each path. Between consecutive marks the lift lies in a unit ball. Thus on bin \(n\), \[ J_A\le C(n+1),\qquad |\widetilde\omega(2t)-\widetilde\omega(0)|\le n+2. \tag{37}\] If \(J_A>0\), an endpoint is at lifted distance at most \(n+3\) from any visiting point: the first half’s endpoint-to-midpoint displacement is at most \(n_1+1\), and the diameter of the other half is at most \(n_2+2\). Thus both endpoints have torus distance at most \(n+15\) from \(A\). By Equation (37), the unit tube about the straight lifted endpoint segment projects into \(\{x:d(x,A)<2n+18\}\), hence into \(\{x:d(x,A)<32(n+1)\}\).

Set \(O_n=\{x:d(x,A)<32(n+1)+2\}\). Choose a Lipschitz cutoff \(0\le p_n\le1\) equal to one when \(d(x,A)\le32(n+1)\) and zero when \(d(x,A)\ge32(n+1)+1\), with \(|\nabla p_n|\le C\). Its support is compact in \(O_n\). These definitions allow \(O_n\) to be the whole torus. They satisfy \[ |O_n|\le C(n+1)^3|A|, \qquad O_n\text{ is covered by at most }C(n+1)^3|A| \text{ unit cells}. \tag{38}\] Here \(|O_n|\) is volume and \(|A|\) is cardinality.

Let \(\mathcal K_n(y,z)\) be the unnormalized free torus path kernel of duration \(\delta\) with the marking weight and the bin-\(n\) restriction. Thus endpoint integration against \(\mathcal K_n\) is the free-path integral against that weight, without any hard-core restriction.

The factor \(\varepsilon^{1/3}\) records the rarity of the single-path failure. The confinement to \(O_n\) will ensure that the interacting moment costs a multiple of \(|A|\), even when the number of marked paths is unrestricted.

Colors and the trace-sandwich estimate

Choose a constant \(m_0\) sufficiently large, depending only on the upper increment constant in Proposition 7 and the fixed \(\alpha\)-window. Define \[ M_n=(m_0+n)/\delta,\qquad \eta_n=l_n e^{m_0+n}. \tag{42}\] We choose \(m_0\) so that, for \(\delta\le2\), \[ M_n/2\ge C_{\rm inc}\alpha+1, \qquad \beta M_n/2\ge1, \tag{43}\] where \(C_{\rm inc}\alpha\) bounds an upper particle-number increment and \(D\ge1\). The choice of \(m_0\) is independent of \(t\).

First truncate the permitted marked bins at \(n\le n_*\), so that the moment in Equation (36) becomes \[\mathfrak M_{n_*} =\mathbb E_{\mathcal R}\prod_{i=1}^N \left[1+\bigl(e^{\lambda J_A(\omega_i)}-1\bigr) \mathbf 1_E(\omega_i)\mathbf 1_{\{n(\omega_i)\le n_*\}}\right].\] The enlarged one-particle space is \[\mathfrak h_e=L^2(\Lambda_K) \oplus\bigoplus_{n=0}^{n_*}L^2(O_n).\] Its first summand is called the original color, and the others are the marked colors. In each labelled color assignment of \(N\) particles impose the hard exclusion only between original-color particles. The direct sum of these allowed labelled spaces is denoted by \(\mathcal H_e^{\rm lab}\). On it let \(\mathbb H^{\rm lab}\) be the operator with the original-color hard-core kinetic form, and with one-particle operator \(-c_1\Delta_{O_n}+M_n\) on a particle of color \(n\). There are no interactions involving a marked color. Simultaneous permutations of positions and colors commute with \(\mathbb H^{\rm lab}\). Denote their invariant subspace by \(\mathcal H_e\), and denote the restriction of \(\mathbb H^{\rm lab}\) to it by \(\mathbb H\).

On zero-extended original \(N\)-particle functions apply in each coordinate the map \[v_e f=(f,(\sqrt{\eta_n}p_n f)_{0\le n\le n_*}), \qquad V_{\rm lab}=v_e^{\otimes N}.\] Here \(V_{\rm lab}\) has domain \(L^2(\Omega_N)\), the original labelled hard-core space, and takes values in \(\mathcal H_e^{\rm lab}\). It maps form-domain functions to form-domain functions: the original hard-core zeros remain, the marked cutoffs are compactly supported in their \(O_n\), and all multipliers are Lipschitz. Define first the labelled operator \[\mathcal T_{\rm lab} =V_{\rm lab}^*e^{-\delta\mathbb H^{\rm lab}}V_{\rm lab}.\] The map \(V_{\rm lab}\) intertwines coordinate permutations with simultaneous position-color permutations. Its restriction \(V_e\) to the original symmetric space therefore takes values in \(\mathcal H_e\), and \(\mathcal T_{\rm lab}\) commutes with the original symmetrizer \(P_{\rm sym}\). Its symmetric restriction is \[\mathcal T=\mathcal T_{\rm lab}|_{\operatorname{ran}P_{\rm sym}} =V_e^*e^{-\delta\mathbb H}V_e.\]

Expanding the product defining the trajectory moment marks subsets of labels. For every marked subset, bin its paths and drop all collision prohibitions incident to them. The nonnegative path integral increases. Apply Lemma 18 to each marked path. Its coefficient is reproduced exactly by the color map, since \(\eta_n e^{-\delta M_n}=l_n\). Each choice of marked labels and their bins appears once in the labelled color direct sum. Thus the tested labelled slab kernel is bounded pointwise by the kernel \(K_{\mathcal T_{\rm lab}}\) of \(\mathcal T_{\rm lab}\), before any restriction to symmetric functions.

The outer kernel \(B_{\beta-\delta}^{\rm sym}\) is nonnegative. Let \(H_N^{\rm lab}\) denote the original labelled hard-core Hamiltonian. Integrating the pointwise bound against this outer kernel gives the symmetric trace by the following exact identity: \[\begin{align*} &\int B_{\beta-\delta}^{\rm sym}(Z,Y) K_{\mathcal T_{\rm lab}}(Y,Z)\,\,\mathrm dY\,\,\mathrm dZ\\ &\qquad=\mathop{\mathrm{Tr}}_{\rm lab}\left( e^{-(\beta-\delta)H_N^{\rm lab}} P_{\rm sym}\mathcal T_{\rm lab}\right) =\mathop{\mathrm{Tr}}_{\rm sym}\left(e^{-(\beta-\delta)H_N}\mathcal T\right). \end{align*}\] Indeed both labelled operators commute with \(P_{\rm sym}\); the product in the middle vanishes on its orthogonal complement and restricts to the final product on its range. The sole permutation normalization is the average \(P_{\rm sym}=N!^{-1}\sum_\pi U_\pi\) already present in the outer kernel. No factorial is inserted in the labelled color expansion or in this trace identity. Consequently the truncated moment satisfies \[ \mathfrak M_{n_*} \le\frac{\mathop{\mathrm{Tr}}_{\rm sym} (e^{-(\beta-\delta)H_N}\mathcal T)}{Z_N} \le\left(\frac{\mathop{\mathrm{Tr}}_{\rm sym}\mathcal T^{\beta/\delta}} {Z_N}\right)^{\delta/\beta}. \tag{44}\] The second inequality is Schatten Hölder with exponents \(\beta/(\beta-\delta)\) and \(\beta/\delta\). All operators have finite positive-time traces at the fixed finite volume and particle number.

To control the large power in Equation (44), we must account for the norm of the color map. Define \[ a(x)=\frac12\log\left(1+\sum_{n=0}^{n_*}\eta_np_n(x)^2\right), \qquad A_0=\sum_{i=1}^N a(x_i). \tag{45}\] The same position multiplier acts in every color. The map \(U_e=e^{-A_0}V_e\) is isometric, because the squared pointwise norm of its one-coordinate color vector is one. Therefore \[\mathcal T=U_e^*X_0U_e, \qquad X_0=e^{A_0}e^{-\delta\mathbb H}e^{A_0}.\] Eigenvalue min–max for positive compact compressions gives \(\mathop{\mathrm{Tr}}\mathcal T^q\le\mathop{\mathrm{Tr}}X_0^q\) for every \(q>0\). The next lemma converts this sandwich into a heat trace with a bounded attractive field.

The interacting trajectory moment

The remaining task is to compare the enlarged heat trace with \(Z_N\). The original color will be estimated by the field-density bound; the positive gaps will pay for the other colors. Spatial confinement in Equation (38) keeps both costs proportional to the number of tested sites.

Completion of the certificate estimate

We first record the sizes of the two costs in Equation (50). The Gaussian bin tail in Equation (39) implies \[ \sum_{n\ge0}(n+1)^3\eta_n \le C_\lambda\lambda\varepsilon^{1/3}, \tag{54}\] where \(C_\lambda\) is bounded on bounded \(\lambda\)-intervals, uniformly for \(0<t\le1\). Indeed the summand is bounded by a constant times \(\lambda\varepsilon^{1/3}(n+1)^4 e^{C\lambda(n+1)+n-cn^2}\), including the fixed factor \(e^{m_0}\). The same estimate without \((n+1)^3\) controls the smallness condition. Since \(\beta\ge D\) and \(\delta\le2\), the second term of Equation (50) is \(o(1)|A|\) as \(D\to\infty\), uniformly in \(0<t\le1\) and \(K\ge100\).

We have obtained an unconditional joint bound for failure of the full-path certificates, with no loss proportional to the total volume. The next two sections use these certificates to find movable paths and then expose their environment while preserving an exact conditional bridge law.

Separated endpoints and Gaussian densities

Collision with a deterministic obstacle

Many paths can be moved successfully

The averaged estimate now pays for all nearby obstacles. The following statement separates that deterministic estimate from the random cell certificates that will supply its hypotheses.

Eligible labels and their local trial laws

The endpoints \(Y,Z\) and path regularity are those of Section 5. A label \(i\) is eligible at \(v\) if

1. \(Y_i\in B_v\) and \(d(Z_i,v)\le3\);

2. \(d(Y_i,Y_j)>s_0\) and \(d(Z_i,Z_j)>s_0\) for every \(j\ne i\);

3. its trajectory is regular and remains in the radius-\(10\) ball about \(v\).

The eligible sets at distinct sites are disjoint, since the starting cells form a partition. When \(K\) is large, the confinement ball lifts injectively to Euclidean space, so the endpoints have unique lifts near the chosen lift of \(v\).

For each eligible label \(i\) at \(v\), a target cell is \(B_v\) or one of its six face-neighbor cells. Write \(Q_i^u\) for the probability law of two independent Euclidean bridges, each of duration \(t\), from \(Y_i\) to \(u\) and from \(u\) to \(Z_i\), projected to the torus. All lifts in this definition are near \(v\). For a collection \(F\) of fixed obstacle paths with distinct labels other than \(i\), put \[ \begin{split} C_i(F)=\{&\text{the trial is regular and stays within distance $10$ of $v$;}\\ &\text{it avoids every path in $F$ at distance $r$}\}. \end{split} \tag{67}\] Avoidance throughout means strict distance greater than \(r\) at every time. The endpoints are fixed in this notation.

Disjoint groups and the information retained

Choose an integer \(M\ge1\), to be fixed after the one-path comparison constant below, and put \[ G_D=\left\lfloor\frac{\ell D}{4M}\right\rfloor. \tag{69}\] We take \(D\) large enough that \(G_D\ge1\). At a site with at least \(MG_D\) eligible labels, choose an ordered list of \(MG_D\) distinct eligible labels uniformly without replacement, and divide it into \(G_D\) successive groups of size \(M\). If there are fewer, all groups at that site are empty. The allocation randomizations are independent between sites conditional on the full path sample, and use the eligible lists only.

Fix one group index \(g\in\{1,\ldots,G_D\}\). Let \(\mathcal I\) be the union of its labels over all sites. The exposed datum \(\mathcal B\) comprises

• both endpoint configurations, \(W'\), every eligibility indicator, and all allocation information;

• the complete trajectories of labels outside \(\mathcal I\).

These last trajectories form the frozen family \(F\). The law of \(\mathcal B\) is the pushforward of the thermal slab law \(\mathcal R\) and the allocation randomizations. No certificate event is included in this datum. Subsequent expectations over \(\mathcal B\) always use this unconditional law.

For \(i\in\mathcal I\) at site \(v\), let \(B_i\) be the unconditioned Euclidean bridge law of duration \(2t\) between its near endpoint lifts. Define \[ P_i(\,\mathrm d\omega_i)= \frac{\mathbf 1_{C_i(F)}\,B_i(\,\mathrm d\omega_i)}{a_i}, \qquad a_i=B_i(C_i(F)). \tag{70}\] The event \(C_i(F)\) includes the individual regularity and confinement cutoffs, as in Equation (67).

Accessibility and the probability of bad cells

For \(i\in\mathcal I\) and one of its target cells \(B_w\), set \[ T_i(w)=\{u\in B_w:Q_i^u(C_i(F))\ge0.9\}. \tag{72}\] A label is accessible if \(|T_i(w)|\ge0.99\) for all seven target cells. This property and all the sets \(T_i(w)\) depend only on \(\mathcal B\). Let \(\mathcal A_v\) be the accessible labels of the fixed group at \(v\). A site is good if \(|\mathcal A_v|\ge M/2\), and bad otherwise. The sets in Equation (72) are measurable: bridge kernels are measurable in their endpoints, and regularity, confinement and strict avoidance are Borel events of continuous paths.

One-path comparisons at fixed exposed data

The remaining estimates apply at a fixed datum, even when its unexposed trajectories no longer satisfy any full-sample certificate. Let \(i\) be accessible, let \(B_w\) be a target cell, and let \(U\subset T_i(w)\) be a measurable set of volume at least \(0.98\). Define the proposal \(\Pi_i^U\) by choosing \(u\) uniformly in \(U\) and then sampling \(Q_i^u\) conditioned on \(C_i(F)\). The target set is chosen using exposed data only; it must not depend on the trajectories of other unexposed labels.

We record explicitly how Proposition 29 applies when two proposals share a midpoint. Suppose that \(i\) and \(j\) are accessible labels for which \(B_w\) is a target cell, and put \(U=T_i(w)\cap T_j(w)\). Then \(|U|\ge0.98\). Choose one point uniformly in \(U\) and, conditionally on that point, choose two independent successful paths, one with each label’s bridge law. Each path separately has law \(\Pi_i^U\) or \(\Pi_j^U\). Thus each marginal has density at most \(G\) relative to its own \(P\)-law, and each has collision probability at most \(e_D\) against any fixed regular, confined opponent of a distinct label. These bounds integrate the common midpoint. They do not assert a collision bound conditionally on its value: choosing the midpoint at an opponent’s midpoint would force a collision. Nor do we assert a product density bound for the pair of paths, whose midpoints agree. If the two paths are used in two separately constrained configurations, there is no avoidance check between them. Union bounds for their separate checks therefore use only the two marginal estimates just proved. A factor consisting of one successful path together with its midpoint has path law \(\Pi_i^U\) and midpoint density at most \(1/0.98\le G\) relative to uniform measure on \(B_w\).

Each changed path has only \(CM\) potential opponents by confinement. Consequently a fixed number of separately constrained configurations has a one-variable failure bound of the form \(CMe_D\). The comparison argument will choose \(M\) after \(G\), then increase \(D\) so that this quantity is small. In the second-moment calculation, conditional normalizers will cancel away from encounters between the two lattice routes. This is what makes the final likelihood bound uniform in their lengths.

A folded random skeleton

The skeleton first advances in one coordinate while fluctuating in the other two. Its fluctuations are read forward and then backward, which fixes both endpoints without conditioning on a future value. Independent dyadic blocks make the future transverse displacement sufficiently unpredictable to give summable encounter probabilities. The use of unpredictability and intersection moments originates in Benjamini et al. (1998, Theorem 1.3 and Lemma 3.1); the aligned block construction is related to Häggström and Mossel (1998, sec. 3, Proposition 3.1). Finite-endpoint path averaging appears in Abbe et al. (2018, sec. 6, Lemma 6.1) and Garban and Spencer (2022, sec. 2, Lemma 2.5). The following explicit law and the two estimates are those of OpenAI (2026a, sec. 8.1).

Fix an admissible pair, choose a lift of \(v\), and give \(w\) the lift \(v+(n,d_2,d_3)\). For each \(j\in\{2,3\}\) use independent random variables \(U^{(j)}_{\ell,k}\), uniform on \([-1,1]\), for integers \(\ell,k\ge0\). Put \[ v_i^{(j)}=c_{\rm vel}\sum_{\ell\ge0}2^{-\ell/4} U^{(j)}_{\ell,\lfloor(i-1)/2^\ell\rfloor}, \qquad Z_t^{(j)}=\sum_{i=1}^t v_i^{(j)},\qquad Z_0^{(j)}=0. \tag{80}\] Fix \(c_{\rm vel}=(1-2^{-1/4})/2\), so that \(c_{\rm vel}\sum_{\ell\ge0}2^{-\ell/4}=1/2\). The series converges absolutely for every sample. The base vertices are \[ u_t=v+\left(t, \left\lfloor td_2/n+Z_{\min(t,n-t)}^{(2)}\right\rfloor, \left\lfloor td_3/n+Z_{\min(t,n-t)}^{(3)}\right\rfloor\right), \qquad 0\le t\le n. \tag{81}\] The endpoints are \(v,w\). Each base increment advances the first coordinate by one and changes each transverse coordinate by at most two. Refine it by first making the first-coordinate step, then all required steps in coordinate two, then those in coordinate three. This takes at most five nearest-neighbor steps. The occurrence list consists of the initial vertex and the vertex reached after each step, without adding an extra copy at the join between consecutive refinements. Denote the projected walk by \(\Gamma\) and retain this lift for the detour construction.

For two independent copies \(\Gamma,\Gamma'\) of this law and a fixed integer \(R_s\ge1\), define the occurrence count \[ J_{\rm occ}^{(R_s)}= \sum_{z\in\Gamma}\mathbf 1_{\{d_\infty(z,\Gamma')\le R_s\}} +\sum_{z'\in\Gamma'}\mathbf 1_{\{d_\infty(z',\Gamma)\le R_s\}}. \tag{82}\] Both sums count occurrences, including any repetitions. For a fixed \(B>0\), put \[S_B(\Gamma,\Gamma')= \sum_{z\in\Gamma}e^{-d_\infty(z,\Gamma')/B},\] again counting occurrences.

The skeleton law and its bounds use no many-particle parameter. In applying them, we draw the two arrays independently of each other and of the exposed datum \(\mathcal D\).

For later use we convert the occurrence count to our pair count. Every first-coordinate level of a lifted skeleton contains at most five occurrences: level zero has only the initial vertex, and all vertices created in the \(t\)th refinement have first coordinate \(v_1+t\). The first-coordinate span is \(n\le K/8\), so the periodic distance between two such levels is their ordinary distance. A fixed occurrence of \(\Gamma\) can therefore have at most \(5(2R+1)\) opposing occurrences within distance \(R\). With \(R_s=R\), this proves \[ J_R(\Gamma,\Gamma')\le 5(2R+1)J_{\rm occ}^{(R)}. \tag{90}\] The left side uses the double occurrence sum from Equation (78). This conversion uses the actual refinement law, as well as its moment bounds.

Finite components and their exterior boundaries

We record the deterministic facts used to move a lattice path around bad vertices. For a finite \(*\)-connected nonempty set \(C\subset\mathbb Z^3\), let \(\operatorname{fill}(C)\) consist of \(C\) and all finite nearest-neighbor components of \(\mathbb Z^3\setminus C\). The remaining component is the exterior. There is only one infinite component: outside any box containing \(C\), nearest-neighbor vertices communicate, and every infinite component meets that region.

For an integer \(a\ge1\), range-\(a\) adjacency joins distinct torus vertices whose maximum distance is at most \(a\).

We will also use a basic counting bound. For each fixed range \(a\), there is a constant \(A_a\) such that the number of connected sets of \(m\) vertices containing a specified root is at most \(A_a^m\), on either \(\mathbb Z^3\) or the torus. To see this, choose deterministically a rooted spanning tree for each set and traverse it depth first. The traversal has \(2(m-1)\) steps, each chosen from a fixed finite set of possible displacements, and its visited vertices recover the set. Increasing \(A_a\) covers \(m=1\). Together with (77), this gives \[ \mathbb P(\text{a range-$a$ bad component has at least }m\text{ vertices}) \le K^3(A_ap)^m. \tag{91}\] A component of size at least \(m\) contains a connected subset of exactly \(m\) vertices, by growing a spanning tree one vertex at a time.

We have proved the two encounter bounds for paths that ignore the bad set. To use them, we will retain the skeleton vertices whenever possible and replace obstructed segments by short exterior routes. A size restriction guarantees the finite lifts needed for this construction; the endpoints must also lie outside the components’ filled interiors. The joint bad-set bound makes both requirements likely.

Fix \(a_1=R+2\). Reject the environment if it contains a range-\(a_1\) bad component of size at least \[m_K=\left\lfloor\frac{K}{10a_1}\right\rfloor.\] For large \(K\), every remaining bad \(*\)-component has finite periodic lifts, by Lemma 33. Reject also if either endpoint belongs to the projection of the fill of one of these components. The event on which neither rejection occurs is \(\mathcal E_{v,w}\).

If the fill of a lifted \(*\)-component of size \(m\) contains a lift of an endpoint, some root of the component lies within maximum distance \(m\) of that endpoint. This follows from the bounding-box assertion and the coordinate span in Lemma 33. There are at most \(C m^3\) possible roots modulo \(K\). Counting connected sets and using (77) thus yields \[ \mathbb P(\mathcal E_{v,w}^{c}) \le K^3(A_{a_1}p)^{m_K} +C\sum_{m\ge1}m^3(A_1p)^m. \tag{92}\] The constant includes both endpoints. First make \(p_0\) small enough that the series is at most \(1/4\), then make \(K_0\) large enough that the first term is at most \(1/4\) for \(p\le p_0\) and \(K\ge K_0\). This proves \(\mathbb P(\mathcal E_{v,w})\ge1/2\). We may decrease \(p_0\) further below.

Nearest-neighbor detours

Draw the skeleton of Section 8.1 independently of the datum. Its folding in Equation (81) fixes the final endpoint without conditioning the random process on a future value. We now adapt this nearest-neighbor walk to the bad set while keeping the endpoint rejection event fixed.

Figure 1 illustrates the replacement. The construction takes place in \(\mathbb Z^3\), where a finite obstacle has a well-defined exterior; projection and loop erasure are performed afterward.

On \(\mathcal E_{v,w}\), replace the visits of this lifted walk to bad components as follows. If it meets a lifted bad \(*\)-component \(C\), take its first and last visits to \(C\). The vertices immediately before and after these visits belong to \(\partial_*^{\rm ext}C\): the path from the first endpoint to the first such vertex misses \(C\), and the path from the last such vertex to the other endpoint misses \(C\); both endpoints are outside \(\operatorname{fill}(C)\). By Lemma 32, join these two shell vertices by a simple nearest-neighbor path in the shell, replacing the intervening part of the walk. The added vertices are all good. Each replacement removes at least one bad visit, and no replacement introduces a bad visit. The process therefore terminates after finitely many steps.

Every component treated in this procedure was met by the original nominal refinement: any remaining bad vertex still belongs to that original walk. Project the final walk to the torus and erase loops in chronological order. The result is a simple good nearest-neighbor path from \(v\) to \(w\). Every nonnominal vertex belongs to the shell of a bad \(*\)-component met by \(\Gamma\). All choices in the refinement, shell paths, and erasure can be made using fixed orderings. Thus the construction gives the measurable kernel in Proposition 30.

We now bound the encounters introduced by this construction. Use two independent nominal samples \(\Gamma,\Gamma'\) in the same environment, and let \(\pi,\pi'\) be their final simple paths. Let \(H\) range over the range-\(a_1\) bad components on the torus. Fix \(C_R=52(2R+1)^3\), which also exceeds \(5(2R+1)\) in Equation (90). On \(\mathcal E_{v,w}\), \[\begin{align*} J_R(\pi,\pi') &\le J_R(\Gamma,\Gamma')\\ &\quad+C_R\sum_H |H| \mathbf 1_{\{d_\infty(H,\Gamma)\le a_1,\, d_\infty(H,\Gamma')\le a_1\}}. \tag{93}\end{align*}\] For nominal walks, \(J_R\) here counts vertex occurrences, which only increases the bound.

To prove [lattice:detour-charge], first count encounters where both vertices are nominal. These are bounded by the first term. If a nonnominal vertex belongs to the shell of \(C\) and encounters a nominal vertex of the other walk, then \(C\) is within distance \(R+1\le a_1\) of that other walk, and \(C\) meets its own nominal walk. If two nonnominal vertices belong to shells of \(C,C'\), then \(d_\infty(C,C')\le R+2\le a_1\), so both components belong to one range-\(a_1\) component \(H\) meeting both nominal walks. Charge each such encounter to one of its nonnominal vertices and to this \(H\). There are at most \(26|H|\) possible added vertices associated to the \(*\)-components inside \(H\), even if several lifted copies were used: projection can only decrease this number. Each such vertex encounters at most \((2R+1)^3\) vertices of the other simple path. Charging from either path costs at most an additional factor two. This proves the claimed bound.

Averaging the environment and applying both moments

Fix both complete nominal paths. Their independence from \(\mathcal D\) leaves (77) available for any prescribed collection of bad vertices. Expand the exponential of the second term in [lattice:detour-charge] as a product over the actual range-\(a_1\) components. A term corresponding to distinct components has disjoint vertex sets. Drop maximality, sum over all disjoint connected candidate sets, and apply (77). Finally drop the disjointness restriction and use \(1+x\le e^x\). The resulting bound is \[\begin{align*} &\mathbb E_{\mathcal D}\left[ \mathbf 1_{\mathcal E_{v,w}} \exp\left(\kappa C_R\sum_H|H| \mathbf 1_{\{d_\infty(H,\Gamma),d_\infty(H,\Gamma')\le a_1\}}\right) \right]\\ &\qquad\le \exp\left(\sum_F (p e^{\kappa C_R})^{|F|} \mathbf 1_{\{d_\infty(F,\Gamma),d_\infty(F,\Gamma')\le a_1\}} \right), \tag{94}\end{align*}\] where \(F\) ranges over all nonempty range-\(a_1\) connected torus sets. The factor \(e^{\kappa C_R|F|}-1\) from the expansion was bounded above by \(e^{\kappa C_R|F|}\). Thus only joint bad-set probabilities were used; there is no independence assumption on the environment.

We bound the exponent by the soft-distance statistic in Equation (84). If a contributing set \(F\) has size \(m\), choose an occurrence \(z\in\Gamma\) within distance \(a_1\) of a root of \(F\). There are at most \((2a_1+1)^3\) root choices for each \(z\), and at most \(A_{a_1}^m\) connected sets at each root. A spanning-tree path in \(F\) has at most \(m-1\) edges, each of length at most \(a_1\) in the periodic maximum metric. Since \(F\) is also within \(a_1\) of \(\Gamma'\), the triangle inequality gives \[d_\infty(z,\Gamma')\le 2a_1+a_1(m-1)=a_1(m+1).\] This argument applies even to wrapping candidate sets; only the actual components used for detours required the earlier lift and rejection test. Absorb the root choices into a constant \(A_R\ge1\). The exponent in Equation [lattice:environment-expansion] is at most \[ \sum_{z\in\Gamma}\sum_{m\ge1}q^m \mathbf 1_{\{d_\infty(z,\Gamma')\le a_1(m+1)\}}, \qquad q=A_Rp e^{\kappa C_R}. \tag{95}\] All constants here depend only on the fixed \(R\). Counting the same set more than once only increases this nonnegative upper bound.

Require \(q\le e^{-2}\). If \(d\le a_1(m+1)\), split \(q^m\) into two equal powers and use \[q^m=q^{m/2}q^{m/2}\le q^{m/2}e^{-m} \le e\,q^{m/2}e^{-d/a_1}.\] Summing the first factor over \(m\ge1\) proves \[ \sum_{m\ge1}q^m\mathbf 1_{\{d\le a_1(m+1)\}} \le\eta(p,\kappa)e^{-d/a_1}, \qquad \eta(p,\kappa)=\frac{e\sqrt q}{1-\sqrt q}. \tag{96}\] In particular \(\eta(p,\kappa)\to0\) as \(p\to0\) at fixed \(\kappa\). Set \(B=a_1\). Equations [lattice:detour-charge], (90), and [lattice:environment-expansion]–(96) give \[ \mathbb E_{\mathcal D}\left[ \mathbf 1_{\mathcal E_{v,w}}e^{\kappa J_R(\pi,\pi')} \mid\Gamma,\Gamma'\right] \le\exp\left(\kappa C_RJ_{\rm occ}^{(R)}+ \eta(p,\kappa)S_B(\Gamma,\Gamma')\right). \tag{97}\] On the left, the adapted paths are used only on \(\mathcal E_{v,w}\). The environment was averaged once, with both entire skeletons fixed.

First choose \(\kappa>0\) with \(2\kappa C_R\le\alpha_R\), where \(\alpha_R=c_{\rm hit}/(1+R)^2\). Next choose \(p_0>0\) so small that \(q\le e^{-2}\) and \(2\eta(p,\kappa)\le\xi(B)\) for \(p\le p_0\), as well as the earlier endpoint rejection requirements. The constants \(K_0\) can then be enlarged to cover those rejection estimates. Cauchy–Schwarz and both moments in Lemma 31 imply \[\begin{align*} \mathbb E\exp\left(\kappa C_RJ_{\rm occ}^{(R)}+\eta S_B\right) &\le \left(\mathbb Ee^{2\kappa C_RJ_{\rm occ}^{(R)}}\right)^{1/2} \left(\mathbb Ee^{2\eta S_B}\right)^{1/2}\\ &\le\sqrt{C_{\rm hit}C(B)}=:C_{\rm path}<\infty. \end{align*}\] Together with Equation (97), this proves the annealed bound (79). Both path draws use one common datum and independent skeleton seeds. The event retains its original mass; there is no renormalization by conditioning on acceptance and no assertion of a bound for each fixed environment.

Finally, for \(K\ge80\) the interval \([\lceil K/10\rceil,\lfloor K/8\rfloor]\) contains at least \(K/40-1\ge K/80\) integers. For each such \(n\), there are \((2n+1)^2\ge K^2/25\) transverse choices. They are distinct modulo \(K\), since \(2n<K\). Multiplying by the \(K^3\) choices of starting vertex gives at least \(K^6/2000=\upsilon K^6\) admissible ordered pairs. This completes Proposition 30.

Affinity and a common finite measure

For finite nonnegative measures \(P,Q\) on the same measurable space, define their affinity by \[\mathop{\mathrm{Aff}}(P,Q)=\int\sqrt{pq}\,\mathrm d\xi, \qquad p=\frac{\,\mathrm dP}{\,\mathrm d\xi},\quad q=\frac{\,\mathrm dQ}{\,\mathrm d\xi}, \quad \xi=P+Q.\] Using another dominating measure gives the same value. We will use three elementary properties. If \(P\ge P'\) and \(Q\ge Q'\), then \(\mathop{\mathrm{Aff}}(P,Q)\ge\mathop{\mathrm{Aff}}(P',Q')\). For finite lists of measure pairs, \[ \mathop{\mathrm{Aff}}\left(\sum_jP_j,\sum_jQ_j\right) \ge\sum_j\mathop{\mathrm{Aff}}(P_j,Q_j). \tag{98}\] Indeed, pointwise Cauchy–Schwarz gives \(\sum_j\sqrt{p_jq_j}\le\sqrt{(\sum_jp_j)(\sum_jq_j)}\). Finally, applying the same probability kernel to both measures cannot decrease affinity. To see this, form the joint measures with that kernel and then condition a common dominating measure on the output. Conditional Cauchy–Schwarz gives \(\mathbb E(\sqrt{pq}\mid\text{output})\le \sqrt{\mathbb E(p\mid\text{output})\mathbb E(q\mid\text{output})}\). Integration proves the assertion. Projection is a special case.

Cell measures and disjoint groups of tags

Recall \(V=K^3\), \(D=N/V\), and the unit cells \(B_v\), each of volume one. Write \(X'=(x_2,\ldots,x_N)\) for the ordered bath. For ordered cells \(v,w\), define finite measures on \((x,y,X',W')\in B_v\times B_w\times\Lambda_K^{N-1}\times\Lambda_K^N\) by \[ \begin{aligned} \,\mathrm dP_{vw}=V\Phi(x,X',W')^2\,\mathrm dx\,\mathrm dy\,\mathrm dX'\,\mathrm dW', \\ \,\mathrm dQ_{vw}=V\Phi(y,X',W')^2\,\mathrm dx\,\mathrm dy\,\mathrm dX'\,\mathrm dW'. \end{aligned} \tag{99}\] Nonnegativity of \(\Phi\) and the occupation formula in Proposition 14 give the exact identity \[ B_{\rm occ}=\frac1{V^2}\sum_{v,w}\mathop{\mathrm{Aff}}(P_{vw},Q_{vw}). \tag{100}\]

Fix a group index \(1\le g\le G_D:=\lfloor\ell D/(4M)\rfloor\) from Section 7. Its exposed data are \(\mathcal B\), its unexposed label set is \(\mathcal I\), and its conditional path law is \(\lambda_{\mathcal I}\) from Lemma 27. Define measures \(\widehat P_g,\widehat Q_g\) on \((\mathcal B,x,y,X')\); the data \(\mathcal B\) already include \(W'\). For \(\widehat P_g\), sample the data and the conditional unexposed paths, and sum the following contributions over all \(i\in\mathcal I\): take \(x=\omega_i(t)\), restrict to \(x\in B_v\), order the remaining \(N-1\) midpoints by a fresh uniform permutation to form \(X'\), and sample \(y\) uniformly in \(B_w\). For \(\widehat Q_g\), take the tagged midpoint as \(y\in B_w\) and sample the extra point \(x\) uniformly in \(B_v\). The use of a sum, rather than a uniformly chosen tag, fixes their normalization.

The remaining task is to find, for each retained group and each of many ordered cell pairs, a common measure of mass at least \(1/2\) whose squared likelihood integrals against \(\widehat P_g\) and \(\widehat Q_g\) are bounded by one constant \(C_2\). Lemma 34 would then give affinity at least \(1/(4C_2)\) per group. The factor \(1/D\) in Equation (101) can be paid because the number of disjoint groups is proportional to \(D\).

Two midpoint assignments with the same observed bath

Take \(R=30\) in Proposition 30, and fix an admissible ordered cell pair \(v,w\): its lift displacement \((n,d_2,d_3)\) satisfies \(\lceil K/10\rceil\le n\le\lfloor K/8\rfloor\) and \(|d_i|\le n\). Choose the good-site parameters of Proposition 28 to meet the bad-set hypothesis of Proposition 30. Let \(\mathcal E_{vw}\) be the data-measurable event supplied by Proposition 30, of probability at least \(1/2\). On this event draw a simple nearest-neighbor path \[z_0=v,z_1,\ldots,z_d=w\] through good sites. For each \(k<d\), independently choose a uniform accessible label \(i_k\) anchored at \(z_k\). The choices inspect only \(\mathcal B\) and the lattice path. In particular, they do not inspect any latent trajectory. The selected labels are distinct because their anchors are distinct.

We construct two path configurations that share their observed \((x,y,X',W')\). Keep the exposed data fixed. First sample all unselected unexposed trajectories from their exact marginal under \(\lambda_{\mathcal I}\), and use them in both copies. For every vertex \(z_k\), prepare a factor as follows. The first copy needs label \(i_k\) through this cell if \(k<d\), and the second copy needs label \(i_{k-1}\) through it if \(k>0\). Intersect the corresponding good-target sets \(T_{i_k}(z_k)\) and \(T_{i_{k-1}}(z_k)\) from Section 7, using only the one required set at an endpoint. The intersection, denoted by \(A_k\), has volume at least \(0.98\). Sample \(U_k\) uniformly in \(A_k\), and then independently sample the one or two required bridge trials through \(U_k\), each conditioned on its individual success against the frozen paths. All \(d+1\) vertex factors are independent before the additional conditioning below. Figure 2 shows the two midpoint assignments.

Use \(U_d\) as the extra point in the first copy and \(U_0\) as the extra point in the second copy. Impose all remaining hard-avoidance checks in both copies: selected paths must avoid the unselected unexposed paths and one another within their respective copies. Condition the product of vertex factors on these checks, separately for each fixed collection of unselected paths. The sampled unselected-path marginal therefore remains its original marginal under \(\lambda_{\mathcal I}\). More explicitly, let \(\lambda_{\rm out}\) be that marginal, let \(F_k\) be the probability law of the \(k\)th vertex factor, and let \(J\) be the indicator of the remaining checks in both copies. The joint law just defined is \[ \lambda_{\rm out}(\,\mathrm d\omega_{\rm out})\, \frac{J(\omega_{\rm out},\xi_0,\ldots,\xi_d) \prod_{k=0}^d F_k(\,\mathrm d\xi_k)} {\displaystyle\int J(\omega_{\rm out},\xi_0,\ldots,\xi_d) \prod_{k=0}^d F_k(\,\mathrm d\xi_k)}. \tag{102}\] The denominator is a function of the fixed outside paths. Integrating the second factor gives one for each such configuration. A single normalization after integrating the outside paths would change their marginal and would not yield the comparison used below. Each \(F_k\) depends only on the data, route and selected labels, so it is fixed before those outside paths are sampled.

We verify that this conditional construction is defined. A vertex factor carries at most two paths, each with a marginal of the form \(\Pi_i^{A_k}\) in Proposition 29. Its paths are confined within distance ten of their anchors, and there are at most \(M\) unexposed labels per anchor. Consequently each factor has at most \(C_{\rm col}M\) possible opponents in the two copies, for a fixed geometric constant \(C_{\rm col}\). All opponents have distinct labels within the copy in which a check is imposed. The deterministic-opponent estimate, summed over those checks, gives \[ \chi_D=C_{\rm col}M e_D\longrightarrow0 \qquad(D\longrightarrow\infty,\ M\text{ fixed}). \tag{103}\] For any fixed regular and confined values of the other paths with their recorded endpoints, the factor passes every incident check with probability at least \(1-\chi_D\). This statement averages its common midpoint over \(A_k\); it makes no claim at a prescribed midpoint. It uses the two path marginals and a union bound, so no independence of the paths within the factor is required. Inserting the \(d+1\) factors successively now bounds the two-copy conditioning probability below by \((1-\chi_D)^{d+1}>0\) for sufficiently large \(D\).

Tag \(i_0\) in the first copy and \(i_{d-1}\) in the second. In each copy the tag and the extra point then give \(x=U_0\), \(y=U_d\). The selected bath midpoints in both copies are exactly \(U_1,\ldots,U_{d-1}\); the unselected midpoints also agree. Choose a common uniform ordering of the shared midpoint instances; their physical labels in the two copies may differ. In each copy separately, this has the uniform ordering law determined by its paths and its tag. This defines a single finite measure \(\widehat\nu\) on \((\mathcal B,x,y,X')\) after averaging the data, routes and labels, with zero mass off \(\mathcal E_{vw}\). Each conditional sampling law on this event is a probability measure, so \[ \widehat\nu(\text{all})=\mathbb P(\mathcal E_{vw})\ge\frac12. \tag{104}\] These are measurable probability kernels: the route and label choices are finite, the target sets are measurable functions of the data, and all path restrictions are Borel subsets of the continuous-path spaces. The positive normalizers just proved permit the displayed conditioning.

Cancellation of conditional normalizers

The midpoint construction has two path copies in each internal vertex factor. To estimate its likelihood, designate one copy as primary and regard the other as auxiliary. At an internal vertex \(z_k\), \(1\le k<d\), the primary path has label \(i_k\) in the first-copy view, whereas the auxiliary path has label \(i_{k-1}\). Thus deleting a factor is not the same operation as deleting all instances of one particle label. The following lemma keeps this distinction explicit and isolates the normalizers that cancel when two routes are far apart. Its coordinates and factors are abstract; we identify them with the midpoint construction immediately after the proof. The two changes arise because the square of a route-averaged likelihood expands into a product for two independent route choices at the same exposed datum.

The next lemma, from OpenAI (2026b, Lemma 8.3), concerns finitely many coordinates in standard Borel spaces, each with a probability reference \(P_i\). All auxiliary spaces below are standard Borel as well. A check will mean an indicator imposing a constraint on one or two coordinates. The joint reference law \(\lambda\) is the product \(\bigotimes_iP_i\) conditioned on a finite collection of checks. An additional independent coordinate is allowed; it simply has no checks.

A change indexed by a set \(S\) leaves the marginal outside \(S\) unchanged. Inside \(S\), it starts from independent factors \(\Pi_{S,i}\), \(i\in S\). Each factor includes a primary coordinate in the space of \(P_i\) and possibly auxiliary coordinates. Its primary marginal is \(g_{S,i}P_i\), with \[ 0\le g_{S,i}\le G, \qquad \int g_{S,i}\,\mathrm dP_i=1. \tag{105}\] The factors are fixed before the outside coordinates are sampled. The product is conditioned on specified checks, including every reference check involving the primary coordinates in \(S\). Checks involving only fixed outside coordinates are already satisfied almost surely under the unchanged outside marginal; otherwise the conditional proposal would not be defined there. Omit these redundant checks. Every remaining proposal check therefore involves a coordinate carried by a changed factor. Auxiliary coordinates are then forgotten. The resulting primary likelihood relative to \(\lambda\) is denoted by \(L_S\).

For each primary and auxiliary coordinate, fix a measurable allowed set on which all its relevant reference and proposal marginals are concentrated. These sets, like the proposal factors, are fixed before sampling outside coordinates. A configuration is individually permitted when each coordinate lies in its allowed set; this imposes no pairwise checks. The compatibility hypothesis below is uniform on these sets, including configurations that fail some pairwise checks.

We make explicit the deletion convention for this construction. When some factors are removed, remove their coordinates and all checks incident to them. Do not replace a removed auxiliary coordinate by an original reference coordinate. Coordinates fixed outside the sets under discussion remain as obstacles in all the checks in which they occur. Coordinates here are path instances in a specified copy. If an auxiliary with label \(j\) belongs to a retained factor, it remains integrated in that factor even when a different factor carrying the primary label \(j\) is deleted. It is never replaced by the original path with label \(j\).

The likelihood cost is confined to encounters

Fix the data, the route and the selected labels. Regard either copy as the primary one. The reference for that copy is \(\lambda_{\mathcal I}\otimes P_*\), where \(P_*\) is the uniform law of the extra point in its endpoint cell. Let \[S=\{i_0,\ldots,i_{d-1}\}\cup\{*\}.\] In Lemma 36, a primary coordinate is the chosen copy’s path or endpoint extra point. Its auxiliary coordinates are the other copy’s path or extra point through the same midpoint. The checks are the collision exclusions within each copy; there is no collision check between paths in different copies. Index a vertex factor by its primary label, using \(*\) for the extra point; its center is its midpoint cell \(z_k\). The two paths in one factor may have different labels, and each copy contributes at most one path. The allowed set for each path consists of the regular, confined, frozen-avoiding paths with its own recorded endpoints. Each extra point lies in its target cell. These are individual restrictions; the remaining collision checks still couple different factors.

By Proposition 29, the primary marginal of each path factor has density at most \(G\) relative to \(P_i\), and integrates to one. For the extra point the density is \(\mathbf 1_{A_k}/|A_k|\) relative to \(P_*\), which is at most \(1/0.98\). Enlarge the fixed \(G\) to be at least two, covering this factor as well. These marginal densities and their auxiliary kernels depend on the exposed data and the route and label choices; they do not depend on the unselected unexposed paths.

The union bound proving Equation (103) verifies hypothesis (i) for each proposal factor. The same argument with \(P_i\) in place of \(\Pi_i^{A_k}\) verifies it for insertion of a selected reference path, by Proposition 29. The reference extra point has no checks. These estimates are uniform over all individually permitted opponent paths, whether or not their labels are accessible, and deleting checks can only improve them. Thus the bound remains available for every reduced normalizer in Lemma 36.

Take two independent route and label choices at the same data and endpoint pair, and denote their selected index sets by \(S,T\). For the chosen primary side, declare a factor of \(S\) near if its center is at lattice supremum distance at most \(R\) from some center of \(T\), and declare every other factor far. Define \(C_S,F_S,C_T,F_T\) accordingly. A shared real label has centers at distance at most two in the two assignments, so it is near; the shared extra index has the same endpoint center. Consequently the far index sets are disjoint from the opposing lists.

All paths carried by a factor lie within distance eleven of its center. The original path of an opposing real label also lies within distance eleven of that opposing factor’s center. Since \(R=30\), far factors cannot interact with any coordinate carried by the opposite list or with those original paths. This includes the auxiliary-copy paths. Far sets therefore meet the separation assumptions of Lemma 36.

For clarity, a reduced far proposal retains exactly the paths carried by its far vertex factors and the fixed paths outside \(S\cup T\). It deletes the omitted near factors in both copies. It does not put their original trajectories back as unselected obstacles. With this convention all the normalizers in (108)–(111) are the ones arising from the present construction.

Write \(L_S,L_T\) for the two primary likelihoods. If \[J_R=\#\{(j,k):d_\infty(z_j,z'_k)\le R\},\] then \(|C_S|+|C_T|\le2J_R\). Lemma 36 gives, at the fixed data, \[ \int L_SL_T\,\mathrm d(\lambda_{\mathcal I}\otimes P_*) \le G^{|S\cap T|}(1-\chi_D)^{-4J_R}. \tag{112}\] In particular, no factor is paid for a long portion of one route that stays away from the other.

Averaging labels and forgetting the paths

Condition on the data and the two lattice paths before choosing their labels. Each common departure cell has at least \(M/2\) accessible labels. The two uniform choices at that cell match with probability at most \(2/M\), and the match events are independent between distinct common cells. Real labels anchored at different cells cannot agree. The shared extra point contributes one factor \(G\), so \[ \mathbb E_{\mathrm{labels}}G^{|S\cap T|} \le G\exp\left(\frac{2(G-1)}M J_R\right). \tag{113}\] Choose the fixed integer \(M\) sufficiently large for the good-site supply and for \[ \frac{2(G-1)}M\le\frac\kappa2. \tag{114}\] Then increase \(D_*\) so that, for every \(D\ge D_*\) in the allowed \(\alpha\) window, all earlier estimates hold and \[ -4\log(1-\chi_D)\le\frac\kappa2, \qquad \frac{G_D}{D}\ge\frac\ell{8M}. \tag{115}\] The first requirement is possible by (103); the second follows once \(\ell D/(4M)\ge2\). These choices do not change \(G\), \(\kappa\), or \(C_{\mathrm{path}}\).

The following use of an averaged likelihood and a two-route second moment also occurs in the point-reassignment argument of Peres and Sly (Peres and Sly 2014, Proposition 2.1). Here Lemma 36 supplies the additional conditional-normalizer estimate required by the hard-core path law.

Let \(\overline L\) be the likelihood averaged over the conditional route and label choices, with value zero off \(\mathcal E_{vw}\). Tonelli’s theorem expresses its square integral using two independent such choices. Combining (112)–(115) and the annealed encounter bound in Proposition 30 gives \[ \mathbb E_{\mathcal B}\int\overline L^{2} \,\mathrm d(\lambda_{\mathcal I}\otimes P_*) \le G\mathbb E\bigl[\mathbf 1_{\mathcal E_{vw}}e^{\kappa J_R}\bigr] \le C_2, \qquad C_2:=G C_{\mathrm{path}}. \tag{116}\] Here the two route randomizations share the same data; the expectation over the data is taken only once. The event is not conditioned to have probability one. Its indicator is part of both likelihoods, and its square is itself. The calculation applies separately with either copy primary, with the same constant \(C_2\).

We next check carefully that tagging and observing the bath do not increase this bound. At fixed data, split \(\overline L=\sum_{i\in\mathcal I}f_i\), where \(f_i\) contains exactly the choices designating \(i\) as the primary tag. The functions are nonnegative. In the first copy \(f_i\) is supported where \(\omega_i(t)\in B_v\); in the second it is supported where \(\omega_i(t)\in B_w\). Since \[\sum_i f_i^2\le\left(\sum_i f_i\right)^2,\] the measure that retains the tag index has squared likelihood integral at most \(C_2\) relative to the sum of the tag-restricted reference measures on the disjoint copies indexed by \(i\). Now apply the observation kernel that orders the bath and retains \(\mathcal B,x,y,X'\), and forget the tag and all the paths. If a finite measure has density \(f\) relative to a reference \(P\), the density after applying a common kernel is the conditional average of \(f\) in the corresponding joint reference measure. Conditional Cauchy–Schwarz bounds its squared integral by \(\int f^2\,\mathrm dP\). This remains valid for finite reference measures, by normalization when their mass is nonzero.

For either primary copy, the resulting measure is the common observed \(\widehat\nu\) already constructed. Its corresponding reference is precisely \(\widehat P_g\) or \(\widehat Q_g\). We have proved \[ \int\left(\frac{\,\mathrm d\widehat\nu}{\,\mathrm d\widehat P_g}\right)^2 \,\mathrm d\widehat P_g\le C_2, \qquad \int\left(\frac{\,\mathrm d\widehat\nu}{\,\mathrm d\widehat Q_g}\right)^2 \,\mathrm d\widehat Q_g\le C_2. \tag{117}\] Together with (104), Lemma 34 now gives \[ \mathop{\mathrm{Aff}}(\widehat P_g,\widehat Q_g)\ge\frac1{4C_2}. \tag{118}\] This lower bound is uniform in the group index and in every admissible ordered pair of cells.

The remaining step is the return to fixed physical density and temperature.