diff 654c66f..f0945ea marked_polygon_one_arc_v2.txt
diff --git a/marked_polygon_one_arc_v2.txt b/marked_polygon_one_arc_v2.txt
index e69de29..80c6c54 100644
--- a/marked_polygon_one_arc_v2.txt
+++ b/marked_polygon_one_arc_v2.txt
@@ -0,0 +1,2036 @@
+================================================================================
+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.
+
+--------------------------------------------------------------------------------
+READER'S GUIDE
+--------------------------------------------------------------------------------
+
+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]
+