R87/G02 working theorem 2 — quantitative classical input, proof program and dependencies
Status: derivation in progress, NOT a certified theorem yet. This file distinguishes exact imported statements, derived extensions, and interfaces still being checked.

Temperature conversion: the frozen H0 uses coupling1/4, so the standard Ising inverse coupling is b=beta/4 and b_c=(1/2)log(1+sqrt2). The FK parameter is p=1-exp(-2b)=1-exp(-beta/2). On beta in [beta_min,beta_c], p_c-p is comparable, by fixed positive constants, to delta=beta_c-beta. Every later power refers to this conversion.

Imported inputs:
(A) Lubetzky–Sly, arXiv:1001.1613v4, Theorems3.1,3.2 and4.2: critical rectangular heat-bath gaps are bounded below by c r^{-C_*}, uniformly in fixed boundary spins, with r the smaller side; free/periodic bounded-aspect cases are included separately. Their proof of the spatial coupling uses an upper bound below1 for fully-wired critical FK crossing (Section3.2), not a lower crossing bound.
(B) Duminil-Copin–Garban–Pete, arXiv:1111.0144, Theorem1.2 and Lemma2.13: for p<p_c there is a scale ell(p)<=C(p_c-p)^{-1}log[1/(p_c-p)] at which fully-wired crossing probabilities decay exponentially on dyadic larger rectangles. A conservative polynomial upper bound ell<=C max(1,delta^{-2}) is enough here. The source's exact finite-size criterion is used, not an unproved identification of infinite-volume two-point correlation length with uniform-boundary mixing.

Derived extension to audit:
The arbitrary-boundary coupling in (A) is valid for every p; its critical spatial-mixing estimate uses only an upper bound on wired crossing. By stochastic monotonicity in p, the same upper bound holds for p<=p_c. The recursive gap proof then yields the same polynomial local gap exponent C_* throughout beta<=beta_c. This is a proof-level extension, not a claim that the spectral gap itself is monotone under arbitrary boundary conditions. Check each place in the recursion where criticality was used before adopting this extension.

Boundary-marginal estimate:
A physical FK path from an interior site u to the outer boundary must cross an annulus lying inside the domain. Cover such an annulus by a fixed number of bounded-aspect rectangles; boundary-condition domination and (B) bound its probability by C exp[-dist(u,boundary)/(C ell)]. The mixed-spin-boundary FK coupling of (A) is dominated by the wired exploration; agreement holds outside the explored components. A union bound over C=partial^+ A then gives TV of the C marginal at most C0 |C| exp[-buffer/(C1 ell)]. Boundary wirings must not be counted as physical paths. This supplies the input to work-01 without claiming a boundary-size-free estimate for arbitrarily large observables.

Proposed uniform global-gap recursion:
For a bounded-aspect rectangle of side scale R, split the longer side into two overlapping rectangles with overlap width2w(R), where w(R)=K ell log(R+2). Average over cuts whose centers range in the middle third. Every site is covered once plus an average overlap at most Cw/R. A fully-wired FK component crossing the overlap has probability at most eta_R=C R^2 exp[-w/(C ell)]. Choose K so eta_R<=R^{-4}.
The two-block heat-bath chain then has continuous-time gap at least1-eta_R, by the same repeated-coupling argument as (A), not merely a two-step Doeblin bound bounded away from1. Comparing block variance with single-site Dirichlet forms gives
 lambda(R)^{-1} <= [(1+C w(R)/R)/(1-eta_R)] max_child lambda(child)^{-1}.   (1)
Two recursive splits reduce the maximal side by a fixed factor. Stop at R0=C ell[1+log(ell+2)]^2. The product of factors in(1) is uniformly bounded because sum_scales ell log R/R is finite and bounded at this cutoff. The critical uniform local-gap estimate on the final blocks would then imply lambda_cl>=c R0^{-C_*}, polynomial in delta, uniformly in volume. For a torus, first use two overlapping periodic slabs and then cut the remaining periodic direction; charge both overlap strips and use the periodic finite-size base case.

Unfinished checks: precise averaged-cut coverage near rounding endpoints; two-block contraction approaching1 rather than a constant; torus/cylinder FK exploration; extension of all critical proof steps to p<=p_c. This remains a working proof until those checks are explicit. Even success supplies only the reference parent gap, not finite-g stability or preparation complexity.
