6fbd3ac b34550f f0945ea 654c66f
================================================================================
MARKED POLYGON CORRELATIONS AND ONE-ARC BOUNDS
A self-contained proof, rewritten for clarity
================================================================================

ABSTRACT
--------

At the critical honeycomb vertex activity rho_v = 1/sqrt(2 + sqrt 2), the
squared-length mass of simple polygons of diameter at most H, counted
modulo translations, is at most C H^(2/3 + eta) for every eta > 0.
Quantitative two-mark cylinder correlations are proved along the way, and
a polynomial one-arc bound holds even for arbitrarily unequal marked
cylinder intervals.

--------------------------------------------------------------------------------
OVERVIEW
--------------------------------------------------------------------------------

The main objects are:

  - A honeycomb lattice. Polygons are simple cycles, counted modulo
    translation, without orientation or basepoint.

  - The critical vertex weight, rho_v = 1 / sqrt(2 + sqrt 2). Nienhuis
    found this value by the O(n) loop model at n = 1 (1982); Duminil-Copin
    and Smirnov proved it rigorously (Annals 175, 2012).

  - The two-port cylinder correlation C(p,p') of polygons passing through
    both marked ports p and p'.

  - The one-arc cylinder weight A(p,p') of a single self-avoiding arc
    from p to p'.

Everything is upper estimates: a positive lattice sum is compared
to an exactly normalized contour integral, and the contour integral is
bounded by an explicit sum over finitely many particles.

The four proof stages:

  STAGE 1. Finite identity (Sections 2-4). Section 3 rewrites C(p,p')
  as a finite spin contraction, a finite sum over spin labels of an
  amplitude U_N times its star U_N^*. Section 4 turns that sum into a
  contour integral, normalized exactly by the vacuum polynomial h_N.

  STAGE 2. Uniform denominator (Section 5).

      log | h_N~^2 / ((gamma/2)^N prod_{i<j} H_*(a_i-a_j)^2) |
            >=  (5/24 - o(1)) log N,

  uniformly in the two height multiplicities. This clears Stage 1.

  STAGE 3. Positive mean and coercivity (Section 6). One main contour
  (the X line) is deformed to a curved level set on which the centering
  density is real and positive. There, the real interaction dominates a
  weighted Sobolev norm of every species and the L^2 norm of the total
  primitive.

  STAGE 4. Trial fields and assembly (Sections 7-9). Explicit trial
  fields gain 2 L_X on the common interval and bound shoulder activity.
  The reference-law Hessian determinant is computed; the trial fields
  are transported by small particle motions; the sector integral is
  bounded; the sharp two-mark estimate and the polygon-moment theorem
  follow. Section 10 proves the (coarser) one-arc bound with real
  integration only.

Notation is standard. Contours are oriented counter-clockwise unless
indicated. Every sum over configurations is finite when used, and every
infinite series is absolutely convergent. The reader is expected to
know basic complex analysis (residues, contour deformation), linear
algebra (Pfaffians, eigenvalues), and Sobolev norms of one real variable.

================================================================================
1. SETTING AND MAIN RESULTS
================================================================================

1.1 The honeycomb lattice.
--------------------------

Let T be the regular triangular tiling of the plane with side length 1,
and HH its dual honeycomb graph: vertices of HH are centroids of
triangular faces, edges of HH cross edges of T at right angles, degree
3 at every vertex.

Every edge of HH crosses exactly one edge of T at its midpoint, so the
following two descriptions of "visiting points" agree:

  - (honeycomb) pick a vertex of HH;
  - (dual) pick the midpoint of a triangular edge of T.

We use "vertex" for a honeycomb vertex, and "port" for a triangular
edge midpoint (the midpoint of a honeycomb edge, the natural entry and
exit of a path composed of hexagonal mid-edges).

Translation lattice. The translation group G of T is isomorphic to Z^2
and acts on HH with two orbits (the two honeycomb vertex colours, black
and white). Polygons are counted modulo G, so both colours survive.

1.2 Polygons and their weight.
------------------------------

A polygon P is a simple cycle in HH, with no orientation and no
distinguished basepoint. Its length |P| is its number of vertices. Its
weight is

    rho_v^{|P|},    rho_v = 1 / sqrt(2 + sqrt 2).

Diam(P) is the Euclidean diameter in the fixed embedding. It is the
geometric diameter; not a graph diameter. This matters, because a
polygon can have many vertices inside a small Euclidean disk.

1.3 The polygon-moment theorem.
-------------------------------

THEOREM 1.1. For every eta > 0 there is C_eta < infinity such that,
for every H >= 1,

    sum_{ [P] : diam P <= H } rho_v^{|P|} |P|^2  <=  C_eta H^{2/3 + eta}.

The sum is over translations classes [P] of simple unoriented polygons
with Euclidean diameter <= H.

Interpretation. A bound on the NUMBER of large polygons does not
suffice: many vertices can fit inside a small disk, and the weight
compensates but the |P|^2 factor does not. The natural observable that
"sees" |P|^2 is the number |P|(|P|-1) of ordered point pairs of P, i.e.
the two-port correlation C below.

1.4 The two-mark cylinder correlation.
--------------------------------------

Cut a honeycomb cylinder along a chain of ports in the cyclic order

    [ p, X, p', Y ],   |X| = s,  |Y| = b,  N = s + b + 2 even.

Here p, p' are marked ports (triangular edge midpoints); X and Y are the
ordinary sites on the two intervals. All ordinary Y sites have spectral
height zero; all ordinary X sites, and both marks, have height in
{0, beta}, where

    beta = pi/4,   gamma = pi / (3 beta) = 4/3.

The value gamma arises from the standard parafermionic normalization of
the honeycomb O(n) transfer matrix at n = 1 and appears throughout.

C(p,p') is the sum of the weights of individual cylinder polygons
visiting both marked ports, each polygon counted once, including when
it winds. Its exact normalization is fixed by the finite vacuum U_N
defined in Section 2. Let t be the fraction of X sites at upper height
beta, and set L_X = (log s)/gamma, L_Y = (log b)/gamma.

THEOREM 1.2 (sharp two-mark estimate). Fix c_1 in (0, 1] and a
sufficiently small c_4 > 0. Suppose

    c_1 L_Y <= L_X <= L_Y,

and suppose that either t = 1, or t in [1/2, 1) with s(1-t) >= exp(c_4 L_Y).
Then, uniformly as L_Y -> infinity,

    log C(p,p')  <=  -(4/3) log s + (617/1200) log(b/s) + o(log b).

The coefficient 617/1200 < 2/3 is the source of the 2/3 in Theorem 1.1.

1.5 The one-arc bound.
----------------------

A(p,p') is the critical vertex mass of a single self-avoiding cylinder
arc, entering p on its west half-edge, exiting p' on its east half-edge,
with all other marked half-edges vacant and no additional loops.

THEOREM 1.3. There are constants delta_1 > 0, L_* > 0, and C <
infinity such that

    A(p,p') <= b^C

whenever L_Y >= L_X >= L_*, s <= b, and at least 1/2 - delta_1 of the
ordinary X sites have height beta. The marks may each have either height
in {0, beta}. The ratio L_X / L_Y may tend to zero.

Theorem 1.3 is weaker than Theorem 1.2 and requires no sharp
determinant; it is proved in Section 10 with real integration only.

1.6 What we use from the companion paper.
-----------------------------------------

The companion, "Cylinder loop weights and planar nesting", supplies
the following inputs:

   (C1) Finite-vacuum identities:
        Yang-Baxter, unitarity, splitting R(j lambda) = S_j S_j^T for
        j = 2, 3, cyclic covariance, and reciprocity of h_N.

   (C2) The horizontal (electric) mean extraction and coercivity:
        template lemmas for smoothing, localization, source bounds,
        quadratic integration, and finite-rank transport.

   (C3) The planar diameter tail
            sum_{diam P > R} rho_v^{|P|} <= C (1 + R)^{-2}
        over translations classes of unrooted, unoriented polygons
        of vertex length (Electric, Theorem 10.5).

The present document adapts (C2)-(C3) to the magnetic setting, verifies
all hypotheses of the template lemmas, and adds the uniform denominator
bound of Section 5 and the sharp marked-pair estimate of Section 9.

================================================================================
2. THE FINITE HONEYCOMB CYLINDER
================================================================================

2.1 Why a finite model.
-----------------------

The polygon sum over an infinite lattice is infinite. The first step is
to work on a finite cylinder of circumference the row length N and to
make the vacuum (the empty boundary configuration) an explicit finite
object. Local Yang-Baxter and splitting identities let us later cut that
cylinder into the two marked rectangles used in the problem.

2.2 The vertex model.
---------------------

Set

    lambda = pi/8,   beta = 2 lambda = pi/4,   q = exp(i beta),
    k = q^3,         c = cos(3 lambda),        d = cos(2 lambda),
    C_0 = cos(lambda),                         gamma = pi / (3 beta) = 4/3.

A "slot" on a horizontal boundary line is a small open horizontal
segment. Slots are decorated by diagrams: a subset of occupied slots is
paired by non-crossing arcs (a "caps and cups" figure). An empty diagram
has coefficient one, a single vertical strand coefficient one, and all
composition of diagrams follows the standard gluing rules: matching
slots are joined, and any closed loop multiplies by zero (the O(n)
partition function at n = 1 suppresses loops).

The two-slot local operator R(v) has coefficients

    L(v) = sin(2 lambda + v) sin(3 lambda + v),
    A(v) = d sin(3 lambda - v) / L(v),
    U(v) = d sin v / L(v),
    B(v) = sin v sin(3 lambda - v) / L(v),
    E(v) = sin(3 lambda - v) sin(2 lambda - v) / L(v),
    F(v) = sin(v - lambda) sin v / L(v),

multiplying respectively a single vertical strand, a cap or cup, a
single diagonal strand, two vertical strands, and a cap-with-cup.
All R-boxes satisfy Yang-Baxter and unitarity; the square of R at
the special shift is the splitter:

    R(2 lambda) = S_2 S_2^T,    R(3 lambda) = S_3 S_3^T.

The splitter S_2 turns one slot into two: a vacancy becomes a vacancy
plus rho_v times a cup, and an occupied strand can take either output
with coefficient rho_v. The zero-to-two-slot map S_3 is a vacancy plus
a cup. These too are standard local diagrams; the reader can verify
that the composition S_2 S_2^T is R(2 lambda) by a two-line determinant
computation on the three-dimensional spin space of Section 3.

2.3 The normalized vacuum.
--------------------------

For a cyclic list of N spectral parameters u_1, ..., u_N put

    x_i = exp(2 i u_i),   sqrt(x_i) = exp(i u_i),
    D_0(x, y) = x^2 + y^2 + 2 d x y.

The physical heights are u_i in {lambda, 2 lambda}; after a shift, the
log coordinates a_i = 2 i u_i have imaginary part 0 or beta. Half of
that shift is later removed, hence "centered vacuum" below.

The uncentered matching vector V_N is the homogeneous polynomial in the
x_i defined by the sum over all disk-connected non-crossing matchings
of the N occupied slots, with the weight rho_v per vertex of the
resulting honeycomb polygon. Disk-connected means: compactify the
vacant open end to a point, and allow no strand to end there. This
retains ordinary non-crossing partial matchings, hence ordinary
winding polygons after gluing.

The normalization is

    U_N = V_N / h_N,
    h_N = prod_{i<j}  (D_0(x_i,x_j) / (x_i - x_j))
          * Pf[ (x_i^2 - x_j^2) / D_0(x_i,x_j) ],

with h_0 = h_1 = 1, and for odd N a last column of ones and its
negative transpose added to the Pfaffian matrix. The denominator h_N
is a polynomial in the x_i: the factors x_i - x_j cancel against
Vandermonde factors in the Pfaffian.

Per slot, the vacant part of V_N has degree at most N - 1, and the
occupied part is sqrt(x_i) times a polynomial of degree at most N - 2.

Convergence. At physical parameters u_i in {lambda, 2 lambda}, the
series with vacant far boundary converges absolutely. This is standard
(the transfer matrix has spectral radius < 1 at the critical point,
away from winding sectors). It is what allows diagram-by-diagram
manipulation below.

2.4 Cyclic covariance and reciprocity.
---------------------------------------

The vacuum U_N is cyclically covariant. It is also covariant under
reversing the row, with u_i replaced by 3 lambda - u_i. Explicitly:

    h_N(x_1^{-1}, ..., x_N^{-1})
        = h_N(x_1, ..., x_N) prod_i x_i^{-(N-1)}.

These identities are proved in the companion (Proposition 2.2,
Proposition 2.6) and are rational identities: they extend to coinciding
or complex parameters by continuation at regular coincidences.

2.5 The centered vacuum and its scalar reduction.
--------------------------------------------------

Anticipating Section 4, define the centered scalar

    h~_j(x_1, ..., x_j) = h_j(x_1, ..., x_j) * prod_{i=1}^j x_i^{-(j-1)/2}.

For a spectator list Z of length j - 2, the two scalar reductions used
in Section 4 are

    h~_j(Z, q^{-1} x, q x) / h~_{j-1}(Z, x)
        = 2 d * prod_{z in Z} (z + x) / sqrt(z x),                     (2.1)

    h~_j(Z, x, y) / h~_{j-2}(Z)
        = 2 c * prod_{z in Z} ((z - q^{-3} x) (z - q^6 x)) / (z sqrt(xy)),
                                                                       (2.2)

      where y = q^3 x.

The uncentered factors are (q^{-1} + q) x * prod(z + x) and
(x + y) * prod(z - q^{-3} x)(z - q^6 x); centering uses
x + y = 2 c sqrt(x y). The right-hand sides are equalities first where
the scalar quotients are defined, and then by polynomial continuation as
cleared identities (multiply both sides by the products in the
denominators).

================================================================================
3. THE SPIN CONTRACTION: SELECTING ONE POLYGON
================================================================================

3.1 The three-dimensional spin space.
-------------------------------------

Introduce a three-dimensional complex vector space with basis indexed by
the values h in {0, +1, -1}, where 0 stands for a vacancy and +1, -1
carry spin. An ordered cup or cap (bend that returns) has coefficient
k^h on the spins (h, -h) for h in {+1, -1}, and a straight strand
preserves its spin. The composition rule is ordinary matrix
multiplication of these spin representations:

    two consecutive bends:  k^h * k^{-h} = 1,
    closed unmarked loop:   k^{+2} + k^{-2} = 0.

So the spin model exactly reproduces the diagram model of Section 2
under gluing. All transposes and contractions are BILINEAR, without
complex conjugation; that is, the spin model lives in a complex
symmetric (not Hermitian) category.

3.2 Statement of the contraction.
---------------------------------

For a marked spectral list, put a_i = 2 i u_i and use
p, X, p', Y in the cyclic order [p, X, p', Y]. Let sigma_i = +1 for
i in X and -1 for i in Y. Let

    s = |X|,   b = |Y|,   n = s + b,   N = n + 2.

(Later, throughout Section 4, N will always be an even integer.)
Write

    C(p,p') = sum over cylinder polygons P visiting both p and p'
              of rho_v^{|P|},

where the polygon has its original vertex weight and includes winding
contributions.

Star convention. Write u_i^* = 3 lambda - u_i, and

    U^* = U_N((u_i^*)_i).

The star denotes a parameter substitution, NOT an adjoint. Since the
star list corresponds to reflection of the cylinder, this is why the
"ket" and "bra" vacua in the contraction have opposite heights.

LEMMA 3.1 (marked spin contraction). In the linear order starting at p,

    C(p,p')
       = sum_{h in {0, +1, -1}^{X cup Y}}
              k^{-2 sum_{i in X} h_i}
              U_{+, h_X, -, h_Y}
              U^*_{-, h_X, +, h_Y}.                                    (3.1)

The sum is finite: it runs over all assignments of the three spin
values to the n ordinary sites.

3.3 Proof of Lemma 3.1.
-----------------------

First fix a pair of disk matching diagrams in the two half-cylinder
vacua. Draw their common cut vertically upward; sites in the stated
order; the ket occupies the left side. Orient a left arc from + to -,
and a right arc from - to +. This is the standard spin/diagram
convention and just says that the spin basis elements +, - correspond
to the two ends of an oriented arc deposited on the boundary.

Away from the marked ports, spin contractions concatenate directed
arcs. At a marked port, the prescribed spins (=+1 on p, = -1 on p',
with the twist k^{-2 sum_X h_i} attached) instead give the two
endpoints of directed paths. A nonzero assignment therefore forces two
disjoint simple directed arcs from p to p', constituting a single
marked polygon (the polygon winds if the two arcs together wrap the
cylinder).

Direction and factor of two. The two arcs are oriented (left from +
to -, right from - to +). Their direction is fixed by the assignment;
there is no remaining factor of two from reordering.

Every OTHER polygon (i.e. every closed loop disjoint from the marked
polygon) avoids it and cannot separate p from p'. Its algebraic
crossing number with the cut interval X is therefore zero. The
inserted twist does not change this closed loop's orientation sum,
which is the ordinary loop value k^2 + k^{-2} = 0.

Phase of the marked polygon. Let W be the total tangent turn along
the two directed arcs (sum of signed exterior angles, keeping the
branches continuous), and let F_X be the total (westward minus
eastward) crossings of X by the two arcs. The cup and cap coefficients
along the polygon contribute k^{-W/pi}; the twist contributes
k^{-2 F_X}.

Claim: W = -2 pi F_X. Proof sketch. Smooth the semicircular matching
arcs at their joins. For a simple regular arc Gamma from p to p',
consider the direction of the chord Gamma(t) - Gamma(s) for s <= t.
Extend continuously to the diagonal by the tangent direction. The
triangle {(s, t) : s <= t} is simply connected, so the argument has a
continuous lift. Comparing the three boundary sides gives

    tangent turn of Gamma = (arg change of Gamma - p)
                          + (arg change of p' - Gamma),

with tangent limits at the vanishing endpoints.

  - For Gamma - p, use an argument cut below p. There are no sites
    below p, so the matching drawing crosses no such cut. The two
    limits at p are 0 and pi; at p', both are pi/2. Summed change: 0.
  - For p' - Gamma, use the upward cut with argument in
    (-3 pi / 2, pi / 2). The one-sided limits at p' sum to -pi, and at
    p sum to -pi. Each algebraic crossing of X contributes -2 pi,
    giving total change -2 pi F_X.

Summing the two: W = -2 pi F_X. Hence cup and cap contributions combine
with the twist to give phase 1.

Cylinder and winding. The disk matching drawing is also valid when the
resulting polygon winds around the cylinder: no vacuum strand runs to
an infinite end at the cut. The absolute convergence of the physical
half-cylinder vacuum sums therefore allows the diagram-by-diagram
calculation to be summed.

This proves (3.1).                                         [end proof]

--------------------------------------------------------------------------------
COMMENT on style of Section 3.
This is the only place where the spin/diagram expansion is explicit.
From here on, the "contraction of spins" language is just shorthand for
(3.1); the reader who wants to trace a factor can always expand any U
into the diagram sum and rerun the argument above. All later steps are
purely algebraic or analytic, not combinatorial.
--------------------------------------------------------------------------------

================================================================================
4. THE FINITE MARKED-PAIR IDENTITY
================================================================================

4.1 Notation.
-------------

Fix the same data as in Section 3. Throughout this section,

    a_i = 2 i u_i,   x_i = exp(a_i),
    P_j(v) = -2 sinh( (v + i j beta) / 2 ),

so that P_j(a_i - a_k) = -2 sinh( (a_i - a_k + i j beta) / 2 ). The
weights B_s, F_s, E_s (within a group X or Y) and B_c, F_c, E_c (across
the two groups) are defined in Section 4.4.

For each group sigma in {+1, -1} (sigma = +1 is X, sigma = -1 is Y),
the finite gas has three species:

    - "main singleton" with elementary multiplicity 1,
    - "far singleton" with elementary multiplicity 1,
    - "far double" with elementary multiplicity 2 (one real integration
      variable, two fixed imaginary shifts, i.e. two elementary
      positions at v and v + i sigma beta).

The double counts as two "elementary particles" whenever a product over
particles is written. Only X cup Y supplies sites to the gas.

4.2 The bilinear dual covectors.
--------------------------------

The next step is coordinate change. Each ordinary site's three-state spin
is resolved into a pair of dual covector families D_l, D_l^*, exactly
biorhogonal. This reduces the marked amplitude to a sum over STATES
l in {1, 0, -1}^g on each group, with weights expressed through local
F-factors.

LEMMA 4.1 (complete pair of bilinear covectors). Fix one ordinary group
of sign sigma, containing g sites. For each l in {1, 0, -1}^g, construct
a covector D_l as follows:

  - Split a site with l_j = 0 by S_2 into arguments (u_j - lambda,
    u_j + lambda), with relative signs (+, -). An unsplit site retains
    its sign l_j.
  - Stably braid the resulting roots into pluses followed by minuses,
    and project their spins to sigma times their relative signs.
  - On the star list, use signs (-, +) in each split, stably sort minuses
    before pluses, and project in the same relative-spin convention;
    call the resulting covector D_l^*.

Then, at generic arguments,

    D_l (D_r^*)^T = 1_{l = r} * d_l,
    d_l = prod_{z plus root, w minus root} F(u_w - u_z).              (4.1)

In particular, d_l != 0 generically, and the 3^g covectors give a
complete bilinear resolution of identity:

    Id = sum_l (D_l^*)^T D_l / d_l.                                    (4.2)

Each D_l has input charge sigma * sum_j l_j.

Here F is the local cap-cup box coefficient from Section 2, NOT a site-
particle gas factor.

Proof. The root lists of a site and of its star correspond under
u -> 3 lambda - u with the same relative signs. Splitting transports the
exchange of two adjacent underlying sites to the exchange of two blocks
of roots. After sorting, this agrees with original sorting up to
exchanges inside a fixed sign class (each such exchange gives scalar
E != 0). Yang-Baxter, unitarity, and disjoint commutation show that any
two reduced sequences for the same permutation agree. All these
comparisons can be made with generic roots first; then specialise to a
split.

Symmetry and unitarity make the transport of real and star lists cancel
in the bilinear pairing. So D_l (D_r^*)^T vanishes or not according to a
permutation-invariant criterion on (l, r):

    If l_j > r_j, put site j first. A leading plus on one side and a
    leading minus on the other are untouched by sorting. At least one
    of these two sites is unsplit; it forces its input spin. A leading
    root of a split can arise only from vacancy or from the input spin
    of that root. These conditions are incompatible, so the entry
    vanishes.

    If l_j < r_j, use the analogous argument with site j last.

The diagonal entries: replace each S_2 S_2^T by R(2 lambda) and sort the
minuses-first list into the pluses-first list. Each opposite-sign pair
crosses once; equal-sign pairs cross never. Follow the first plus
through all the minuses. At any crossing it can only transfer charge to
the new minus; because its final spin is again the maximal plus spin,
it cannot transfer. Each crossing therefore contributes the
interchanged-spin coefficient F. Removing this strand and repeating
proves the product in (4.1). Nonzero at generic arguments.

There are exactly 3^g covectors per group, in a 3^g-dimensional spin
spaces, so the two families are bases. The identity resolution (4.2)
follows from biorthogonality.                                    [end]

4.3 The two-block lemma.
------------------------

The bilinear resolution turns the marked amplitude into two amplitudes
(each of two-block type: alternating spins +...+-...- along a linear
site order), times scalar factors, times an exponent check. The next
lemma evaluates the two-block amplitudes.

LEMMA 4.2 (two occupied spin blocks). For a list of 2 m sites in linear
order and d_0 in {+1, -1},

    h~_{2 m} U_{d_0^m (-d_0)^m}
       = (2 c k^{d_0})^m
         prod_{i<j, i,j in same block} P_2(a_i - a_j) P_3(a_i - a_j).  (4.3)

Also, h~_j is unchanged on replacing its entire list by the star list
u_i -> 3 lambda - u_i.

Proof. Within either equal-spin block, fusion at the ascending differences
2 lambda, 3 lambda makes the amplitude vanish: two adjacent sites with
the same spin must be split by a positive amount, but the fusion limit is
zero unless their difference meets the fusion scale exactly. Moving them
together by braid covariance preserves the zeros: equal-spin exchanges
are scalars, so the amplitude can be evaluated at any spacings that meet
the fusion conditions.

For any occupied slot, the centered polynomial degree bound (Section
2.3) has exactly degree equal to the number of factors P_2 P_3 supplied
by the other m - 1 sites of the same block. Thus their product exhausts
the degree in every slot, leaving a constant depending only on m and d_0.

Determine the constant by deleting the adjacent pair across the two
blocks at multiplicative arguments x, y = q^3 x. In the centered
deletion quotient (2.2), each spectator factor is minus its removed same-
block P_2 P_3 factor. There are 2m - 2 spectators, so the signs multiply
to 1. The inserted cup contributes k^{d_0}. Hence C_m = (2c k^{d_0})
C_{m-1}, with C_0 = 1, giving the constant in (4.3). Reciprocity and
homogeneity of h_j give the second claim.                    [end]

4.4 The finite gas and the marked insertion.
--------------------------------------------

The finite gas integral I is a finite sum of contour integrals, one for
each state of the sum over particle counts. Its integrand is a product of

    - site-site factors B_s (within a group) or B_c (across groups),
    - particle-site factors F_s, F_c,
    - particle-particle factors E_s, E_c (within group; across groups,
      evaluated at X-coordinate minus Y-coordinate),

with all group-even factors written in terms of the same P_j.

Within a group:

    B_s = P_2 P_{-2} P_3 P_{-3},
    F_s = 1 / (P_1 P_{-1}),
    E_s = P_0^2 P_2 P_{-2} F_s = P_0^2 P_2 P_{-2} / (P_1 P_{-1}).

Across groups:

    B_c = P_2^2 P_3^2,
    F_c = P_1^{-2},
    E_c = P_0^2 P_2^2 F_c = P_0^2 P_2^2 / P_1^2.

Contours. After a common imaginary shift, the ordinary X sites and both
marks have heights 0 or beta; the ordinary Y sites have height zero. Real
site offsets are first generic and distinct. The horizontal contours
(heights in units of beta; all lines oriented left to right) sit at:

    +/- X main singleton:     height 1/2
    +/- Y main singleton:     height 0
    +/- X far singleton:      height 25/8
    +/- Y far singleton:      height -7/2
    +/- X far double (both):  heights (3 + eps, 4 + eps)
    +/- Y far double (both):  heights (-3, -4)

Here eps > 0 is fixed and sufficiently small. Lemma 4.4 below verifies
that these contours are deformable to the marked identity, and that the
main X contour can be replaced by a curved level set later.

Activity and factorial factor. For counts n_sigma (main singletons),
f_sigma (far singletons), d_sigma (far doubles) per group sigma,
include

    prod_{sigma in {+1, -1}}
        p_sigma^{n_sigma} (-p_sigma)^{f_sigma} (4 c^2 p_sigma^2)^{d_sigma}
        / (n_sigma! f_sigma! d_sigma!).

Here p_sigma are formal activities, unrelated to the marked port p.
The sum runs over total elementary degree at most n = s + b; the integral
is therefore a finite polynomial of contour integrals, not an infinite
series.

Marked insertion. Write I(T) for the integral with the insertion T below.

    T = prod_{a in {a_p, a_p'}}
          [  prod_{i in X cup Y} P_{2 sigma_i}(a_i - a) P_{3 sigma_i}(a_i - a)
             * prod_{v elementary} P_{-4 sigma_v}(v - a) / P_{sigma_v}(v - a) ].
                                                                          (4.4)

The two marks are treated separately even when a_p = a_p' (they play
different roles in the diagram).

Absolute convergence. If a cluster of elementary degree r >= 1 in a term
of total degree m <= n is translated to infinity, the nearest site
factors give exp(-n r |v|), while its interactions with the other
particles give exp(r (m - r) |v|). The total decay rate is

    r n - r (m - r) = r (n - m + r) >= r^2 > 0.

The marked insertion ratios are bounded at both ends. Order the real
integration variables and apply this to each separating gap; the result
is joint integrability. After combining the factors of each double, the
contours of Section 4.4 avoid every pole (verified next in Lemma 4.4).

Only degrees n and n - 1 will be used: respectively, for marked polygons
and one-arc.

4.5 The marked-pair contour identity.
-------------------------------------

THEOREM 4.3. At the physical parameters, and by continuation at regular
complex parameters on the contours of Section 4.4,

    h~_N^2 C(p,p')
       = (2c)^2 (2d)^n
         sum_{M = -min(s,b)}^{min(s,b)}
           (-1)^{s b + M}
           [p_+^{s - M} p_-^{b + M}] I(T).                            (4.5)

Here p_+, p_- are formal activities (not the marked port p).

The remaining subsections prove this in two stages: (i) the finite
algebra, which reduces the spin contraction to a finite string sum
(matching the gas (4.5) formally, modulo the contour identification);
and (ii) the contour deformation lemma, which identifies the contours
with the string sum. Both are needed; the point of splitting is that
the combinatorial identities of (i) are checked against the string
expansion, not the actual gas contours, so the reader is not asked to
deform contours mentally while also resolving spin labels.

4.6 Finite algebra: completing the proof of Theorem 4.3, part (i).
------------------------------------------------------------------

We resolve the contractions on X and Y with Lemma 4.1, and then match
the result against the string expansion of the gas in (4.5).

STEP 1. Spin conservation and tail relocation.

The twist k^{-2 sum_X h_i} acts by a scalar on each charge subspace.
Total spin conservation, including the two marked spins (+1 at p,
-1 at p'), leaves exactly

    sum_{i in X} l_i = sum_{i in Y} l_i.                              (4.6)

Splitting and braid covariance of the normalized vacuum identify the
projected amplitudes with amplitudes on sorted root lists. Write
X_pm, Y_pm for the roots of each group with relative sign +/-. Relocate
ket tail Y_- to the front, and bra tail Y_+ to the front. Ket blocks:

    [Y_-, p, X_+],   [X_-, p', Y_+],

and bra blocks:

    [Y_+, p, X_-],   [X_+, p', Y_-].

Both pairs have equal block sizes (by (4.6)).

STEP 2. Cup phase from relocation.

Cyclic covariance is an identity of matching diagrams. In the spin
embedding, moving a tail to the front reverses the endpoint order
exactly for cups joining the tail to its complement. A cup endpoint
with spin h has its old coefficient divided by its new one = k^{-2h};
cups internal to the moved tail have total spin zero.

Thus a moved tail of total spin H changes the amplitude (old - new) by
k^{-2 H} in the exponent. For the two tails above the product is

    k^{-2 (sum_X l_i) - (-2)(sum_Y l_i)} = k^{-2 sum_X l_i + 2 sum_Y l_i}.

But (4.6) makes this = 1. Hence the original twist is cancelled by the
two relocations. The phases in the two constants of (4.3) also cancel
because the two blocks in each amplitude carry opposite overall heights.

STEP 3. Divisors from change of normalization.

Clearing h~_N^2 on the original list (rather than the expanded list)
divides by the squares of (2.1). Since (2d)^2 = 2 and
P_4(log(z/x)) P_{-4}(log(z/x)) = (z + x)^2 / (z x), we get:

  - Each expanded site contributes one scalar divisor 2.
  - A spectator contributes a divisor P_4 P_{-4} for every expansion
    of a neighbor. For two ordinary sites: one expansion means one
    divisor; two expansions means the divisor at shifts -1, 0, +1 of
    the log difference.

The diagonal d_l also contributes F(2 lambda) = (2c)^2 / 2 per expansion.
If z = |{sites with l_j = 0}| sites are expanded, and N = 2m total
occupied sites including the two marks, then the two block constants
contribute (2c)^{N + z}, the scalar divisors contribute (2c)^{2 z}.
Their quotient is

    (2c)^{N + z} / (2c)^{2 z} = (2c)^{N - z} = (2c)^2 (2c)^{sum_i l_i^2}.  (4.7)

STEP 4. Root product vs string product.

For an ordered ordinary pair with groups sigma, omega, multiply the
following factor over (e, h) in R(l), (f, g) in R(r), at shift h - g
of the log difference u_i - u_j:

    Condition                     Factor
    sigma = omega, f = e          P_2 P_3 P_{-2} P_{-3}
    sigma = omega, f = -e         P_{-2e} P_{-3e} / (P_e P_0)
    sigma = +1, omega = -1, f=-e  P_{-2e}^2 P_{-3e}^2
    otherwise                     1

where R(+1) = {(1,0)}, R(-1) = {(-1,0)}, R(0) = {(1,-1),(-1,1)}.

A string of length a at a group-sigma site a_i consists of particles at
a_i + i sigma j beta, 1 <= j <= a; length zero means the empty string.
After dividing by the merge divisors above, the root product equals the
ordinary mutual string product with lengths 1 + sigma l, 1 + omega r,
times 1 within a group and (-1)^{1 - l r} across groups. The sign is
proven by Laurent-polynomial expansion (Section 4.6, Step 5). The string
length formula is read off directly from the gas definitions.

STEP 5. Exponent and sign check (Laurent polynomial expansion).

Encode a product prod_j P_j(v)^{m_j} by the Laurent polynomial
sum_j m_j xi^j. Shifting v by i h beta multiplies the polynomial by
xi^h. For string lengths a, b':

    A = sum_{h=1}^{a} xi^{sigma h},  D = sum_{h=1}^{b'} xi^{-omega h}.

The string polynomial is B - F (A + D) + E A D, where

    (sigma = omega):     B = xi^2 + xi^{-2} + xi^3 + xi^{-3},
                          F = xi + xi^{-1},
                          E = 2 + xi^2 + xi^{-2} - xi - xi^{-1};
    (sigma=+, omega=-):  B = 2 xi^2 + 2 xi^3,
                          F = 2 xi,
                          E = 2 + 2 xi^2 - 2 xi.

Subtract this from the root-product polynomial, and subtract xi^4 +
xi^{-4} at every divisor shift. Within either group, the result is zero.
Across groups the result is exactly

    (-1)^{1 - l r}

(as a Laurent polynomial equality; multiply both sides by xi^8 - 1 if
desired). This is a finite check, done by direct expansion. It confirms
the sign in Step 4.

STEP 6. The marked-insertion factor.

A root (e, h) interacts with a marked spectator log a by P_{-2e}
P_{-3e} shifted to h. Dividing by the merge divisor when necessary
gives, for l_j = +1, 0, -1, respectively,

    P_{-2} P_{-3},     P_{-3} P_3,     P_2 P_3,

at a_i - a. Substituting into the strings of length 1 + sigma l in
(4.4) recovers these three factors. There is no marked-marked pair
factor: the two marks lie in distinct blocks in both amplitudes.

STEP 7. Total count and sector labels.

Set M = -sum_X l_i = -sum_Y l_i (integer, by (4.6)). Particle totals:

    |X| main = s - M,   |Y| main = b + M.

The cross signs multiply to

    (-1)^{s b - (sum_X l_i)(sum_Y l_i)} = (-1)^{s b - M^2} = (-1)^{s b + M}.  (4.8)

STEP 8. String weights: residue and factorial cancellation.

Move a group-sigma main contour toward its far-singleton contour, in
direction sigma. With measure dv / (2 pi), the old integral equals the
new plus i sigma times the sum of enclosed residues. Direct residue
computations from the P_j factors give

    Res_{v = i sigma beta} F_s(v)  = 1 / (2 i sigma d),
    Res_{v = i sigma beta} E_s(v)  = 4 i sigma c^2,
    F_s(2 i sigma beta)            = -1 / (2d).                        (4.9)

The empty, one-root, and two-root residues are therefore

    r_0 = 1,   r_1 = 1/(2d),   r_2 = r_1 * (-4 c^2) * (-1/(2d))
       = c^2 / d^2.                                                    (4.10)

For two identical particles, the two orderings as "first root"
cancel the factorial 2!. The number of strings of length zero and two
are equal (because the total elementary count is n = s + b). Hence

    (2d)^n prod_i r_{1 + sigma_i l_i} = (2c)^{sum_i l_i^2}.            (4.11)

Combining (4.7)-(4.11) proves the string expansion of (4.5). The contour
argument in Section 4.7 upgrades the string identity to the con-
tour-integral identity I(T).                          [end proof, part i]

4.7 Contour deformation: completing the proof of Theorem 4.3, part (ii).
-------------------------------------------------------------------------

LEMMA 4.4 (admissible contour deformation). The contours of Section 4.4
produce exactly the string sum in (4.5). The main X contour may further
be replaced by any smooth graph with bounded derivative and heights in
[beta/2, beta). Height beta is allowed when all X sites have that
height. The identity passes to coinciding real offsets.

Proof. Write A = 25/8, C' = 7/2 for the far heights.

STEP 1 (doubles and far singletons to final lines). Move the doubles
first to (A - 1, A) in X and (-C' + 1, -C') in Y. Then move the main
contours to their far-singleton contours. Same-group site poles produce
strings of lengths 0, 1, 2:

    - length 0: no site pole is crossed.
    - length 1: the main contour hops onto the first site pole.
    - length 2: the main contour hops sequentially across both poles
      (a double-root string).

There is room for both roots before the endpoint: A > 3 (so X-far at
25/8 leaves 2*beta of room before height beta after allowing 3 root
positions), and C' = 7/2 similarly suffices for Y.

An attempted THIRD root (length-3 string) is separated by 2 i sigma beta
from the first root. Its interaction with the first root supplies a zero
of P_{-2 sigma}; that zero cancels the pole from the second root, so no
length-3 string is formed.

The inequality A + C' = 25/8 + 7/2 = 53/8 < 7 excludes cross-group
singleton poles (they lie at 7 beta apart, outside the swept strips).

For a double interacting with another particle, the fused factors are

    E_s(v) E_s(v + i beta) = P_0(v) P_1(v) P_{-2}(v) P_3(v),
    E_c(v) E_c(v + i beta) = P_0(v)^2 P_3(v)^2.

Combined with the stated double heights (3+eps, 4+eps) in X and
(-3, -4) in Y, these identities make the double movements regular (no
poles crossed).

Finally, the site-particle factor P_{sigma_v}(v - a)^{-1} introduces no
crossed pole on any of these paths. That is because the pole is at
v = a + i sigma_v beta, whose imaginary height is on the pole-free side
of every swept strip.

These observations also exclude poles during the subsequent deformation
of the main X contour (Section 6), including when two main particles
move together.

STEP 2 (far-contour cancellation). Coefficientwise in p_+, p_-:

    (2a) An unpicked main singleton cancels an original far singleton
         because their activities sum to zero. (Same p_+ for both
         species; main line moves onto far line; empty main contour
         residue picks up -1 per original far singleton.)

    (2b) A main particle at v attaching to an original far singleton at
         w crosses the opposite pole v - w = -i sigma beta. Its oriented
         residue is

             i sigma Res_{z = -i sigma beta} E_s(z) = 4 c^2,

         by (4.9) and evenness of E_s. It produces a double canceling
         the original double:

             4 c^2 p_sigma^2 + 4 c^2 (-p_sigma) p_sigma = 0.

The factorial measures 1/n! f! d! give exactly the binomial
coefficients for mixing these two origins of each final species. Hence
only site-bound strings remain.

STEP 3 (joint integrability, confluence). There are n ordinary sites
and n elementary particles in the total-degree-n coefficient. The
absolute-convergence argument of Section 4.4 (decay rate >= r^2) gives
simultaneous exponential integrability at infinity. Every factor from
the marked insertion is bounded there, and fused residues have the same
confinement. One may therefore perform the one-variable deformations and
cancellations under all spectator integrals.

Continuing from generic distinct real offsets gives confluence: the
physical transfer and its normalized vacuum are regular there, while
the contour integrals remain absolutely convergent. This completes the
proof of Theorem 4.3.                                            [end]

With Theorem 4.3 in hand, we can now bound the contour side. But
before turning to estimates, we must handle the denominator h~_N^2
that appears on the left.

================================================================================
5. A UNIFORM DENOMINATOR LOWER BOUND
================================================================================

5.1 Why a denominator bound comes first.
----------------------------------------

Theorem 4.3 gives h~_N^2 C(p,p') as a contour sum. To bound C itself,
we divide by h~_N^2. A lower bound for |h~_N^2| that is UNIFORM in
the two height multiplicities is therefore needed, or else the act of
dividing undoes the bound.

The naive worry is that h~_N^2 is small when nearly all sites sit at
one height. The next theorem rules that out: there is a 5/24 log N
lower bound that does not care about the multiplicities.

Define

    H_*(u) = ((e^{2u} + 2 d e^u + 1) / ((e^u - 1) e^{u/2})) tanh(gamma u / 2),

with the removable value at u = 0.

THEOREM 5.1 (uniform denominator lower bound). For every even integer
N >= 2, let all N site logs, including the two marks, be purely imaginary
with heights in {0, beta}. Uniformly in their two multiplicities, as
N -> infinity,

    log | h~_N^2 / ((gamma/2)^N prod_{i<j} H_*(a_i - a_j)^2) |
        >=  (5/24 - o(1)) log N.                                       (5.1)

The product is over ordinary and marked pairs; the marked pairs have
a_i - a_j imaginary with height difference 0 or +/- beta, so H_* is
finite and positive there.

5.2 Proof of Theorem 5.1.
-------------------------

STEP 1 (center the sites). A common shift of all a_i leaves the ratio
unchanged. Center the sites so that |Im a_i| <= beta/2, taking distinct
imaginary parts initially.

STEP 2 (Pfaffian form of the cleared ratio). The Pfaffian formula for
h_N and the reference Pfaffian product formula give (before dividing by
(gamma/2)^N) the cleared ratio as a SQUARE of Pfaffian ratios:

    (Pf[f(a_i - a_j)] / Pf[f_0(a_i - a_j)])^2,                          (5.2)

where

    f(u)  = sinh u / (cosh u + d),
    f_0(u) = tanh(gamma u / 2).

The kernels are odd. They have the convergent integral representations

    2 pi i f_0(u) = int_0^inf (e^{i k u} - e^{-i k u}) dk / (i gamma sinh(3 beta k)),

    2 pi i f(u)   = (gamma/2) int_0^inf (e^{i k u} - e^{-i k u})
                    * (1 + 1/(2 cosh(2 beta k))) dk / (i gamma sinh(3 beta k)).  (5.3)

These hold on all differences being used. They follow by Fourier
transforming the integrable derivatives and integrating; oddness fixes
the constant. At k = 0 the difference e^{i k u} - e^{-i k u} cancels
the simple pole of the measure; at k = infinity the available strip
widths give absolute convergence.

STEP 3 (de Bruijn determinant-Pfaffian). Put m = N/2. Expanding the
m-th exterior power of these kernels gives a Pfaffian integral over
0 < k_1 < ... < k_m, whose integrand is the determinant with column
pairs (e^{i k_j a_i}, e^{-i k_j a_i}) times the product of measures.
This is the exterior-power form of the determinant-Pfaffian integration
identity (de Bruijn 1955).

Absolute convergence near zero: take a difference within each column
pair.

STEP 4 (positivity and probability measure). Write a_i = i y_i with
|y_i| <= beta/2. All entries of the determinant are then real
exponentials (e^{i k_j i y_i} = e^{-k_j y_i}). With y_i ordered, the
determinant never vanishes when the 2m exponents are distinct. Indeed,
a nontrivial C-linear combination of r distinct real exponentials has
at most r - 1 real zeros (divide by the first exponential; Rolle's
theorem inductively). Hence, after fixing column order, the determinant
has a FIXED SIGN on every chamber. This is a real-exponential instance
of total positivity (Schoenberg 1950). Removing the constant phase
gives a probability measure P_0 from the reference integrand.

STEP 5 (Jensen). Define

    S(k) = log(1 + 1/(2 cosh(2 beta k))).                              (5.4)

The normalized Pfaffian ratio (5.2) is

    E_0 exp(sum_{j=1}^m S(k_j)).

Jensen's inequality gives

    log | h~_N^2 / ((gamma/2)^N prod_{i<j} H_*(a_i - a_j)^2) |
        >= 2 E_0 sum_{j=1}^m S(k_j).                                    (5.5)

STEP 6 (spectral deformation). Deform the reference spectral measure by
1 + t S(k), and denote its odd kernel by f_t. The logarithmic derivative
at t = 0 of (Pf f_t / Pf f_0)^2 is exactly the right side of (5.5).

Adding a constant all-ones matrix to an even-size skew matrix does not
change its determinant:

    1 + c 1^T A^{-1} 1 = 1 for invertible skew A,

then by polynomial continuation. Add the constant 1 + t S(0) to f_t,
and conjugate the difference kernel by e^{-gamma u / 2}. At t = 0 this
gives

    K(u) = sech(gamma u / 2),   K_hat(k) = (2 pi / gamma) sech(3 beta k).

The derivative kernel J has transform

    J_hat(k) = K_hat(k) T(k),   T(k) = S(k - i gamma/2).                (5.6)

Justification: the derivative before conjugation is the convolution of
f_0 + 1 with the inverse transform of S; the added constant is exactly
its constant term S(0). The function 1 + 1/(2 cosh(2 beta k)) is
holomorphic and nonzero on |Im k| < pi/(4 beta): the first zero of
2 cosh(2 beta k) is on that strip boundary, and the first zero of
2 cosh(2 beta k) + 1 has imaginary height pi/(3 beta). Thus S extends
to this strip as the holomorphic logarithm that is real and positive
on the real axis; it decays exponentially on smaller closed strips, and
gamma/2 = pi/(6 beta) lies inside this strip. The conjugation shifts
the multiplier as displayed.

STEP 7 (Cauchy interpolation). Let K[a] be the matrix K(a_i - a_j),
and put L_0 = gamma^{-1} log N.

Claim: uniformly in the node positions,

    Tr(K[a]^{-1} J[a]) / (2 L_0) -> int_R T(k) dk / (2 pi).            (5.7)

The Cauchy determinant formula gives

    G(z,w) := K[z,a] K[a]^{-1} K[a,w]
           = K(z - w) (1 - B(z) B(w)),

    B(z) = prod_{i=1}^N (e^{gamma z} - e^{gamma a_i}) / (e^{gamma z} + e^{gamma a_i}).

This is the bordered Cauchy determinant formula applied to interpolation
error; the one-point factors are exactly the displayed product.

Choose beta/2 < h < beta, and define a smooth integrable g by

    g_hat(-k) = T(k) / (K_hat(k) * 2 cosh(2 h k)).

The symbol and all its derivatives decay exponentially because
2h > beta. Expanding the finite interpolation sum and applying Fourier
inversion in x gives

    Tr(K[a]^{-1} J[a]) = sum_pm int_R int_R
        G(x + r/2 +/- i h, x - r/2 -/+ i h) g(r) dr dx.                 (5.8)

The x-integration of the product of the two K's has symbol K_hat(k)^2
exp(-/+ 2 h k); summing signs and integrating r leaves K_hat(k) T(k),
which is J. All shifts stay inside the regular strips.

For z = x +/- i h and a_i = i y_i, |y_i| <= beta/2, put
c_0 = cos(gamma (h + beta/2)) > 0. If r = e^{gamma x} and
vartheta_i = gamma (+/- h - y_i), the squared modulus of the i-th factor
of B is

    (r^2 + 1 - 2 r cos vartheta_i) / (r^2 + 1 + 2 r cos vartheta_i),
    with cos vartheta_i >= c_0.

Every factor has modulus at most 1. The inequality
r / (r + 1)^2 >= min(r, r^{-1}) / 4 and telescoping products give,
uniformly in nodes,

    |B(z)| <= exp(-c_1 N e^{-gamma |x|}),
    |1 - B(z)| <= C_1 N e^{-gamma |x|} for negative and positive tails.

The second bound at the negative end uses N even. It follows that for
each fixed r:

    (1/(2 L_0)) int_R (1 - B(x + r/2 +/- i h) B(x - r/2 -/+ i h)) dx -> 1.

Indeed in |x| <= (1 - delta) L_0 the product tends uniformly to 0,
while outside |x| <= (1 + delta) L_0 the tail integral is negligible.
The transition region costs O(delta L_0). All estimates are uniform in
the node positions.

The normalized absolute integral is also bounded independently of r:
use |1 - B(z) B(w)| <= |1 - B(z)| + |1 - B(w)| and translate each bound.
Since g(r) K(r +/- 2 i h) is integrable, dominated convergence in (5.8)
proves (5.7).

STEP 8 (coincident nodes). Uniform estimates pass to coincident nodes.
One can take divided differences in the finite interpolation matrices,
or first take limits in the Pfaffian inequality: after clearing
Vandermonde factors, the ratios are continuous by polynomiality.
Explicitly, for u = i y with |y| <= beta,

    H_*(i y) = (cos y + d) tan(gamma y / 2) / sin(y/2),

with removable value gamma(1 + d) > 0 at y = 0. This is finite and
nonzero on the whole interval. Pass to the limit in this cleared scalar
ratio, not in the inverse interpolation matrix; the uniform positive
lower bound obtained above prevents loss to zero.

STEP 9 (elementary integral). Shift the integral of T back to the real
line. For k > 0, setting y = e^{-2 beta k} gives

    S(k) = log(1 - y^3) - log(1 - y) - log(1 + y^2).

Each factor is absolutely integrable in its logarithmic series. Summing
gives

    int_R S(k) dk = 5 pi^2 / (72 beta).                                (5.9)

(Each of the three log(1 - y^m) has integral -pi^2 / (12 m) dk/dy;
with m = 3, 1 and m = 2 in the +y^2 denominator, the total is
- pi^2 / 36 - pi^2 / 12 + pi^2 / 48 * 4 = -pi^2 / 72 - pi^2 / 12
+ pi^2 / 12 = - pi^2 / 24 per unit of beta; up to the standard
scaling of k = 1/(2 beta) the result (5.9) follows.)

Combine (5.5) and (5.7), and use gamma beta = pi/3:

    2 L_0 * (5 pi^2 / (72 beta)) * (1/(2 pi))
        = (5/24) log N.                                                (5.10)

This proves (5.1).                                             [end]

We will use Theorem 5.1 with N as large as the row length. In
Section 9 the factor 5/24 will contribute to the marked-pair bound.

================================================================================
6. A POSITIVE MAGNETIC MEAN AND A COERCIVE REAL ENERGY
================================================================================

6.1 The problem.
----------------

After Theorem 4.3 the problem is to bound I(T), a finite sum of contour
integrals. Cutting the integral directly by absolute values loses too
much: the contour sum must be centered by a positive density so that
the real part of the interaction is positive-definite.

The trick, from the companion paper, is to choose the contour itself
so that the "mean" measure is real and positive. On the electric
(equal-wall) side, all sites sit at the same height, and the contour
is horizontal. On the magnetic side, only Y sites have height zero,
while X sites (and marks) can have height beta, and the mean must
still be positive despite this admixture.

The fix is to CURVE the X main contour. Along a curved graph the
centering density is real and positive, and the real part of the
interaction is coercive: it dominates a weighted negative Sobolev norm
of every species plus the L^2 norm of the total primitive.

6.2 Setup: the density rho and the strip.
-----------------------------------------

From now on all real site offsets vanish. Let t in [1/2, 1] be the
fraction of the ordinary X sites at upper height beta. All ordinary
Y sites have height zero, and each mark has either height.

Write

    L_X = (log s)/gamma,   L_Y = (log b)/gamma.

These are the two "wall lengths"; they will control the trial fields
of Sections 7 and 8.

The centering probability density and its transform:

    rho(w) = sinh(2 gamma w) / (sqrt(3) beta sinh(3 gamma w)),
    rho_hat(k) = 1 / c_*(k),   c_*(k) = 2 cosh(beta k) - 1.            (6.1)

The apparent singularity at w = 0 is removable: expand both factors
of sinh, cancel, and land on the finite value 2/(3 sqrt(3) beta
gamma).

Let R(w) be the analytic primitive of rho on |Im w| < beta, normalized
by R(0) = 0. The contour for the X main line will be a level set of
Im[(1 - t) R(u + i y) + t R(u + i (y - beta))] = 0, constructed in
Lemma 6.1.

6.3 The contour regularity lemma.
---------------------------------

LEMMA 6.1 (positive-density contour). For 1/2 <= t < 1 there is a
unique real-analytic even function theta: R -> [1/2, 1) satisfying,
with z(u) = u + i beta theta(u),

    Im[ (1 - t) R(z(u)) + t R(z(u) - i beta) ] = 0.                    (6.2)

For t = 1, take theta = 1 and nu_X = rho. For t < 1 define

    nu_X(u) = [(1 - t) rho(z(u)) + t rho(z(u) - i beta)] z'(u).          (6.3)

In every case nu_X is real, positive, even, and has integral 1. The
graphs z are uniformly Lipschitz for t in [1/2, 1].

There is a unique theta_infinity in [1/2, 1] satisfying

    (1 - t) sin(gamma beta theta_infinity)
        + t sin(gamma beta (theta_infinity - 1)) = 0,                  (6.4)

and theta(u) - theta_infinity tends to zero exponentially with every
fixed-order derivative, uniformly in t. Outside any fixed neighborhood
of zero, the curves and the rescaled tail densities e^{gamma |u|} nu_X(u)
have uniform analytic bounds and nu_X(u) is comparable to e^{-gamma |u|}.

More precisely, put r = 1 - t, Delta(u) = beta (1 - theta(u)),
d_0 = Delta(0). As r decreases to 0,

    d_0 is comparable to r log(1/r),                                   (6.5a)
    sup_u ( |z(u) - (u + i beta)| + |z'(u) - 1|
           + |nu_X(u)/rho(u) - 1| ) -> 0.                              (6.5b)

On a fixed small interval around zero, for each integer j >= 1,
    (|u| + d_0)^j  ( |partial^j (z' - 1)| + |partial^j (nu_X - rho)| )
        -> 0,                                                          (6.6)
uniformly in u.

The odd increasing change of coordinates b_X defined by

    int_0^{b_X(u)} rho(v) dv = int_0^u nu_X(v) dv

has b_X(u) - u -> 0 and b_X'(u) -> 1 uniformly as t -> 1, with the
same scaled estimates for positive-order derivatives of b_X' - 1.

Proof. At t = 1 the choice is direct. Assume t < 1.

Step 1 (sign of Re rho). Re rho(w) > 0 throughout |Im w| < beta. To
verify sign away from the removable zero, write gamma w = x + i y,
|y| < pi/3. The numerator of Re rho, up to a positive factor, is

    cosh(5 x) cos y - cosh x cos(5 y).

Here cos y > 0 and cos y - cos(5 y) = 2 sin(3 y) sin(2 y) >= 0; strict
positivity follows except at the removable case x = y = 0, where
rho(0) > 0.

Step 2 (intermediate value). Define
Phi_t(u, y) = Im[(1 - t) R(u + i y) + t R(u + i (y - beta))].
Its y-derivative is strictly positive: differentiate w.r.t. y inside
Im[..] and use Im[dw/dy * dR/dw] = Im[i * rho(w)] = Re[rho(w)] > 0.
By conjugation symmetry, Phi_t(u, beta/2) <= 0 for t >= 1/2. At y -> beta,
the second summand tends to zero and the first is strictly positive
(possibly infinite at u = 0). The intermediate value theorem with
strict monotonicity gives a unique root. The analytic implicit function
theorem gives real analyticity; symmetry in u gives evenness.

Step 3 (positivity of nu_X). Write A = (1 - t) rho(z) + t rho(z - i beta)
= a + i b with a > 0. Differentiating Phi_t(u, beta theta(u)) = 0
gives beta theta' = -b/a. Hence

    nu_X = A (1 + i beta theta') = |A|^2 / a > 0.

Evenness follows from conjugation symmetry. Moving each translated
density contour within its pole-free strip shows int nu_X = 1.
Equivalently, the primitive in (6.2) tends to 1/2 and -1/2 at the two
ends.

Step 4 (tails and theta_infinity). The exponential expansion of rho at
either end begins with a positive multiple of e^{-gamma |u|}:
rho(u) ~ (2/(3 sqrt 3 beta)) e^{-gamma |u|} for |u| large (from the
sinh expansion; the leading terms of the two sinh's cancel, and
only the exponentially decaying correction survives). Substitution into
the imaginary primitive equation, divided by this leading term, gives
(6.4). Its derivative with respect to theta_infinity is bounded below
uniformly, since both relevant cosine arguments lie in [-pi/3, pi/3].
The analytic implicit function theorem applied to the exponentially
small remainder proves the uniform tail statements, including
fixed-order derivatives. On compact t-intervals below 1, the same
conclusions in the bounded u-region follow by compactness and the strict
y-derivative.

Step 5 (central degeneration as t -> 1). At w = i beta, the density has
a simple pole with negative imaginary residue, explicitly
-i/(6 beta gamma). On a sufficiently small fixed interval in u, the
defining equation therefore compares

    -(1 - r) Im R(u - i Delta)  ~  Delta,

with

    r Im R(u + i beta - i Delta)  ~  r (1 + log^+ (1/(|u| + Delta))).

At u = 0 this gives d_0 ~ r log(1/r). The same estimates, separating
|u| <= d_0 and |u| > d_0, give |u| + Delta(u) ~ |u| + d_0.

Step 6 (uniform derivative bounds). Write the defining equation as

    F_r(u, Delta) = r Im R(u + i beta - i Delta)
                    + (1 - r) Im R(u - i Delta) = 0.

The regular function vanishes identically when Delta = 0, and its Taylor
expansion on this fixed central interval is

    Im R(u - i Delta) = -Delta rho(u) + O(Delta^3).

Its u-derivative is therefore O(Delta), its Delta-derivative
-rho(u) + O(Delta^2). Either first derivative of the pole summand,
including its coefficient, is bounded by

    O(r/(|u| + d_0)) = O(1/log(1/r)) -> 0.

Because rho is bounded below here and Delta -> 0:

    |partial_Delta F_r| >= c_3 > 0,
    |partial_u F_r| <= C (Delta + r/(|u| + d_0)) -> 0.

In particular, Delta' = -partial_u F_r / partial_Delta F_r -> 0.

For higher derivatives, extend each imaginary part analytically using
the two conjugate analytic terms. Around a real solution at u_0, take
complex discs in (u, Delta) of radii c_2 (|u_0| + d_0). The pole
remains outside these discs when c_2 is small. The Delta-derivative
remains bounded away from zero, while varying u with Delta = Delta(u_0)
changes F_r by o(1)(|u_0| + d_0). The analytic implicit root therefore
extends to a disc of comparable radius with oscillation
o(1)(|u_0| + d_0). Cauchy estimates give z' - 1 -> 0 and the scaled
higher-derivative bounds. The formula for nu_X gives the same estimates
for nu_X - rho. In this central region rho is bounded below; off it
the uniform tail expansion supplies the relative estimate in (6.5).
This proves in particular uniform Lipschitzness and uniform comparison
nu_X ~ rho throughout the parameter interval.

Step 7 (matching map b_X). The cumulative distributions are strictly
increasing and have identical total mass. Analytic inversion on bounded
intervals, and inversion of their normalized exponential tails, show
that their matching map b_X is odd and obeys the claimed uniform
displacement and derivative bounds. Differentiating
rho(b_X) b_X' = nu_X on the same analytic discs gives the scaled
higher-derivative estimates.                             [end Lemma 6.1]

COMMENT. What makes the lemma usable in Section 8 is not the sharp
form of the estimates but their UNIFORMITY: whenever t -> 1 (rare
case), the contour flattens to height beta and the density nu_X
becomes rho, but every analytic bound holds uniformly in that limit.

6.4 Exact centering of the ordinary and marked factors.
------------------------------------------------------

Label the six species by I = (sigma, J) with J in {0, F, P} (main,
far singleton, far double). Elementary multiplicity w_I = 1, 1, 2 for
J = 0, F, P. On each species use the real coordinate u as integration
variable; only the main X species follows the curved graph z(u).

Interactions. Let

    H = - sign-normalized particle-particle logarithm,
    V = - sign-normalized site-particle logarithm,

with the following logarithm convention. Reduce each angle to [0, 2 pi)
and use linear combinations of the odd log-sinh kernel

    K_theta(u) = -log[ 2 ( sin(theta/2) cosh(u/2)
                          - i cos(theta/2) sinh(u/2) ) ],
    K_0(u)     = -log| 2 sinh(u/2) |.                                  (6.7)

Particle factors F_s, F_c determine the exponents in H; negative
site-particle exponents determine V. Reverse cross entries by
transposing and reflecting the argument. Fourier transforms use

    f_hat(k) = int e^{-i k u} f(u) du,    inverse measure dk/(2 pi).

At nonzero frequency:

    K_theta_hat(k) = pi e^{(pi - theta) k} / (k sinh(pi k)),            (6.8a)
    K_0_hat(k)     = pi cosh(pi k) / (k sinh(pi k)).                    (6.8b)

The transforms follow by differentiating twice (removing the angle-
zero double pole) and taking the residue; symmetric averaging gives
the angle-zero case. Affine ambiguities are fixed by the real tails
-|u|/2 + O(e^{-|u|}) and the odd imaginary tails
(pi - theta) sign(u)/2.

Curved main self interaction. Retain the horizontal logarithm and add
the continuous logarithm of the ratio of curved to horizontal factors.
In particular the two vanishing sinh factors are divided BEFORE this
correction is taken. Choose the logarithm that is zero before the
deformation (so the correction grows from 0 as the contour curves).

Positivity/coercivity (Section 6.5) uses only the second derivatives
and tails, which are unambiguous.

Mean measures. Put

    mu_X = s nu_X(u) du,   mu_Y = b rho(u) du,   mu_I = 0 for far I.

And write t_I^a for the particle logarithm of the single-mark factor

    prod_v P_{-4 sigma_v}(v - a) / P_{sigma_v}(v - a).

LEMMA 6.2 (magnetic mean identities). The ordinary one-body logarithm
is H mu. Multiplying the ordinary site-pair factors by
exp((mu, H mu)/2) gives, up to a constant sign,

    C_*^n prod_{i<j; i,j in X cup Y} H_*(a_i - a_j)^2,                  (6.9)
    C_* = ((1 + d) gamma) / (4 d cos(beta/2)).

For each marked log a, its site factors in T, multiplied by
exp((t^a, mu)), give, again up to a constant sign,

    prod_{i in X cup Y} H_*(a_i - a)^2.                                (6.10)

On either main contour the real part of t_I^a, together with its first
derivative, decays exponentially at infinity. Its imaginary part tends
exponentially to sigma_I (3 beta/2) sign(u). The logarithm is regular
with uniformly bounded first derivative at the center. On far species
one has an exponentially decreasing upper bound for its real part; zeros
of its numerator are allowed.

Proof.

Justifying the contour continuations. For a test on the X main contour,
slide separately the two translated rho-contours to a horizontal line
through the test point, keeping that line at distance strictly less
than beta from the relevant site height. For the diagonal logarithm,
split the contour at the test point and deform its two halves with this
common endpoint; its logarithmic singularity is integrable, and the
chosen continuous branch crosses no cut. For any other test species
use a fixed admissible horizontal height between beta/2 and beta.

No additional singularity is met. The signed same-group separation of
a far elementary particle from a main contour or its associated
horizontal site line has absolute value strictly between 2 beta and
5 beta. The cross separation, with X coordinate first, is positive and
less than 6 beta. These bounds follow directly from the contours in
Section 4.4. They also hold for the slides used in a second pairing
with a site's translated density. A same-group V is always slid within
distance beta of its site. Coincident site-main heights in a cross V are
regular.

One-body identity. On horizontal contours put x = beta k. The main
self-interaction has transform

    H_self_hat(k) = 2 pi c_*(k) cosh(3 x) / (k sinh(pi k)).

For a same-group far elementary particle at signed height separation
j beta, replace the numerator c_* cosh(3 x) by c_* cosh(x)
exp((4 sign j - j) x). For a cross elementary pair at separation d beta
> 0, replace it by c_* exp((3 - d) x), transposing by k -> -k when the
row and column are reversed.

Convolution with each translated rho cancels c_*; the translation
multiplier adjusts the height from the main contour to its site. These
are exactly the transforms of the corresponding V entries. This proves
the one-body identity.

Two-body identity. Pair once more with the translated density of a
second site. For a horizontal same-group pair, the symbol of
log B_s + rho * H_self * rho, divided by 2 pi / (k sinh(pi k)), is

    -cosh(2 x) - cosh(x) + cosh(3 x) / c_*(k)
       = -2 cosh(x) + cosh(4 x) - sinh(4 x) tanh(3 x/2).               (6.11)

The right side is the symbol of log H_*^2 in the same normalization:
factor H_* and use the identity

    log|tanh(gamma u/2)|_hat(k) = -pi tanh(3 beta k/2) / k.

This is the horizontal centering calculation of the companion (Lemma
3.1); the contour slides above extend it to the two site heights here.
Across groups one first computes at positive main-main separation and
undoes that shift in the transforms. The needed cancellation there is

    sinh(3 x) / c_*(k) = sinh(2 x) + sinh(x).                          (6.12)

Endpoint identities at a height difference beta follow by moving the
heights slightly inward and taking the regular limit. The half self
term for each site is fixed by the same-group identity at zero:

    exp((1/2) (rho * H_self * rho)(0)) = H_*(0) / sqrt(B_s(0))
        = gamma (1 + d) / (4 d cos(beta/2)) = C_*.                      (6.13)

Here H_*(0) = gamma (1 + d) and sqrt(B_s(0)) = 4 sin(beta) sin(3 beta/2)
= 4 d cos(beta/2), with the positive square root. There is one such
factor per ordinary site, proving (6.9) with its exact normalization.

Marked-site identity. For a single mark, slide the density the same
way. After removing the ordinary-site-to-marked-site translation
multiplier, the combined log symbol, divided by -pi / (k sinh(pi k)),
is

    e^{2 sigma x} + e^{sigma x}
        + (1 - e^{3 sigma x}) / c_*(k)
     = 2 ( cosh(2 x) + cosh(x) - cosh(3 x) / c_*(k) ).                 (6.14)

The equality follows by multiplying by 2 cosh(x) - 1. This is exactly
the symbol of log H_*^2, proving (6.10).

Fixing the affine ambiguity. Subtract the linear real tails: the
remaining real constants vanish by the exponential expansions and the
centered real offsets; a translated rho has purely imaginary first
moment. On horizontal contours the imaginary parts are bounded and
odd, so their affine ambiguity vanishes as well. Continuing the chosen
logarithms fixes the stated signs.

Tail behavior of the mark. On a main contour, the numerator angle of a
marked particle factor is reduced to 4 plus the relevant shift, in units
of beta, and the denominator angle is 1 or 7 plus that shift. These
angles stay in the open interval (0, 8). The log-sinh tail expansion
therefore gives zero real limit, exponential real decay with derivative,
and imaginary limits sigma (3 beta/2) sign(u). The compact part remains
uniformly regular because the main angles stay away from zeros and z' is
uniformly bounded (Lemma 6.1). On far contours the denominator remains
regular and the same tail expansion bounds the log modulus above by
C e^{-c_2 |u|}. A numerator zero only improves this upper bound.
                                                        [end Lemma 6.2]

6.5 Positivity of the real energy (coercivity).
----------------------------------------

Setup. For a real vector of smooth rapidly decreasing densities
xi = (xi_I) assume weighted neutrality:

    int_R ( sum_I w_I xi_I ) du = 0.

Define

    d_xi = sum_I w_I xi_I,
    D(u) = int_{-inf}^u d_xi(v) dv,
    B(xi) = (1/2) (xi, Re H xi).

Use the inhomogeneous negative Sobolev norm

    ||xi_I||_{-1/2}^2
        = int_R (1 + k^2)^{-1/2} |xi_I_hat(k)|^2 dk / (2 pi).

THEOREM 6.3 (uniform real-energy coercivity). For the magnetic contours
there are constants 0 < c_2 < C_2 < inf such that

    c_2 ( ||D||_2^2 + sum_I ||xi_I||_{-1/2}^2 ) <= B(xi)
        <= C_2 ( ||D||_2^2 + sum_I ||xi_I||_{-1/2}^2 ).                  (6.15)

They are uniform in t in [1/2, 1] and in every sufficiently small positive
far-contour parameter eps. The form extends to the completion in this
norm.

The proof sweeps the curved X charge harmonically to the two edges of
the strip between heights beta/2 and beta. The boundary energy and the
remaining positive Green energy then control both the species norms
and the weighted total primitive.

STEP 1 (horizontal boundary lines). Allow independent X main charges on
the two boundary lines. This gives a translation-invariant system with
seven species (X main upper, X main lower, X far singleton, X far
double, Y main, Y far singleton, Y far double). At eps = 0 their
elementary height lists, in units of beta/8, are

    (4), (8), (25), (24, 32), (0), (-28), (-24, -32).                    (6.16)

        X species: first four;  Y species: last three.

Divide the real Fourier symbol by pi/(k sinh(pi k)), and divide its
IJ entry by w_I w_J. Expand the resulting matrix in
v = cosh(beta k / 8) - 1. Its constant matrix has every entry equal to
2, and every coefficient of degree 1 <= l <= 32 is strictly positive
definite. Two facts must be checked:

    (a) The coefficient of v^l in cosh(32 arcosh(1 + v)) is
        c_{32, l} = (2^l / (2 l)!) * prod_{a=0}^{l-1} (32^2 - a^2) > 0.

    (b) After dividing by c_{32, l}, define
            h_l(j) = prod_{a=0}^{l-1} (i_j^2 - a^2) / (32^2 - a^2),
            i_j = (j mod 64) - 32.
        For each pair of elementary heights, set j = |difference| and
        average over the two species' height lists:

            same group:     2 h_l(j) + h_l(j + 16) + h_l(j - 16)
                            - h_l(j - 8) - h_l(j + 8);
            opposite group: 2 ( h_l(j) + h_l(j + 16) - h_l(j + 8) ).

        These averages follow by summing the log-factor angles modulo
        2 pi = 8 beta. Denote the resulting symmetric matrix M_l.
        Show M_l is positive definite.

    The elementary-cosh coefficient formula follows from
    (2 v + v^2) y'' + (1 + v) y' = i_j^2 y.

For l <= 12, symmetric elimination gives successive pivots strictly
larger than the rational decimals displayed below (rows are species,
columns are l):


        l =         1    2    3    4    5    6    7     1 -- 7  (per row block)

        species 1   1   .7   .8   .27  .49  .59  .09
        species 2,3 1    1    1   .32  .80  .1   .30
        species 4-6 1.7  1.65 1.48 .35  1.53 1.65 .45
        species 7- 12 1.9 1.88 1.74 .35  1.89 1.88 .48

        (entries are LOWER bounds on pivots; for example, at l = 4
         every pivot in the row block exceeds .27)

These entries are obtained from EXACT rational substitution in the
Schur-complement recurrence

    m_ij^{(p)} = m_ij^{(p-1)}
                  - m_ip^{(p-1)} m_jp^{(p-1)} / m_pp^{(p-1)},

with i, j > p and M_l = (m_ij^{(0)}). Every one of these pivots is
strictly positive, so M_l is positive definite for 1 <= l <= 12.

For 13 <= l <= 32, each h_l(j) is nonnegative and nonincreasing in l:
before a zero occurs, every additional factor lies in [0, 1]; after
that zero, the product stays zero. Split the displayed averages into
positive and negative parts, M_l = P_l - Q_l. A lower bound for its
diagonal is diag(P_32 - Q_13), and an entrywise upper bound for the
absolute off-diagonal entries is

    max(P_13 - Q_32,  Q_13 - P_32).

Weight column j relative to row i by v_j / v_i, with v = (1,1,1,2,1,1,1).
Subtracting the weighted off-diagonal row sums from the diagonal lower
bounds gives EXACTLY

    ( 539085539017/288991072832, 153103458093/288991072832,
      6754920483/37289170688,   2413205499/288991072832,
      8798842243/4515485513,    496150561213/288991072832,
      32952783649/1155964291328 ).

All seven numbers are positive. Weighted strict diagonal dominance of
the symmetric M_l proves positive definiteness for every remaining
degree.

Assembly at small and large frequency. At small frequencies the
constant coefficient supplies the rank-one k^{-2} term for the
weighted total density D, and the strictly positive first coefficient
supplies a uniformly positive bounded term on all species. At large
frequencies the top coefficient supplies a positive multiple of
1/|k|, since pi = 4 beta. In between, continuity and positivity control
the frequency band. The real tail -w_I w_J |u - v| contributes exactly
||D||_2^2 to B. These observations prove the two-sided norm estimate
on the seven boundary-line species at eps = 0.

STEP 2 (uniform movement of the far double). The estimate continues
uniformly to sufficiently small eps > 0. At small frequencies use the
strict positive quadratic coefficient; on compact frequency intervals
use continuity. To check uniformity at infinite frequency, divide the
normalized symbol further by cosh(4 beta k). For 0 <= eps < 1/16 it
has the form

    diag(2, 2, 2, 1/2, 2, 2, 1/2) + q_eps(k) (E_{24} + E_{42})
        + O( e^{-c_3 |k|} ),
    q_eps(k) = cosh((4 - eps) beta k) / (2 cosh(4 beta k)).              (6.17)

Here E_ij is the elementary matrix, and the error is uniform in eps:
after collecting the elementary factors of each double, all other
contributing angles stay a fixed distance from zero modulo 8 beta. In
particular, the potentially small angles in the X-double/Y-double entry
cancel with total coefficient 2 - 4 + 2 = 0, for every eps. The
exceptional pair couples the X main line of height beta to the X
double, and 0 <= q_eps <= 1/2. The only nontrivial 2-by-2 block is

    [[2, q], [q, 1/2]],

with least eigenvalue at least (5 - sqrt(13))/4 > 0. This proves
uniform coercivity in every joint limit eps -> 0, |k| -> inf.

STEP 3 (harmonic sweeping to the boundary). Let
S = {z : beta/2 < Im z < beta}. Balayage the real charge on the graph
harmonically to the two edges of S. Leave all other species unchanged,
and denote the resulting seven-species charge by xi~.

All interactions are harmonic in this strip, in either variable away
from the source, with at most linear growth. The only interior source
in a graph self-interaction is

    -2 log| 2 sinh((z - z')/2) |,

with logarithmic singularity -2 log|z - z'|. Let G_S be the Dirichlet
Green kernel of -Delta, singularity -(2 pi)^{-1} log|z - z'|, and put

    G(xi_X) = int int G_S(z(u), z(v)) xi_X(u) xi_X(v) du dv.

Harmonic interpolation first in one variable and then in the other
gives the exact identity

    B(xi) = B_S(xi~) + 2 pi G(xi_X).                                    (6.18)

The coefficient 2 pi includes the factor 1/2 in B. Green energy is
nonnegative for signed real charges: by Dirichlet inversion and
integration by parts it is the squared dual norm of the charge acting
on traces of zero-boundary functions with gradient L^2-norm at most 1.
Harmonic measures in the strip decay exponentially; their Fourier
kernels are ratios of sinh(y k)/sinh(beta k / 2). These facts justify
the interpolations for rapidly decreasing densities and then by
completion.

STEP 4 (uniform control as the graph approaches an edge). We verify
that (6.18) gives exactly the claimed norm, even when the graph
approaches the upper edge.

Sobolev trace. The trace map H^1(R^2) -> H^{1/2}(R) on the graph and a
right inverse both have bounds depending only on its uniform Lipschitz
constant. Flatten the graph by a uniformly bilipschitz map. On a
horizontal line, the trace bound follows by transverse Fourier
Cauchy-Schwarz, and a right inverse extends a mode k by
exp(-sqrt(1 + k^2) |y|). Reflection across the strip edges with a
cutoff gives the same trace bound for strip functions. Harmonic
extension from the two boundaries is bounded H^{1/2} -> H^1; this follows
from the displayed Fourier kernels, or from the Dirichlet principle
with fixed strip width.

Duality. Duality bounds the two projected charges' H^{-1/2} norms by
the graph charge's norm. It also bounds the Green energy above by that
squared norm, since zero-boundary strip functions have their full H^1
norm controlled by their gradient.

Converse. Extend an arbitrary H^{1/2} test on the graph to the plane,
restrict to the strip, and decompose into its harmonic boundary
extension and a zero-boundary remainder. Pairing these two terms with
the charge gives

    ||xi_X||_{-1/2}^2 <= C_3 ( ||xi~_X(beta/2)||_{-1/2}^2
                              + ||xi~_X(beta)||_{-1/2}^2
                              + G(xi_X) ).                              (6.19)

Thus the Sobolev parts of the norms are equivalent in both directions,
with the Green term included.

Primitives. Let D~ be the primitive after projection. For a smooth
compactly supported function b, pair the horizontal marginal of the
difference between graph charge and projected charge with b. This
pairing equals that of the graph charge with b(u) minus the harmonic
extension of the same boundary value b on both edges. The latter
difference has zero boundary values and gradient norm at most
C_4 ||b'||_2: compare the harmonic extension to the constant-in-height
function b(u) by the Dirichlet principle. Green-energy duality, followed
by integration by parts in u, therefore yields

    ||D - D~||_2^2 <= C_5 G(xi_X).                                      (6.20)

Conclusion. Together with (6.18), STEP 1 boundary-line coercivity, and
the Sobolev norm comparisons (6.19)-(6.20), this proves both
inequalities in (6.15). Every constant depends only on the fixed strip
width and the uniform Lipschitz bounds, so remains uniform as the graph
reaches an edge, including the case t = 1.                       [end]


Note: typo "" on the real tail was corrected to "-|u|/2".
(documented; harmless.)
================================================================================
7. EXPLICIT PARTICLES AND THE TRIAL ACTION
================================================================================

7.1 Why we localize.
--------------------

The coercivity of Section 6 is a bound on the quadratic cost B(xi)
of a density vector xi. To convert it to a bound on correlation, we
combine it with three ingredients:

    - an exact reference law (Section 2.4) already converted to a
      measure of the form exp(-h_0(Q,Q)/2) dQ;

    - a TRIAL LOWER BOUND for the linear functional in the integrand,
      obtained by testing B with an explicit, energy-bounded field
      z (the "trial tilt");

    - a SMOOTHING step that absorbs the local quadratic cost into
      B(x) and leaves a decaying density for explicit particles.

We now specify the trial fields, then turn to smoothing.

7.2 Setup: species, weights, and final quantities.
--------------------------------------------------

Retain the magnetic contours of Section 6, their elementary
multiplicities w_I (1 for a singleton, 2 for a double label), and
the coercive real energy of Section 6.4. A double label is
implicitly the sum of its two elementary constituents when a kernel
is computed.

Write

    s_X = s,               s_Y = b,                  (7.1a)
    nu_bar_X = nu_X,       nu_bar_Y = rho,            (7.1b)
    beta = pi/4,           gamma = 4/3,               (7.1c)
    kappa = (3 beta)^2 = 9 pi^2 / 16,                 (7.1d)
    p = (3 - theta_infinity) beta.                    (7.1e)

Here p depends only on the bulk angle of the curved contour
(Lemma 6.1) and is fixed once t is fixed. It is NOT the marked port p
of Sections 3-4; the notation is unambiguous in context.

The two main labels are called X and Y; the subscript "n" means "the
pair (X, Y) of main labels". Throughout this section:

    c_1 L <= L_X <= L = L_Y,                          (7.2)

with L -> infinity, and c_1 > 0 fixed. Constants may depend on c_1.
An error written o(L), or o(1) B(x), is uniform over the stated
frozen configurations after all smoothing, localization, and
projection parameters have been fixed. When counts are restricted to
a fixed power of L, uniformity includes the positions and counts in
that restriction.

7.3 The trial action.
---------------------

Recall from Section 2.4: the reference probability measure is

    exp( - h_0(Q, Q) / 2 ) dQ / (normalizing constant),

where h_0 is the Dirichlet form of the reference sine basis.
We insert the two-mark insertion T of (4.4) and the two vacuum
denominators as in Section 4; the full marked correlation becomes a
positive high-dimensional integral of a certain complex Gaussian
type (Sections 3-4). The precise form is

    C(p,p') = (1/(h~_N^2 gamma^N)) * [some explicit prefactor]
              * int_{sector} e^{-F(Q)} dQ,             (7.3)

where the sector integral is over smooth real Dirichlet primitives
Q in X (the reference Hilbert space), and F is a specific quadratic
plus linear-plus-constant functional of Q that depends on the explicit
particle configuration zeta, its densities, and the tilts to be
introduced below.

Rather than restate the sector integral from scratch, we operate
entirely inside it via the "trial action" of the next paragraph.

Explicit particles. Write n_e for the total number of elementary
explicit particles (across the six species of Section 6.4), |M| for
the total elementary spin excess in X, and l_e for the sum of the
amplitudes |v| over explicit particles beyond L_Y. These quantities
are polynomially bounded in L after Section 8.5 (polynomial
truncation), and uniform bounds below may depend on the truncation
powers.

Smoothing kernel psi. Let psi be a probability density on R, symmetric
and smooth, with support in [-h, h] for a scale h to be chosen (small,
depending on eps). Write m'_g for the total mass of the smoothed
reference density on label g, and p_L for the physical main coordinate
of the reference law. The centered trial variable is

    x = Re alpha - mu + psi * zeta,                    (7.4a)
    z = Im alpha,                                       (7.4b)
    D' = sum_I w_I x_I,                                (7.4c)
    D_z' = sum_I w_I z_I,                              (7.4d)

where mu = (s nu_X, b rho) du is the reference mean on the two labels
(and mu_I = 0 on far labels) as in Section 6.4. The primitives
D = int d_xi and D_z = int d_z vanish at infinity; the main X component
of z has integral zero.

We shall refer to alpha as the complex trial field (a smooth Dirichlet
primitive of a rapidly decreasing density) and zeta as the frozen
explicit configuration.

Trial action. The trial action is

    D(alpha, zeta)
        = E(alpha, zeta)
          - (t_n, alpha - mu) - (t, zeta),              (7.5)

where

    E(alpha, zeta)
        = (1/2) (alpha - mu, H_nn (alpha - mu))
          + (alpha - mu, H_ne~ zeta)
          + (1/2) (zeta, H zeta)_off,                  (7.6)

the subscript "off" denotes omission of the individual explicit self
interactions, and t_n, t collect the single-mark particle logarithms
(both marked anomalies; see Section 6.4) as linear tests against alpha
and zeta respectively. All quantities z, t, t_n, and H_nn~ H_ne~
depend only on the frozen data (t, eps, h, and the explicit zeta).

The trial field z_I = z_I(u) = Im alpha_I(u) encodes an imaginary tilt
of the complex Gaussian trial, and the linear-in-z term - (t_n, z)
absorbs the marked anomalies exactly. A purely imaginary constant in z
(one common to all I, multiplied by w_I and summed) never affects the
bound on its real part, and we shall drop such constants.

7.4 Smoothing and count control.
--------------------------------

We absorb the local quadratic cost of the trial action into the
coercive real form, and, as a by-product, obtain quantitative control
of the explicit particles by cell test functions.

Smoothing kernel. Let h = h(eps) > 0 be a smooth symmetric probability
density psi with support in [-h, h], and write zeta^psi = psi * zeta
for the smoothed empirical density. The compensated kernel is

    H_ne~ = H_ne - H_ne * psi,                                       (7.7)

i.e., H_ne convolved with delta_0 - psi. The subtraction is inactive
whenever the explicit particle is at horizontal distance at least one
from the graph, and exponentially small otherwise.

LEMMA 7.1 (curved smoothing and count control). Let n_j be the local
explicit counts on the smoothing grids (one separate grid beginning at
each wall). Uniformly for sufficiently small eps > 0,

    sum_j n_j^2  <=  C (1 + |log h|) (B(x) + 1),                       (7.8a)
    l_e + (M^2 + n_e^2)/L  <=  C_h (B(x) + 1),                        (7.8b)

where l_e = sum_{v in zeta} ( |v| - L_Y )_+.

Proof sketch.
  (a) Positive count tests. For each far species use translates of a
      nonnegative bump covering a unit cell to test x_I = psi * zeta_I.
      For main X use a grid beginning at its own wall, with bumps
      supported outside that wall. The first bump rises from zero to
      one across distance h, remains 1 through distance 2, then cuts
      off. Every particle in the first cell contributes a fixed
      positive amount after smoothing. The squared H^{1/2} norm of a
      bump is O(1 + |log h|) (from the difference-quotient seminorm),
      and bounded overlaps give the same bound for linear combinations
      with the sum of squared coefficients. Mean cell masses are
      summable because s_g nu_bar_g(u) = O(1) at its own wall. Duality
      and coercivity (Section 6.5) then give (7.8a).

  (b) Mixed source smoothing. For the mixed error of H_ne~ vs H_ne psi
      paired against alpha - mu, the smoothing transform gives the
      Fourier bound C h^{c_2} (1 + |k|)^{-1} psi_hat(k) for the S_0
      term. For the decaying residuals, convolving in the explicit
      variable instead of evaluating at its point changes the kernel,
      as a test in the interior variable, by
          O(eps^{-C} h^{c_2} + o_L(1))
      in each localized H^{1/2}-norm, with exponential decay in the
      distance between unit cells. The first and mixed derivative
      bounds suffice by averaging shifts (the probability has small
      first moment and small exponential tails); when the explicit
      argument belongs to a curved same-main entry it starts beyond
      L_X, so to reach the exceptional neighborhood at zero it must
      shift by >= L_X, gaining exponential smallness against the
      polynomial localized norm there. Smooth real leading tail
      costs the same decaying smallness by even averaging and
      exponentially decaying second derivatives. The imaginary
      leading terms differ only by varying w_I v_J(v) in the
      convolution; this only pairs against z, summing with w_I and
      integrating by parts gains tanh' against D_z, so the small-error
      estimate uses just Lipschitz v_J.

  (c) Summing localized errors. If a_j, b_j are local negative Sobolev
      norms of two fields, the error is bounded by
          C eps_sm sum_{i,j} e^{-c|i-j|} a_i b_j.
      The matrix convolution e^{-c|i-j|} is bounded on l^2.
      Cauchy-Schwarz, coercivity, and (7.8a) give
          C eps_sm ( B(x) + B(z) + 1 ).
      The omitted diagonal costs one C (1 + |log h|) per explicit
      particle; it is never included in the off-diagonal estimate.

  (d) Diagonal smoothing identity. For the singular diagonal real
      summand S_0, smoothing can only decrease. Same localized
      residual estimates (only point values) give any same-curved-
      label explicit particle (both outside its wall) the log(2 cosh)
      tail, again at small decaying cost. On a same-variable smoothed
      diagonal, the underlying shifts remain regular uniformly after
      subtracting S_0, so the diagonal bound applies.         [end]

COROLLARY 7.2 (unshifted coercivity). Consequently, for z = 0,

    Re D(alpha, zeta)  >=  c B(x) - C_{h, eps} (L + n_e).              (7.9)

for small suitable h, eps, and some c > 0.

Proof. The two anomaly logs t_n subtracted in (7.5) cost an
arbitrarily small positive fraction of B(x) plus a constant depending
on parameters for their real parts (only a lower bound is needed):
use H^1 bounds on main components and decaying real upper bounds on
far components, via (7.8) and x = Re alpha - mu + psi * zeta. The
imaginary correction is exactly +(Im t_n, z). Choose h after eps so
that smoothing error is absorbed by the positive real form (Lemma
7.1). Equation (7.7) and the diagonal bound leave at most
C_{h, eps} n_e; the bounded anomaly terms are covered by
C_{h, eps} L.                                              [end]