Signed completeness, proved for every cell: the kernel of law P^k is the span of the chains of the two other axes (dimension 4b·gcd(a,c) + 4c·gcd(a,b) − 4·gcd(a,b,c) + 2 for k = x); the joint system of the three laws and the bond rule has as solutions exactly the sums over chains of a weight times the chain’s own direction, n = ½ Σ g(C) u_C 1_C; the six direction indicators of a state with every hole oriented are sums over chains in which each chain carries two weights, each coupling two directions whose difference is parallel to the chain; the signed line fractions have six family profiles and do not add to a constant
2026-09-28
Status tags: proved (argument written out here in full), computed (exact, reproducible, no solver), solver (SAT verdict through h32_cap), conjecture. Scripts scratch_h/h440_lib.py to h448_dirsets.py (h449 unused). All work on the primary Mac, one heavy process at a time. No existing file was modified.
Notation. Cell \((a,b,c)\), coordinates modulo \((4a,4b,4c)\), \(N = 8abc\) vertices. \(\Lambda\) is the FCC lattice of translations of A, generated by the \(d_i - d_j\). For a chain family \(f = \{i,j\}\) the step is \(u_f = d_i - d_j\); so \(u_{01} = (0,2,2)\), \(u_{23} = (0,2,-2)\), \(u_{02} = (2,0,2)\), \(u_{13} = (2,0,-2)\), \(u_{03} = (2,2,0)\), \(u_{12} = (2,-2,0)\). \(g_{bc} = \gcd(b,c)\) and so on, \(g_3 = \gcd(a,b,c)\). \(\sigma_v = \pm 1\) on A and B.
Status table
| # | statement | tag |
|---|---|---|
| 1 | Theorem K (B1). On every cell, for each axis \(k\), the real solutions of law \(P^k\) (one equation per hole) are exactly the span of the indicators of the chains of the two axes other than \(k\) and the two sublattice constants. Only the antisymmetric constant is needed beyond the chains, and only at the trivial wavevector. | proved (hand, Fourier); computed on 20 cells × 3 axes |
| 2 | Dimension formula. \(\dim\ker P^x = 4b\,g_{ac} + 4c\,g_{ab} - 4g_3 + 2\), and cyclically. The chains of the two axes and the two constants satisfy exactly \(4g_3\) independent relations. | proved; computed on 20 cells × 3 axes |
| 3 | Wave-operator form. The symbol of \(P^x\) is a \(2\times2\) matrix \(M^x\) (A and B amplitudes) with \(\det M^x = x^{-4}\prod_{f}(\chi(u_f) - 1)\) over the four families of axes \(y\) and \(z\); eliminating B, \(K|_A\) is annihilated by the product of the four difference operators \(T_{u_f} - 1\) along the chain steps. \(M^x = 0\) exactly where both families of \(y\) or both of \(z\) are supported. | proved (hand); symbolic check computed (h442) |
| 4 | Theorem J (B2a). On every cell the real solutions of the joint system (three laws \(P^k\) on \(n_k\) and the bond rule on every bond) are exactly \(n = \tfrac12\sum_C g(C)\,u_C\,\mathbf 1_C\) with real weights \(g\): each chain carries its own step direction. No sublattice constant occurs. \(\dim = 4(a\,g_{bc} + b\,g_{ac} + c\,g_{ab}) - 4g_3 + 1\). | proved; computed on 22 cells |
| 5 | Sharing (B2a). A chain of axis \(x\) enters \(n_y\) and \(n_z\) with coefficients \((+1,+1)\) for family \(\{0,1\}\) and \((+1,-1)\) for \(\{2,3\}\) (similarly for \(y\), \(z\)). Unlike the types, where both families of an axis enter the two transverse indicators with \((+1,-1)\). | proved (part of 4) |
| 6 | (B2b). The three laws never imply the bond rule (on any cell). The bond rule implies the three laws on the cell \((1,1,1)\) and on no other cell. | proved; computed on 22 cells |
| 7 | Theorem D (B2c). In a frozen state with every hole oriented, each of the six direction indicators \(D_\delta\) is a sum over the chains through \(v\) of weights attached to (chain, pair of directions): each chain \(C\) carries two weights, one for each unordered pair \(\{\delta, \delta'\}\) of directions transverse to its axis with \(\delta - \delta' = \pm u_C/2\), entering \(D_\delta\) with \(+\) and \(D_{\delta'}\) with \(-\); plus constants \(\kappa_k/2 + \sigma_v\gamma_k/2\) on \(D_{\pm e_k}\). | proved, given (C) of the record and Lemma 3 |
| 8 | Every state of the odd corpus (1,357) and every sampled odd state on (2,2,4), (2,4,6), (4,4,6), (4,3,3) (48) satisfies the joint system, so lies in the span of the signed modes. | computed (corpus), solver + computed (samples) |
| 9 | No charged hole in the 48 sampled odd states on the four non-cubic cells. Consistent with Theorem U there; a sample, not a proof. | solver |
| 10 | (B3). In 62 sampled frozen states with even curl (45 of them with charged holes) on (3,3,3), (4,4,4), (4,3,3), (2,4,6): \(P^k K_k = 0\) and \(P^k n_k = c\) at every hole, for all three \(k\); \(n_k\) is in the span of Theorem K iff no hole is charged. | solver + computed; the “iff” is proved from Theorem K and Lemma 3 |
| 11 | Proposition O (B3). In a frozen state whose rods fill complete lines (every even-curl state), modulo the span of Theorem K, \(n_k \equiv u_k + \sum_\ell \rho_\ell \mathbf 1_\ell\), where \(u_k\) is the mean-zero antiderivative of the charges along each rod line of axis \(k\) and \(\rho\) (constant on \(k\)-lines) is any solution of a mixed-difference equation whose data are the total charges of the \(k\)-lines of holes. So the part outside the span is determined by the charges (with the positions of the charged holes on rod lines). | proved; checks T1, T4 computed on the 62 states |
| 12 | The simpler decomposition without \(\rho\) (line means are in the span) holds iff every \(k\)-line of holes has total charge zero; it fails in 106 of the 186 (state, axis) cases. | computed |
| 13 | Theorem F (B4). With every hole oriented, on A: \(\sigma_x = [U_{02}{+}U_{13}](y) + [W_{03}{+}W_{12}](z)\), \(\sigma_y = [F_{01}{+}F_{23}](x) + [W_{03}{-}W_{12}](z)\), \(\sigma_z = [F_{01}{-}F_{23}](x) + [U_{02}{-}U_{13}](y)\); on B the same six family profiles with the shifts \(F_{01}(x{-}1)\), \(F_{23}(x{+}1)\), \(U_{02}(y{-}1)\), \(U_{13}(y{+}1)\), \(W_{03}(z{-}1)\), \(W_{12}(z{+}1)\). So the B fractions are determined by the A fractions up to constants. The sum at a vertex of A is \(2F_{01}(x) + 2U_{02}(y) + 2W_{03}(z)\) + const. | proved (from Theorem J); computed on 1,357 + 65 oriented states, 0 exceptions |
| 14 | The sum \(\sigma_x + \sigma_y + \sigma_z\) is not constant in general (constant in 48 of 637 and 38 of 720 corpus states). There is no analogue of “the fractions add to one”. | computed |
| 15 | In every oriented state examined (1,357 + 65), at least one of the three coordinates has one of its two family profiles constant on A. Not explained. | computed, conjecture at most |
| 16 | (B5). On (4,3,3), (6,2,3), (5,2,4), up to the symmetries: a sublattice can carry every pattern of absent / one-way / two-way on at most two axes. No pattern with all three axes present occurs, which Theorem S already implies. | solver (60 queries, each with a satisfiable control) |
Nothing found contradicts the main loop’s claims. Refinements are listed at the end.
B1: the kernel of law \(P^k\)
The law at an A-hole
Let \(O = a + 2e_x\) with \(a \in\) A. The bridgeheads with \(s_x = -1\) are \(a + (1, s_y, s_z)\) with \(s_y s_z = +1\), that is \(a + d_0\) and \(a + d_1\). Those with \(s_x = +1\) are \(a + (3, s_y, s_z)\) with \(s_y s_z = -1\), that is \(a + 4e_x + d_2\) and \(a + 4e_x + d_3\). So law \(P^x\) at \(O\) reads \[K(a + 4e_x) - K(a) = K(a{+}4e_x{+}d_2) + K(a{+}4e_x{+}d_3) - K(a{+}d_0) - K(a{+}d_1). \tag{1}\] The inversion \(v \mapsto (1,1,1) - v\) exchanges A and B, maps holes to holes, reverses every \(s\) (and hence the product condition), maps each chain family to itself, and maps law \(P^x\) at a B-hole to law \(P^x\) at an A-hole. A permutation of the coordinates permutes \(\{d_0,\dots,d_3\}\), the families and the laws. So statements checked at A-holes for \(k = x\) hold at all holes and for all \(k\).
Lemma M (the modes solve the law; proved)
The indicator of a chain of axis \(y\) or \(z\) satisfies (1), and so do \(\mathbf 1_A\) and \(\mathbf 1_B\).
Proof. A B vertex \(b\) lies on a chain \(C\) of family \(\{i,j\}\) iff \(b - d_i \in C\) iff \(b - d_j \in C\). Take \(C\) of family \(\{0,2\}\). Then \(a + d_0 \in C\) iff \(a \in C\), and \(a + 4e_x + d_2 \in C\) iff \(a + 4e_x \in C\). Also \(a + d_1 \in C\) iff \(a + d_1 - d_0 = a - (0,2,2) \in C\), and \(a + 4e_x + d_3 \in C\) iff \(a + 4e_x + d_3 - d_2 = a + (4,-2,2) \in C\). These two points differ by \((4,0,4) = 2u_{02}\), so the last two terms of (1) cancel and (1) holds. The other three families are the same computation. For \(\{1,3\}\) the pairs are \((a+d_1, a)\), \((a+4e_x+d_3, a+4e_x)\), and \(a + (0,2,2)\) against \(a + (2,2,0)\), which differ by \(u_{13}\). For \(\{0,3\}\) they are \((a+d_0, a)\), \((a+4e_x+d_3, a+4e_x)\), and \(a - (0,2,2)\) against \(a + (2,0,-2)\), which differ by \(u_{03}\). For \(\{1,2\}\) they are \((a+d_1, a)\), \((a+4e_x+d_2, a+4e_x)\), and \(a + (0,2,2)\) against \(a + (2,0,2)\), which differ by \(u_{12}\). For \(\mathbf 1_A\), both sides of (1) vanish at an A-hole. At a B-hole the methylene difference is 0 and the four bridgeheads have \(\sum_s s_x = 0\). \(\square\)
(Also checked by the exact product law × modes = 0 on 20 cells in h441, and symbolically in h442 (3).)
Fourier reduction (proved)
Let \(G = \Lambda / (4a\mathbb Z \times 4b\mathbb Z \times 4c\mathbb Z)\), of order \(4abc\). For each character \(\psi\) of \(G\) fix an extension \(\chi(p) = x^{p_1}y^{p_2}z^{p_3}\) with \(x^{4a} = y^{4b} = z^{4c} = 1\). The functions \(e_{\chi,A} = \chi\cdot\mathbf 1_A\) and \(e_{\chi,B} = \chi\cdot\mathbf 1_B\), one extension per \(\psi\), form a basis of \(\mathbb C^V\). Every system below has integer coefficients and is invariant under \(\Lambda\), and it has one orbit of rows per hole sublattice (and per bond direction), so it maps the plane \(\langle e_{\chi,A}, e_{\chi,B}\rangle\) into the corresponding character space on rows, through a small matrix \(M(\chi)\). Hence \(\ker = \bigoplus_\psi \ker M(\chi)\). The span \(W\) of the modes is \(\Lambda\)-invariant, so \(W = \bigoplus_\psi W_\psi\), and \(W_\psi\) is spanned by the \(\psi\)-projections of the generators. The projection of \(\mathbf 1_C\), for \(C\) of family \(f = \{i,j\}\) based at \(p_0\), vanishes unless \(\chi(u_f) = 1\), and is then \(\bar\chi(p_0)\,|C\cap A|/|A| \cdot (1, 1/\lambda_i)\) with \(\lambda_i := \chi(d_i)\). The constants \(\mathbf 1_A\) and \(\mathbf 1_B\) project to \((1,0)\) and \((0,1)\) at \(\psi = 1\) only. Integer coefficients make the real statement follow from the complex one. So it suffices to show \(\ker M(\chi) = W_\psi\) for every \(\psi\).
Lemma P (the partition; proved). Since \(u_f = d_i - d_j\), \(\chi(u_f) = \lambda_i/\lambda_j\), so \(f\) is supported at \(\psi\) iff \(\lambda_i = \lambda_j\). The set \(Z(\psi)\) of supported families is the set of pairs inside the blocks of the partition of \(\{0,1,2,3\}\) by the value of \(\lambda\). There are five cases. All distinct: \(Z = \emptyset\). One pair: one family. Two pairs: the complementary pairs \(\{01,23\}\), \(\{02,13\}\), \(\{03,12\}\) are exactly the two families of \(x\), \(y\), \(z\). A triple \(\{0,1,2,3\}\setminus\{\ell\}\): three families, one of each axis, those of the kagome plane \(\perp d_\ell\). All four equal: then \(\chi\) is trivial on \(\Lambda\) (generated by the \(d_i - d_j\)), so \(\psi = 1\). (This replaces the Hermite normal form classification of the report of 17 September by one line.)
The symbol of \(P^x\) (proved). Rows are the A-hole and B-hole laws, columns \((\mathrm{amp}_A, \mathrm{amp}_B)\): \[M^x = \begin{pmatrix} D & -U \\ -V & D\end{pmatrix},\quad D = x^2 - x^{-2},\quad U = \sum_{\prod s = -1} s_x\chi(s) = xp - q/x,\quad V = \sum_{\prod s = +1} s_x\chi(s) = xq - p/x,\] with \(p = y/z + z/y\) and \(q = yz + 1/(yz)\). Put \(X_m = m^2 + m^{-2}\). Then \(pq = X_y + X_z\), \(p^2 + q^2 = 4 + X_yX_z\), \(UV = pqX_x - p^2 - q^2\) and \(D^2 = X_x^2 - 4\), so \[\det M^x = D^2 - UV = (X_x - X_y)(X_x - X_z).\] Also \(X_x - X_z = x^{-2}(x^2z^2 - 1)(x^2z^{-2} - 1) = x^{-2}(\chi(u_{02}) - 1)(\chi(u_{13}) - 1)\), and in the same way \(X_x - X_y = x^{-2}(\chi(u_{03}) - 1)(\chi(u_{12}) - 1)\). So \(\det M^x \neq 0\) iff no family of axis \(y\) or \(z\) is supported. This is item 3. Eliminating \(\mathrm{amp}_B\) gives \((D^2 - UV)K_A = 0\) as an operator identity, which is the “wave equation” form. It is a product of four difference operators \(T_{u_f} - 1\) (times a shift), applied to the restriction to A. It is not a factorisation of \(P^x\) itself, and the kernel of the product is the sum of the kernels of the factors only because all these operators are diagonal on \(G\).
When \(M^x = 0\) (proved). \(D = 0\) iff \(x^2 = \varsigma \in \{\pm1\}\). Then \(xyz\,U = \varsigma y^2 + \varsigma z^2 - y^2z^2 - 1 = -(y^2-\varsigma)(z^2-\varsigma)\) and \(xyz\,V = \varsigma(y^2z^2+1) - y^2 - z^2 = \varsigma(y^2-\varsigma)(z^2-\varsigma)\). So \(M^x = 0\) iff \(x^2 = y^2 = \varsigma\) or \(x^2 = z^2 = \varsigma\). The first says \(\chi(u_{03}) = x^2y^2 = 1\) and \(\chi(u_{12}) = x^2y^{-2} = 1\), both families of \(z\). Conversely both families of \(z\) give \(y^4 = 1\) and \(x^2 = y^2 = \pm1\). So \(M^x = 0\) iff both families of \(y\) or both families of \(z\) are supported.
Proof of Theorem K. Fix \(\psi\). By Lemma M every supported mode vector lies in \(\ker M^x(\chi)\), and it is nonzero (first entry 1). (i) No family of \(y\) or \(z\) is supported: \(\det \neq 0\), so \(\ker = 0 = W_\psi\) (the constants occur only at \(\psi = 1\), where every family is supported). (ii) Some are supported but not both of one axis: \(M^x \neq 0\) and \(\det = 0\), so \(\dim\ker = 1\), spanned by any supported mode. (iii) Both families of \(y\) are supported (or of \(z\)), say \(f = \{0,2\}\), \(f' = \{1,3\}\): \(M^x = 0\) and \(\ker = \mathbb C^2\). The modes are \((1, 1/\lambda_0)\) and \((1, 1/\lambda_1)\). They are independent unless \(\lambda_0 = \lambda_1\), which together with \(\lambda_0 = \lambda_2\), \(\lambda_1 = \lambda_3\) makes all four equal, so \(\psi = 1\). There the constants give \((1,0)\) and \((0,1)\). In every case \(\ker M^x(\chi) = W_\psi\). \(\square\)
Proof of the dimension formula. \(\dim\ker = \#\{\psi: \det = 0\} + \#\{\psi: M^x = 0\}\). Write \(\alpha, \beta, \gamma, \delta\) for the conditions \(\chi(u_{02}), \chi(u_{13}), \chi(u_{03}), \chi(u_{12}) = 1\). The number of \(\psi\) satisfying a set of conditions is \(|G|\) divided by the order of the subgroup of \(G\) generated by the corresponding steps. - One condition: \(\langle(2,0,\pm2)\rangle\) has order \(2\,\mathrm{lcm}(a,c)\), giving \(2b\,g_{ac}\) characters, which is the number of chains of the family. Likewise \(2c\,g_{ab}\) for the \(z\) families. - \(\alpha\beta\): the subgroup \(\{(2p,0,2q): p \equiv q \bmod 2\}\) has order \(2ac\), giving \(2b\) characters. \(\gamma\delta\) gives \(2c\). - A cross pair, for example \(\alpha\gamma\): the two steps span \(P_1 = \Lambda\cap d_1^\perp\). Now \(v \mapsto v\cdot d_1/4\) maps \(\Lambda\) onto \(\mathbb Z\) with kernel \(P_1\) and sends the cell periods to \(a, -b, -c\), so \(\Lambda/(P_1 + \text{periods}) \cong \mathbb Z/g_3\) and there are \(g_3\) characters. The four cross pairs are the four kagome planes. - Any three conditions include both families of one axis and one of another, which forces the fourth (for example \(\delta = \alpha\beta/\gamma\)). With all four, \(\psi = 1\), a single character.
By inclusion and exclusion, \(\#\{\det = 0\} = (4b\,g_{ac} + 4c\,g_{ab}) - (2b + 2c + 4g_3) + 4 - 1\) and \(\#\{M = 0\} = 2b + 2c - 1\). The sum is \(4b\,g_{ac} + 4c\,g_{ab} - 4g_3 + 2\). The generators number \(4b\,g_{ac} + 4c\,g_{ab} + 2\), so there are \(4g_3\) relations: one at each non-trivial \(\psi\) of the four kagome planes (\(4(g_3-1)\)) and four at \(\psi = 1\) (six vectors in \(\mathbb C^2\)). \(\square\)
B1 computations (h441_kernel.py; exact ranks modulo \(2^{31}-1\))
Soundness: rank mod \(p \le\) rank over \(\mathbb Q\). So \(N - \mathrm{rank}_p(P^k) \ge \dim\ker\) and \(\mathrm{rank}_p(\text{modes}) \le \dim\text{span}\). The script checks law × modes \(= 0\) over \(\mathbb Z\), so span \(\subseteq\) ker. Equality of the two numbers therefore proves ker = span on the cell.
| cell | coprime pair | \(\dim\ker P^x, P^y, P^z\) | = span? | formula |
|---|---|---|---|---|
| (1,1,2) | yes | 10, 10, 6 | yes | ok |
| (1,2,2) | yes | 14, 14, 14 | yes | ok |
| (1,1,5) | yes | 22, 22, 6 | yes | ok |
| (1,2,3) | yes | 18, 14, 10 | yes | ok |
| (2,2,2) | none | 26, 26, 26 | yes | ok |
| (2,2,3) | yes | 30, 30, 14 | yes | ok |
| (2,2,4) | none | 42, 42, 26 | yes | ok |
| (1,5,5) | yes | 38, 38, 38 | yes | ok |
| (4,4,4) | none | 114 ×3 | yes | ok |
| (4,3,3) | yes | 22, 58, 58 | yes | ok |
| (6,2,3) | yes | 46, 46, 46 | yes | ok |
| (5,2,4) | yes | 22, 54, 46 | yes | ok |
| (3,4,4) | yes | 30, 62, 62 | yes | ok |
| (2,4,6) | none | 74, 58, 42 | yes | ok |
| (5,3,3) | yes | 22, 70, 70 | yes | ok |
| (4,4,6) | none | 122, 122, 58 | yes | ok |
| (6,2,9) | yes | 94, 94, 46 | yes | ok |
| (5,4,4) | yes | 30, 94, 94 | yes | ok |
| (6,3,4) | yes | 70, 70, 46 | yes | ok |
| (7,3,6) | yes | 34, 106, 94 | yes | ok |
Also (3,3,3): 62 ×3, (1,1,1): 6 ×3, (2,3,3): 22, 34, 34. The chain counts \(2E_i\,\gcd(E_j,E_l)\) per family were asserted on every cell. 60 of 60 (cell, axis) pairs are equal, with no extra solutions anywhere, thin cells (extent 1 or 2) included.
B2: the joint system
The signed modes (proved). For a chain \(C\) of family \(f=\{i,j\}\) put \(n = \tfrac12 u_f\) on its vertices and 0 elsewhere. Distinct \(d\)’s have \(d_m\cdot d_{m'} = -1\), so \(d_m\cdot u_f = 0\) for \(m \notin f\), while \(d_i\cdot u_f = 4\) and \(d_j\cdot u_f = -4\). The bond rule on a bond of direction \(d_m\) with one end or both in \(C\): if \(m \notin f\) both sides are 0; if \(m \in f\) both ends are in \(C\) and both sides equal \(\tfrac12 d_m\cdot u_f\). The component of \(u_f\) along the chain’s own axis is 0, and each other component is a multiple of \(\mathbf 1_C\), which solves the law of that axis by Lemma M. So the mode solves the joint system. In coordinates, \(\tfrac12u_{01} = (0,1,1)\), \(\tfrac12u_{23} = (0,1,-1)\), \(\tfrac12u_{02} = (1,0,1)\), \(\tfrac12u_{13} = (1,0,-1)\), \(\tfrac12u_{03} = (1,1,0)\) and \(\tfrac12u_{12} = (1,-1,0)\). (I first derived these as the vectors orthogonal to the two \(d_m\) off the chain, and only then noticed that they are the chain steps.)
Proof of Theorem J. Symbol per \(\psi\): unknowns \((n_A, n_B) \in \mathbb C^3\times\mathbb C^3\). Law rows: \((n_{A,k}, n_{B,k}) \in \ker M^k(\chi)\) for each \(k\). Bond rows: \(d_r\cdot n_A = \lambda_r\, d_r\cdot n_B\), \(r = 0,\dots,3\). The mode of \(f\) projects to \((u_f, u_f/\lambda_i)\). Cases by Lemma P: - All distinct: every \(\det M^k \neq 0\), so the kernel is 0. - One pair \(f = \{i,j\}\) of axis \(m\): \(n_m = 0\) (no family of the other axes). For \(k \neq m\), \(\ker M^k\) is the line of \((1, 1/\lambda_i)\), so \(n_B = n_A/\lambda_i\). The bond rows become \(d_r\cdot n_A(1 - \lambda_r/\lambda_i) = 0\). For \(r \notin f\), \(\lambda_r \neq \lambda_i\), so \(n_A \perp d_r\) for both \(r \notin f\) and \(n_A \in \mathbb C u_f\). The kernel is 1-dimensional and spanned by the mode. - Two pairs, both families of axis \(m\) with values \(\alpha \neq \beta\): \(n_m = 0\) and, for \(k \neq m\), \(M^k = 0\), so the \(m\)-free components are unconstrained by the laws. Taking \(m = x\): \(d_0, d_1\) project to \(\pm(0,1,1)\) and \(d_2, d_3\) to \(\pm(0,1,-1)\) in the \(yz\) plane, and the bond rows reduce to \((n_A - \alpha n_B)\cdot(0,1,1) = 0\) and \((n_A - \beta n_B)\cdot(0,1,-1) = 0\). That is two independent equations on four unknowns, so the kernel is 2-dimensional. The two modes lie in it and are independent. - A triple \(\{0,1,2,3\}\setminus\{\ell\}\) with common value \(\mu \neq \lambda_\ell\): for each \(k\) the two supported families of the other axes lie on different axes, so \(M^k \neq 0\) and \(\ker M^k\) is the line of \((1, 1/\mu)\). Hence \(n_B = n_A/\mu\) with \(n_A \in \mathbb C^3\). The rows \(r \neq \ell\) hold automatically and row \(\ell\) gives \(n_A \perp d_\ell\). The kernel is 2-dimensional and spanned by the three modes \(u_f \perp d_\ell\) (any two of which are independent). - All equal (\(\psi = 1\), \(\lambda_r = \lambda\)): all \(M^k = 0\) and the bond rows give \(n_A = \lambda n_B\). The kernel is 3-dimensional and spanned by the six \(u_f\).
So the kernel equals the span of the signed modes at every \(\psi\). No sublattice constant is needed: at \(\psi = 1\) the antisymmetric constant is killed by the bond rule. Dimension: the chains number \(4(a\,g_{bc} + b\,g_{ac} + c\,g_{ab})\), with one relation at each non-trivial kagome \(\psi\) (\(4(g_3-1)\) in all) and three at \(\psi = 1\), which gives \(4(a\,g_{bc} + b\,g_{ac} + c\,g_{ab}) - 4g_3 + 1\). \(\square\)
In components, with \(G_f(v)\) the weight of the chain of family \(f\) through \(v\): \[n_x = G_{02} + G_{13} + G_{03} + G_{12},\quad n_y = G_{01} + G_{23} + G_{03} - G_{12},\quad n_z = G_{01} - G_{23} + G_{02} - G_{13}.\] Compare the types: \(K_y = G^T_{01} + G^T_{23} - G^T_{03} - G^T_{12} + \sigma\alpha\) and so on, where both families of an axis enter the two transverse types with signs \((+,-)\). For the signs the two families of an axis differ: \((+,+)\) for \(\{0,1\}\), \(\{0,2\}\), \(\{0,3\}\) and \((+,-)\) for \(\{2,3\}\), \(\{1,3\}\), \(\{1,2\}\), in the component order \((y,z)\), \((x,z)\), \((x,y)\). So the answer to “do they share weights in the same way” is: in another way. Each chain has one signed weight, and it enters both transverse components.
(B2b) proof. Per \(\psi\) the bond rule alone forces \(n_A\) once \(n_B\) satisfies \(\sum_r\lambda_r(d_r\cdot n_B) = 0\). The rows \(d_r\) satisfy only \(\sum d_r = 0\), so \(D n_A\) must have coordinate sum 0. The kernel is therefore 2-dimensional unless \(\sum_r\lambda_r d_r = 0\), which (the \(d_r\) having that one relation) means all \(\lambda_r\) are equal, \(\psi = 1\), where it is 3-dimensional. So \(\dim\ker(\text{bond}) = N + 1\) on every cell. The joint kernel is smaller exactly at the \(\psi\) with all \(\lambda\) distinct (0 against 2) or exactly one pair (1 against 2). At \(\psi = 1\) the laws alone allow 6 and the joint system 3, so the laws never imply the bond rule. The bond rule implies the laws iff the cell has no \(\psi\) of the first two kinds. On \((1,1,1)\) the four \(\psi\) are the trivial one and three of type “two pairs” (h443), so it does. If some extent, say \(c\), is at least 2, then \(\chi = (i, 1, \zeta)\) with \(\zeta = e^{2\pi i/4c}\) is admissible, and \(\lambda = (i\zeta, i/\zeta, -i/\zeta, -i\zeta)\) are distinct because \(\zeta^2 \neq \pm1\). So every other cell has a generic \(\psi\). \(\square\)
B2 computations (h443_joint.py)
Exact ranks of JOINT, LAWS and BOND. Independently, every one of the \(64abc\) lifted characters is enumerated with rational exponents, its partition is classified, and the predicted dimensions are summed from the case analysis above. That second count tests every per-\(\psi\) claim in aggregate.
| cell | ker JOINT | span of modes | formula | Fourier count | ker LAWS | ker BOND | bond ⇒ laws |
|---|---|---|---|---|---|---|---|
| (1,1,1) | 9 | 9 | 9 | 9 | 18 | 9 | yes |
| (1,1,2) | 13 | 13 | 13 | 13 | 26 | 17 | no |
| (1,1,3) | 17 | 17 | 17 | 17 | 34 | 25 | no |
| (1,1,5) | 25 | 25 | 25 | 25 | 50 | 41 | no |
| (1,2,2) | 21 | 21 | 21 | 21 | 42 | 33 | no |
| (1,2,3) | 21 | 21 | 21 | 21 | 42 | 49 | no |
| (1,3,3) | 33 | 33 | 33 | 33 | 66 | 73 | no |
| (1,5,5) | 57 | 57 | 57 | 57 | 114 | 201 | no |
| (2,2,2) | 41 | 41 | 41 | 41 | 78 | 65 | no |
| (2,2,3) | 37 | 37 | 37 | 37 | 74 | 97 | no |
| (2,2,4) | 57 | 57 | 57 | 57 | 110 | 129 | no |
| (3,3,3) | 97 | 97 | 97 | 97 | 186 | 217 | no |
| (4,4,4) | 177 | 177 | 177 | 177 | 342 | 513 | no |
| (4,3,3) | 69 | 69 | 69 | 69 | 138 | 289 | no |
| (6,2,3) | 69 | 69 | 69 | 69 | 138 | 289 | no |
| (5,2,4) | 61 | 61 | 61 | 61 | 122 | 321 | no |
| (3,4,4) | 77 | 77 | 77 | 77 | 154 | 385 | no |
| (2,4,6) | 89 | 89 | 89 | 89 | 174 | 385 | no |
| (5,3,3) | 81 | 81 | 81 | 81 | 162 | 361 | no |
| (4,4,6) | 153 | 153 | 153 | 153 | 302 | 769 | no |
| (5,4,4) | 109 | 109 | 109 | 109 | 218 | 641 | no |
| (6,3,4) | 93 | 93 | 93 | 93 | 186 | 577 | no |
“Laws ⇒ bond” is false on all 22. Only the partition counts 0, 1, 2, 3 and 6 pairs occurred (the script would stop on any other), which confirms Lemma P on these cells.
Theorem D, the six directions (proved, given (C) and Lemma 3)
Let a frozen state have every hole oriented. By (C) (report of 17 September, confirmed by check4), \(K = \sum_C f(C)\,t_C + \kappa + \sigma_v\gamma\) with type modes \(t_C = e_y - e_z\), \(e_z - e_x\), \(e_x - e_y\) for chains of axis \(x\), \(y\), \(z\), \(\kappa = (1,0,0)\) and \(\gamma = (-\alpha-\beta, \alpha, \beta)\). By Lemma 3, \(n\) solves the joint system, so by Theorem J \(n = \tfrac12\sum_C g(C)\,u_C\). For a chain \(C\) of axis \(m\), the transverse directions split into two unordered pairs \(\pi = \{\delta, \delta'\}\) with \(\delta - \delta' = \pm\tfrac12u_C\). For \(\{0,1\}\) these are \(\{+e_y, -e_z\}\) and \(\{+e_z, -e_y\}\); for \(\{2,3\}\) they are \(\{+e_y, +e_z\}\) and \(\{-e_y, -e_z\}\). Orient each pair so that \(\delta - \delta' = +\tfrac12u_C\) and give it the weight \(a_\pi(C)\). The pair mode (\(+a\) on \(D_\delta\), \(-a\) on \(D_{\delta'}\)) contributes \(a(e_{\tau(\delta)} - e_{\tau(\delta')})\) to \(K\) and \(a\,u_C/2\) to \(n\). With \(a_{\pi_1} = (f+g)/2\) and \(a_{\pi_2} = (g-f)/2\) (for family \(\{0,1\}\), \(\pi_1 = \{+y,-z\}\) and \(\pi_2 = \{+z,-y\}\); the other families alike), the sum over the two pairs reproduces \(f(C)t_C\) and \(\tfrac12g(C)u_C\). Therefore \[D_\delta(v) = \sum_{C\ni v}\ \sum_{\pi\ni\delta,\ \pi\text{ a pair of }C} \pm a_\pi(C) + \tfrac12\kappa_{k} + \tfrac12\sigma_v\gamma_{k}\qquad(\delta = \pm e_k),\] with sign \(+\) when \(\delta\) is the leading member. Each weight is shared by exactly two directions whose difference is parallel to the chain, in the way that a type weight is shared by the two transverse types. Explicitly, with \(h_\pm = (f\pm g)/2\) per chain: \(p_y = h_+^{01} + h_+^{23} - h_-^{03} - h_+^{12} + \tfrac12\sigma\alpha\) and \(m_y = h_-^{01} + h_-^{23} - h_+^{03} - h_-^{12} + \tfrac12\sigma\alpha\) (superscripts give the family of the chain through \(v\)), and cyclically. The weights are real, not unique (the relations of Theorems K and J), and nothing here says anything about integrality. The statement is linear. It does not encode \(|n_k| = K_k\).
B3: states that are not odd
h444_even.py uses the type model with T2, the sign field and every hexagon even. For each cell there are 8 plain queries with random assumptions and 8 queries per axis with an unoriented cage forced at the A-hole \((2,0,0)\) (both orders of the bridgehead types). Each cell is one solver process with a 300 s cap.
| cell | queries | SAT / UNSAT | distinct states | charged states | violations |
|---|---|---|---|---|---|
| (3,3,3) | 32 | 21 / 11 | 18 | 12 | 0 |
| (4,4,4) | 32 | 18 / 14 | 17 | 12 | 0 |
| (4,3,3) | 32 | 15 / 17 | 15 | 11 | 0 |
| (2,4,6) | 32 | 12 / 20 | 12 | 10 | 0 |
The violations column counts three checks per state and axis, all exact: \(P^kK_k = 0\) at every hole; \(P^kn_k = c\) at every hole; and \(n_k\) in the span iff \(c \equiv 0\) (rank test). All charges are \(\pm2\). Charged holes, 24 to 256 of them per state, occur in plain samples too. So at a charged hole \(n_k\) fails the law by exactly \(c(O)\) on every axis \(k\), including axes other than that of the hole’s rods. For example, in state plain_7 on (3,3,3) every rod line of axis \(x\) has one sign, yet \(n_x\) is not in the span.
Proposition O (proved). Let every rod line be complete (Lemma 1: every even-curl state). For a rod line \(\ell\) of axis \(k\) and a hole \(O\) on it, the charge formula gives \(c(O) = \varepsilon(O{+}2e_k) - \varepsilon(O{-}2e_k)\), the jump of \(n_k\) along \(\ell\) (T1). Let \(u_k\) be, on each rod line of axis \(k\), the antiderivative of these jumps normalised to mean zero on the line, and 0 elsewhere. Then \(n_k - u_k = \sum_\ell \bar n_\ell \mathbf 1_\ell\), where \(\bar n_\ell\) is the mean of \(n_k\) on the \(k\)-line \(\ell\). Any function on one sublattice that depends on one transverse coordinate lies in \(\ker P^k\): at holes of the same sublattice the methylene difference vanishes, and at holes of the other sublattice the two bridgeheads with a given transverse coordinate have opposite \(s_k\). So by Theorem K it lies in the span, and hence so does \(\sum_\ell F(\ell)\mathbf 1_\ell\) for every separable \(F\). On the torus a function on the grid of lines is separable iff all its mixed second differences vanish. By Theorem 5 of the note, the mixed second difference of \(\bar n\) around a \(k\)-line of holes is \(\mp\) its total charge divided by the line length. Hence \(n_k \equiv u_k + \sum_\ell\rho_\ell\mathbf 1_\ell\) modulo the span, for any \(\rho\) with those prescribed mixed differences. The data are the jumps on the rod lines of axis \(k\) and the line totals of the charges. \(\square\)
Checks (h445_outside.py). T1 (jump law) held in 186 of 186 (state, axis) cases. “The line means are in the span” failed in 106 of 186, and it fails exactly when some \(k\)-line of holes has nonzero total charge (T4, 0 exceptions). The simpler description, \(n_k \equiv u_k\) from the charges on rod lines alone, is therefore wrong in general, and the correction term \(\rho\) is needed.
B4: the signed line fractions
Proof of Theorem F. Average \(n_k = \sum_f (\tfrac12u_f)_k G_f\) along the \(k\)-line through \(v\). A chain of family \(\{0,1\}\) has constant \(x\) and constant \(y - z\) modulo \(4g_{bc}\) on each sublattice. Moving along a \(y\)-line or a \(z\)-line through \(v\) changes \(y - z\) by multiples of 4, so it meets every chain of the family in the pair of planes of \(v\) equally often. The average of \(G_{01}\) is therefore \(F_{01}\), the mean weight of the \(\{0,1\}\) chains whose A-plane is \(x\) (for \(v \in\) A) or \(x - 1\) (for \(v \in\) B, since \(d_0\) has \(x\)-component \(+1\)). For \(\{2,3\}\) it is \(x + 1\) on B (\(d_2\) has \(x\)-component \(-1\)). The other families work the same way. Substituting the components of \(\tfrac12u_f\) gives the formulas of item 13. \(\square\)
So the three signed fractions carry six family profiles, two per coordinate. On one sublattice the \(x\)-profiles of \(\sigma_y\) and \(\sigma_z\) are the sum and the difference of \(F_{01}\) and \(F_{23}\). They are not tied to each other, but they tie A to B: given the A fractions, the B fractions are determined up to additive constants. The sum at a vertex is \(2F_{01}(x) + 2U_{02}(y) + 2W_{03}(z)\) + const on A, shifted on B, and it is not constant. The direction fractions are \((h_k/\ell_k \pm \sigma_k)/2\), separable in the same two coordinates.
Checks (h446_fractions.py; exact, Fractions). Test S is separability of each \(\sigma_k\) on each sublattice. Test L is that the B profiles are the predicted shifts of the family profiles read off A, up to constants. Test Σ is the formula for the sum.
| source | states | J (joint system) | S | L | Σ formula | Σ constant |
|---|---|---|---|---|---|---|
| corpus \(L=3\) (odd) | 637 | 637 | 637 | 637 | 637 | 48 |
| corpus \(L=4\) (odd) | 720 | 720 | 720 | 720 | 720 | 38 |
| odd (2,2,4) | 14 | 14 | 14 | 14 | 14 | 0 |
| odd (2,4,6) | 14 | 14 | 14 | 14 | 14 | 0 |
| odd (4,3,3) | 5 | 5 | 5 | 5 | 5 | 1 |
| odd (4,4,6) | 15 | 15 | 15 | 15 | 15 | 1 |
| even, uncharged (4 cells) | 17 | 17 | 17 | 17 | 17 | 9 |
| even, charged (4 cells) | 45 | 0 | 0 | — | — | — |
Values of the sum on A in odd states include \(\{-1, -\tfrac13, \tfrac13\}\) at \(L = 3\) and \(\{-\tfrac12, 0, \tfrac12, 1\}\) at \(L = 4\). In every charged state some \(\sigma_k\) fails to be separable, as Theorem 5 predicts.
Item 15 (not explained): for each coordinate the script recorded whether \(F_{01}\), \(F_{23}\), both or neither is constant on A, and likewise for the other two coordinates. All four outcomes occur at every coordinate. But in all 1,422 oriented states at least one coordinate has a constant family profile. I have no argument for this, and a sample of this kind has misled the project before.
B5: directions on one sublattice (optional)
h448_dirsets.py: type model with T2 and the sign field, no oddness, nothing about the other sublattice. Reversing all arrows and the maps \(\mathrm{diag}(-1,-1,1)\) and so on preserve both sublattices and together flip any single axis of the moments. So only the pattern per axis matters: absent (0), one-way (1) or two-way (2). On (4,3,3) the swap \(y\leftrightarrow z\) was also used. Each query came with a control that drops the constraints on one required axis, and all controls were SAT.
| cell | patterns queried | SAT | UNSAT | longest query | wall |
|---|---|---|---|---|---|
| (4,3,3) | 17 | every pattern with at most two axes nonzero (11) | every pattern with three axes nonzero (6) | 34 s | 75 s |
| (6,2,3) | 26 | at most two axes (18) | three axes (8) | 13.5 s | 49 s |
| (5,2,4) | 26 | at most two axes (18) | three axes (8) | 33 s | 95 s |
So on these cells the signs add no restriction on one sublattice beyond Theorem S (no sublattice carries all three types): two two-way axes on one sublattice occur. No query of the form “odd and all six directions”, or anything equivalent to H, was run.
Computations run
From scratch_h, project .venv, PYTHONPATH=<repo>:<repo>/experiments/08_frozen_structure, TMPDIR=<repo>/.tmp. Logs and state files in <repo>/.tmp (h441.log, h443.log, h444_*.json, h447_*.json).
| command | what it tested | verdict | wall |
|---|---|---|---|
h441_kernel.py 3,3,3 1,1,1 2,3,3 |
pre-flight, B1 ranks | equal, formula ok | 0.9 s |
h441_kernel.py (20 cells, listed above) |
B1 kernel = span, formula, chain counts | 60/60 equal | 14.5 s (run twice) |
h443_joint.py 1,1,1 2,2,2 3,3,3 |
pre-flight, B2 | equal | 1.7 s |
h443_joint.py 4,4,4 |
timing, B2 | equal | 8.1 s |
h443_joint.py (18 cells) |
B2 ranks, formulas, Fourier count, B2b | all equal | 70 s |
h442_symbol.py (first run) |
symbolic identities | check (2) False: script bug (substitution) | 1.3 s |
h442_symbol.py |
the same, fixed | ALL OK | 1.1 s |
h444_even.py 3,3,3 2 120 |
pre-flight, even states | 6 SAT, 2 UNSAT, 0 violations | 1.5 s |
h444_even.py CELL 8 300 on 4 cells |
B3 samples and checks | table above | solver 0.2 to 0.4 s, under 3 s each |
h445_outside.py (4 cells, twice) |
Proposition O checks | T1 0 failures; T4 0 failures | 2.4 s |
h447_oddsample.py 2,4,6 3 60 |
pre-flight, odd samples | 3 SAT | 1.2 s |
h447_oddsample.py CELL 16 300 on (2,4,6), (4,4,6), (2,2,4), (4,3,3) |
odd non-cubic samples | 15/16/14/5 SAT; no charged hole | 0.5, 19.2, 0.2, 20.1 s solver |
h446_fractions.py (twice) |
B4 on corpus and samples | table above | 8 s |
h448_dirsets.py 4,3,3 120 (first run) |
pre-flight | crashed (unused variable) | 1 s |
h448_dirsets.py 4,3,3 120 |
pre-flight | controls UNSAT on 3-axis patterns (control design, see below) | 31 s |
h448_dirsets.py CELL 200 on 3 cells |
B5 | table above | 75, 49, 95 s |
No query hit its cap. Every solve went through h32_cap.run_batch, one process per cell, with a cap of 300 s or less for the whole batch.
What failed, and why
- The simpler description of the charge defect. My first guess was that in an even-curl state \(n_k\) is, modulo the span, the mean-zero antiderivative of the charges along the rod lines of axis \(k\). It fails in 106 of 186 cases, exactly when a line of holes along \(k\) has nonzero total charge. Those totals include holes whose rods lie on other axes. The correct statement (Proposition O) adds the term \(\rho\) from Theorem 5.
- B5 controls. The first control (“the same directions present, with no absences required”) was UNSAT for every pattern with three axes, because it is itself the three-types query that Theorem S excludes. It was replaced by dropping the constraints on one required axis, and all controls were then SAT.
- Two script bugs, found and fixed before use: a substitution error in check (2) of
h442, and an undefined variable inh448. - Hand proof of Lemma M. I first tried to derive it from the type chain-mode lemma of the record, through the derivation of \(P^k\) from (T2). That route works, but it rests on a lemma I did not re-read, so I replaced it with the direct four-line check above.
- No direct real-space proof. The kernel theorem is not a factorisation of \(P^k\) itself. The factorisation exists only after eliminating one sublattice (item 3), and the case analysis at the degenerate \(\psi\) is still needed.
Rules
No rule was broken, as far as I know. Four points need stating. I listed the scratch_h directory, which shows check7’s file names (h430 to h432), but I did not open, run or touch them. I used shell for loops (not heredocs) to run the same script on several cells one after another, one solver process at a time. I imported read-only from h38_lib, a4_typemodel, h32_cap and hlib and modified none of them. For B5 I re-implemented the sign-field encoding in h448 because a4_typemodel.add_sign_field does not expose its variables.
Relation to the main loop’s claims
Nothing contradicts them. Four refinements: (a) Only the antisymmetric sublattice constant is needed beyond the chains, because \(\mathbf 1_A + \mathbf 1_B\) is a chain sum. (b) “The six indicators have the same linear form as the types” is true in the sense of Theorem D, but the sharing is different. Each chain carries two weights, each coupling two directions whose difference is along the chain. The signed part has no sublattice constant, and the two families of an axis enter with different signs. (c) The signed line fractions do not add to a constant. There are six profiles, not three, and the fractions of B are determined by those of A up to constants, which has no counterpart for the types. (d) The membership of \(n_k\) in the span, sampled in 34 states by the main loop, holds in all 1,357 corpus states and all 65 oriented samples, and is now a consequence of Lemma 3 and Theorem K rather than an observation.