The box partition function of the six-vertex model is not given by the conjectured determinant

Abstract

The determinant formula conjectured by Kade for the partition function of the six-vertex model in a box with arrow-reflecting walls is false already for the smallest box: with one pair of horizontal and one pair of vertical spectral lines, crossing parameter 2, spectral parameters 2 and 3 and all boundary parameters 1, the partition function is -400400/81 while the formula gives -7150.

Definition 1.1 (The weight a).

$a (p, t) = p \cdot t - \frac{1}{p \cdot t}$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.a (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The weight of the two vertices whose arrows run straight through in the same sense, at crossing parameter p and spectral ratio t.

Definition 1.2 (The weight b).

$b (t) = t - \frac{1}{t}$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.b (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The weight of the two vertices whose arrows run straight through in opposite senses; it is also the building block of the wall weights.

Definition 1.3 (The weight c).

$c (p) = p - \frac{1}{p}$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.c (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The weight of the two vertices at which the arrows turn.

Definition 1.4 (Vertex weights).

$vertexWeight (p, t, r i g h t, r i g h t, u p, u p) = a (p, t), vertexWeight (p, t, l e f t, l e f t, d o w n, d o w n) = a (p, t), vertexWeight (p, t, l e f t, l e f t, u p, u p) = b (t), vertexWeight (p, t, r i g h t, r i g h t, d o w n, d o w n) = b (t), vertexWeight (p, t, r i g h t, l e f t, u p, d o w n) = c (p), vertexWeight (p, t, l e f t, r i g h t, d o w n, u p) = c (p), vertexWeight (p, t, h l, h r, v t, v b) = 0 otherwise$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.vertexWeight (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

At the crossing of a horizontal line with parameter x and a vertical line with parameter y the spectral ratio is t = x/y. The weight is a when all four arrows point right and up or all point left and down, b when the horizontal arrows point left and the vertical ones up or the horizontal ones right and the vertical ones down, c when the horizontal arrows point into the crossing and the vertical ones out of it or the reverse, and 0 for the ten configurations that break the ice rule.

Definition 1.5 (Left wall).

$leftWall (p, x, x i_{L}, r i g h t, l e f t) = b (x \cdot x i_{L}), leftWall (p, x, x i_{L}, l e f t, r i g h t) = b (\frac{x}{p \cdot x i _{L}}), leftWall (p, x, x i_{L}, e, f) = 0 otherwise$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.leftWall (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

A pair of horizontal lines ends at the left wall; the weight is b(x xi_L) when the upper edge points right and the lower edge left, b(x/(p xi_L)) for the reverse, and 0 otherwise.

Definition 1.6 (Right wall).

$rightWall (p, x, x i_{R}, l e f t, r i g h t) = b (x \cdot x i_{R}), rightWall (p, x, x i_{R}, r i g h t, l e f t) = b (\frac{x \cdot p}{x i _{R}}), rightWall (p, x, x i_{R}, e, f) = 0 otherwise$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.rightWall (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

A pair of horizontal lines starts at the right wall; the weight is b(x xi_R) when the upper edge points left and the lower edge right, b(x p/xi_R) for the reverse, and 0 otherwise.

Definition 1.7 (Top wall).

$topWall (p, y, x i_{U}, d o w n, u p) = b (y \cdot x i_{U}), topWall (p, y, x i_{U}, u p, d o w n) = b (\frac{y \cdot p}{x i _{U}}), topWall (p, y, x i_{U}, e, f) = 0 otherwise$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.topWall (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

A pair of vertical lines starts at the top wall; the weight is b(y xi_U) when the left edge points down and the right edge up, b(y p/xi_U) for the reverse, and 0 otherwise.

Definition 1.8 (Bottom wall).

$bottomWall (p, y, x i_{D}, u p, d o w n) = b (y \cdot x i_{D}), bottomWall (p, y, x i_{D}, d o w n, u p) = b (\frac{y}{p \cdot x i _{D}}), bottomWall (p, y, x i_{D}, e, f) = 0 otherwise$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.bottomWall (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

A pair of vertical lines ends at the bottom wall; the weight is b(y xi_D) when the left edge points up and the right edge down, b(y/(p xi_D)) for the reverse, and 0 otherwise.

Definition 1.9 (Line parameters).

$rowParam (x s, 2 \cdot i) = x_{i}, rowParam (x s, 2 \cdot i + 1) = \frac{1}{x _{i}}$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.rowParam (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

Counted from the top, the horizontal lines 2i and 2i + 1 carry x_i and 1/x_i; the vertical lines, counted from the left, carry y_j and 1/y_j in the same way.

Definition 1.10 (Column parameters).

$colParam (ys, 2 \cdot i) = y_{i}, colParam (ys, 2 \cdot i + 1) = \frac{1}{y _{i}}$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.colParam (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The vertical lines 2j and 2j + 1, counted from the left, carry y_j and 1/y_j.

Definition 1.11 (The box partition function).

$Z (M, p, x s, ys, x i_{L}, x i_{U}, x i_{R}, x i_{D}) = h \in (Fin (2 \cdot M) \to (Fin (2 \cdot M + 1) \to HArrow)), v \in (Fin (2 \cdot M) \to (Fin (2 \cdot M + 1) \to VArrow)) \sum i \in Fin (M) \prod (leftWall (p, x_{i}, x i_{L}, h (2 \cdot i, 0), h (2 \cdot i + 1, 0)) \cdot rightWall (p, x_{i}, x i_{R}, h (2 \cdot i, 2 \cdot M), h (2 \cdot i + 1, 2 \cdot M))) j \in Fin (M) \prod (topWall (p, y_{j}, x i_{U}, v (2 \cdot j, 0), v (2 \cdot j + 1, 0)) \cdot bottomWall (p, y_{j}, x i_{D}, v (2 \cdot j, 2 \cdot M), v (2 \cdot j + 1, 2 \cdot M))) r, s \in Fin (2 \cdot M) \prod vertexWeight (p, \frac{rowParam ( x s , r )}{colParam ( ys , s )}, h (r, s), h (r, s + 1), v (s, r), v (s, r + 1))$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.Z (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

A configuration h, v puts an arrow on each of the 2M + 1 segments of every horizontal line (segment 0 at the left wall, segment 2M at the right wall) and of every vertical line (segment 0 at the top wall, segment 2M at the bottom wall); x_i = xs(i) and y_j = ys(j). Its weight is the product of the wall weights of the M pairs of rows and the M pairs of columns and of the weights of the 4M^2 crossings, where the crossing of row r and column s sees the arrows h(r, s), h(r, s + 1) on its left and right and v(s, r), v(s, r + 1) above and below; the partition function is the sum over all configurations.

Definition 1.12 (The factor W).

$W (p, x, y) = a (p, x \cdot y) \cdot a (p, \frac{1}{x \cdot y}) \cdot a (p, \frac{x}{y}) \cdot a (p, \frac{y}{x})$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.W (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The unitarity factor of two crossing pairs of lines.

Definition 1.13 (The corner trace at the top left).

$FLU (p, x, x i_{L}, x i_{U}) = b (x \cdot x i_{L}) \cdot b (\frac{x \cdot p}{x i _{U}}) + b (\frac{x}{p \cdot x i _{L}}) \cdot b (x \cdot x i_{U})$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.FLU (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The sum over the two arrow states of the loop through the left and top walls.

Definition 1.14 (The corner trace at the bottom right).

$FDR (p, y, x i_{D}, x i_{R}) = b (y \cdot x i_{D}) \cdot b (\frac{y \cdot p}{x i _{R}}) + b (\frac{y}{p \cdot x i _{D}}) \cdot b (y \cdot x i_{R})$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.FDR (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The sum over the two arrow states of the loop through the bottom and right walls.

Definition 1.15 (The conjectured value).

$formula (M, p, x s, ys, x i_{L}, x i_{U}, x i_{R}, x i_{D}) = \frac{\prod _{i, j \in Fin (M)} (( \frac{x _{i}}{y _{j}} - \frac{y _{j}}{x _{i}} ) W ( p , x _{i} , y _{j} ) )}{\prod _{i < j, i, j \in Fin (M)} ( \frac{x _{j}}{x _{i}} - \frac{x _{i}}{x _{j}} ) ( \frac{y _{i}}{y _{j}} - \frac{y _{j}}{y _{i}} )} det_{i, j \in Fin (M)} (\frac{c ( p ) ^{2} \cdot a ( p , x _{i} \cdot y _{j} ) \cdot a ( p , \frac{1}{x _{i} \cdot y _{j}} ) \cdot FLU ( p , x _{i} , x i _{L} , x i _{U} ) \cdot FDR ( p , y _{j} , x i _{D} , x i _{R} )}{( \frac{x _{j}}{y _{i}} - \frac{y _{i}}{x _{j}} ) \cdot W ( p , x _{i} , y _{j} )})$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.formula (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

The product over all i, j of (x_i/y_j - y_j/x_i) W(x_i, y_j), divided by the product over i < j of (x_j/x_i - x_i/x_j)(y_i/y_j - y_j/y_i), times the determinant of the M by M matrix with entries c^2 a(x_i y_j) a(1/(x_i y_j)) F^LU(x_i) F^DR(y_j) / ((x_j/y_i - y_i/x_j) W(x_i, y_j)), as printed.

Definition 1.16 (The conjecture).

$c l aim \Leftrightarrow (\forall M \in N, \forall p, x i_{L}, x i_{U}, x i_{R}, x i_{D} \in C, \forall x s, ys \in (Fin (M) \to C), (\forall i, j \in Fin (M), ((p, x i_{L}, x i_{U}, x i_{R}, x i_{D}, x_{i}, y_{j} \neq = 0 \land \frac{x _{j}}{y _{i}} - \frac{y _{i}}{x _{j}} \neq = 0) \land W (p, x_{i}, y_{j}) \neq = 0) \land ((i < j) \Rightarrow ((\frac{x _{j}}{x _{i}} - \frac{x _{i}}{x _{j}}) \cdot (\frac{y _{i}}{y _{j}} - \frac{y _{j}}{y _{i}}) \neq = 0))) \Rightarrow (Z (M, p, x s, ys, x i_{L}, x i_{U}, x i_{R}, x i_{D}) = formula (M, p, x s, ys, x i_{L}, x i_{U}, x i_{R}, x i_{D})))$

Formalization. D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.claim (✓ std3).

Citation. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

For every M and all complex parameters at which no printed denominator vanishes (p, the x_i, the y_j and the four boundary parameters nonzero, x_j/y_i - y_i/x_j and W(x_i, y_j) nonzero for all i, j, and the factor for every i < j nonzero), the box partition function equals the conjectured value.

Theorem 1.17 (Refutation).

$\neg c l aim$

Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.result (✓ std3). ∎

Resolves. Problems/kade-2025-box-six-vertex-determinant-refutation (refuted) by D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.result.

Source. Repository-derived.

Acknowledgement. Moritz Kade (2025). Integrable systems: From the ice rule to supersymmetric fishnet Feynman diagrams. DOI: 10.18452/33769. URL: https://arxiv.org/abs/2509.03416v1.

Commentary.

Take M = 1, p = 2, x = 2, y = 3 and all four boundary parameters 1. Over the rationals the kernel sums the weights of all 4096 arrow configurations of the box and obtains -400400/81; the rational cast preserves every weight, so the complex partition function at this point is also -400400/81. There W(2, 3) = -4004/81 and 2/3 - 3/2 = -5/6 are nonzero, the product over i < j is empty, and the formula gives -7150.

References

Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.FDR
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.FLU
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.W
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.Z
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.a
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.b
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.bottomWall
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.c
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.claim
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.colParam
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.formula
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.leftWall
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.result
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.rightWall
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.rowParam
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.topWall
Truth anchor: D5/S3/StatisticalMechanics/VertexModels/KadeBoxBoundaryRefutation.vertexWeight