Completeness of the chain modes, proved for every cell: a stratified symbolic kernel computation on the unit torus

1. Target statement

Let \(H\) be the space of real solutions \((a,b)\) on the vertices of the torus of the homogeneous two-match system: for every hexagon \(h\), \[\sum_{v\in h}\mathrm{ind}_h(v)=0,\qquad \mathrm{ind}_h(v)=\begin{cases}-a(v)-b(v)&\alpha_h(v)=x\\ a(v)&\alpha_h(v)=y\\ b(v)&\alpha_h(v)=z.\end{cases}\] The chain modes \(m_C\) (the vector \(w_E\) on the vertices of a chain \(C\) of axis \(E\) and zero elsewhere, \(w_x=e_y-e_z\), \(w_y=e_z-e_x\), \(w_z=e_x-e_y\), so \((a,b)\) components \((1,-1)\), \((0,1)\), \((-1,0)\)) solve it, as do the two sublattice-antisymmetric constants \((a,b)=\sigma_v(\alpha,\beta)\) with \(\sigma=+1\) on A and \(-1\) on B.

Completeness is the claim that these span \(H\) on every cell \((a,b,c)\). It was verified numerically on seven small cells (e13_realspace.py, e18_verify.py) and is the premise of the parametrisation theorem of docs/theorem-h-2026-09-06.md and of the new partner identity (r6_modes.py, r6_exact.py, main loop, today). The note records that “a hand proof of completeness is the determinant computation above; it was not written out”. Probe F was to write it out as a stratified symbolic kernel computation over the whole unit torus, with sympy and no SAT solver.

2. Outcome

Completeness is proved, for every cell, with no exception: at every one of the 69 strata into which the unit torus falls the kernel of the Fourier matrix is exactly the span of the chain modes supported there, together with the two constants at the sixteen points where the character is trivial on the FCC lattice. No stratum has a kernel larger than the mode span, so the note’s table is not a small-cell coincidence and no extra real-space mode exists. The proof is short because the \(4\times4\) matrix, after clearing denominators, is built out of only four polynomials \(A=x^2-y^2\), \(B=x^2-z^2\), \(P=x^2y^2-1\), \(Q=x^2z^2-1\), one row per omitted direction, and the row omitting \(d_\ell\) vanishes identically on exactly the \(\ell\)-th kagome locus. The stratification has four types: a single chain family (rank 3, kernel 1), both families of one axis (rank 2, kernel 2), the three families of one kagome plane (rank 2, kernel 2, one row vacuous, one relation \(w_x+w_y+w_z=0\) among the three modes), and the sixteen degenerate points where \(M\) is the zero matrix (kernel 4, where the chain modes give only 2 and the two constants are indispensable). Every wavevector of the torus falls into one of these by an exact classification of which of the six locus conditions can hold at once, and the classification is forced: of the \(2^6\) subsets only fourteen are realisable. Two independent cross-checks back the phase conventions: a numerical Fourier transform of the real-space chain modes on \((2,2,3)\) reproduces the formula \(v_f(k)=(w_E,\;w_E/\chi(d_i))\) to \(10^{-15}\), and the bookkeeping \(\sum_q\dim\ker M(q)=\dim H\) holds on three cells, with the note’s seven-cell rank table reproduced exactly and extended to seven further cells.

3. Definitions and encodings

Lattice. Diamond sites in quarter-cube units, box \((4a,4b,4c)\); A-sublattice is the FCC lattice \(\Lambda\) generated by \((0,2,2)\), \((2,0,2)\), \((2,2,0)\) (index 16 in \(\mathbb{Z}^3\)), B is \(\Lambda+(1,1,1)\); the four A-to-B displacements are \(d_0=(1,1,1)\), \(d_1=(1,-1,-1)\), \(d_2=(-1,1,-1)\), \(d_3=(-1,-1,1)\). Axis pairing (icemix.cnf.AXIS_PAIRS): \(x=\{0,1\},\{2,3\}\); \(y=\{0,2\},\{1,3\}\); \(z=\{0,3\},\{1,2\}\).

Chain families. A chain of family \(f=\{i,j\}\) alternates \(+d_i\) and \(-d_j\); its period is \(u_f=d_i-d_j\) and its axis is \(\mathrm{axis}(i,j)\). The six families, their steps and their loci (status: computed, f1_strata.py):

Note \(C=B-A\), \(z^2P-y^2Q=C\) and \(x^2R=z^2P-B\), which is why only \(A,B,P,Q\) appear in the matrix.

Fourier reduction. For \((x,y,z)\) on the unit 3-torus put \(\chi(p)=x^{p_1}y^{p_2}z^{p_3}\) and take the ansatz \(\text{field}(v)=\mathrm{amp}_{\mathrm{sub}(v)}\cdot\chi(\mathrm{pos}\,v)\) with \(\mathrm{amp}_A=(a_A,b_A)\), \(\mathrm{amp}_B=(a_B,b_B)\). Translating a hexagon by \(\lambda\in\Lambda\) multiplies its equation by \(\chi(\lambda)\), so the system collapses to one equation per \(\Lambda\)-orbit of hexagons. There are exactly four such orbits, one per omitted direction \(\ell\) (computed, f1_check.py check (0): on \((2,2,2)\), \((2,2,3)\), \((3,3,3)\) the \(16abc\) hexagons form 4 orbits of \(4abc\), one per \(\ell\); equivalently \(n_{\text{hex}}=16abc=4\cdot4abc\), four per FCC cell). Hence \(M(x,y,z)\in\mathbb{C}^{4\times4}\) acting on \((a_A,b_A,a_B,b_B)\), row \(i\) being the orbit omitting \(d_i\).

Why the unit torus is the right index set. \(B_{abc}=4a\mathbb{Z}\times 4b\mathbb{Z}\times4c\mathbb{Z}\subset\Lambda\), and the restriction map \(\mathrm{Hom}(\mathbb{Z}^3/B_{abc},U(1))\to\mathrm{Hom}(\Lambda/B_{abc},U(1))\) is surjective with kernel \(K=\{\kappa:\kappa|_\Lambda=1\}\) of order 16 (\(\kappa\in\mu_4^3\) with \(\kappa_x^2=\kappa_y^2=\kappa_z^2\)). So the \(64abc\) lifted characters \(x^{4a}=y^{4b}=z^{4c}=1\) cover each of the \(4abc\) FCC wavevectors of the cell exactly 16 times, and proving the claim for every point of the unit torus proves it for every cell (proved). The redundancy is harmless: for \(\kappa\in K\) one has \(M(\kappa\cdot e)=M(e)\,\mathrm{diag}(1,1,\lambda,\lambda)\) with \(\lambda=\kappa_x\kappa_y\kappa_z\), so the kernels correspond.

The mode vectors. A chain of family \(f=\{i,j\}\) based at an A vertex \(p_0\) has A vertices \(p_0+nu_f\) and B vertices \(p_0+d_i+nu_f\); its Fourier amplitude is supported where \(\chi(u_f)=1\), and there \(\chi(d_i)=\chi(d_j)\), so the family contributes the single line \[v_f(k)=\bigl(w_E,\;w_E/\chi(d_i)\bigr)\in\mathbb{C}^4 .\] Explicitly (computed, verified numerically in §4.6):

The constants. A field constant on each sublattice with opposite signs has \(\chi|_\Lambda=1\), that is \((x,y,z)\in K\); there the two constant vectors are \((1,0,-1/xyz,0)\) and \((0,1,0,-1/xyz)\).

Real versus complex. The system has integer coefficients and the modes are integer vectors, so if the complex span of the modes equals \(\ker_{\mathbb{C}}\) then intersecting with \(\mathbb{R}^n\) gives the real statement. Everything below is over \(\mathbb{C}\).

Environment. Mac, project venv, PYTHONPATH with the repo root and experiments/08_frozen_structure. Scripts scratch_h/f1_strata.py and scratch_h/f1_check.py; logs in scratch_h/attack_2026-09-17/ (f1_strata.log, f1_check.log, f1_matrix.log). No SAT solver was used and none was needed.

4. What was found

4.1 The matrix and its determinant

Clearing denominators row by row (each row multiplied by a monomial, which does not change the kernel) gives, with \(A,B,P,Q\) as above (computed, f1_matrix.log):

\[M=\begin{pmatrix} -xyz\,A & -xyz\,B & z^2A & y^2B\\ -xz^2P & -xy^2Q & yz\,P & yz\,Q\\ yz^2P & y\,B & -xz\,P & -xy^2z\,B\\ z\,A & y^2z\,Q & -xyz^2A & -xy\,Q \end{pmatrix}\]

row \(i\) being the hexagon orbit omitting \(d_i\). Its determinant is \[\det M=4x^2y^2z^2\,ABC\,PQR =4x^2y^2z^2\prod_{f}\bigl(\text{locus polynomial of }f\bigr),\] which is the note’s formula up to the monomial (the raw, uncleared matrix has \(\det=4ABCPQR/(y^2z^6)\), exactly as in docs/theorem-h-2026-09-06.md and e11_fourier.py). The script checks \(\det M/\prod_f(\chi(u_f)-1)=4/z^2\), a nonzero constant times a monomial, so the twelve surfaces of the determinant are precisely the six chain loci and nothing else (proved).

Two structural facts follow by inspection and are asserted in the script:

• (S1) every entry of \(M\) is a monomial multiple of one of \(A,B,P,Q\);
• (S2) row 0 uses only \(A,B\); row 1 only \(P,Q\); row 2 only \(P,B\); row 3 only \(A,Q\). Hence row \(\ell\) vanishes identically exactly on the locus where its two polynomials both vanish, and those four loci are precisely the four kagome strata of §4.2 (computed, asserted: “rows vanishing = [\(\ell\)]” for each \(\ell\)).

4.2 The classification of the strata

For a point \(k\) of the torus let \(Z(k)\) be the set of families \(f\) with \(\chi(u_f)=1\). Writing \(E=(x^2,y^2,z^2)\), each of the six conditions is \(E^n=1\) for an integer vector \(n\), and \(E^m=E^n=1\) forces \(E^{m\pm n}=1\); a condition \(E^n=1\) is forced by a set \(S\) precisely when \(n\) lies in the subgroup of \(\mathbb{Z}^3\) generated by \(S\)’s vectors (not merely in its saturation: \(E^{2n}=1\) leaves \(E^n=\pm1\)). The script computes this subgroup membership exactly by Hermite normal form over all \(2^6\) subsets. Result (proved): exactly fourteen subsets are closed, and they are

The two facts that make the list short: two conditions from different coordinate pairs always force a third (so \(|Z|=2\) across pairs is impossible), and both conditions of one pair force the fourth power of each of its two phases to be 1 (for the pair \((x,y)\): \(x^2=y^2\) and \(x^2y^2=1\) give \(x^4=1\)), after which any further condition forces all six. Hence \(|Z|\in\{0,1,2,3,6\}\) and \(|Z|\in\{4,5\}\) cannot occur.

Resolving the signs (each condition \(x^2=y^2\) splits into \(x=\pm y\), each \(x^2y^2=1\) into \(xy=\pm1\)) gives 68 strata with \(Z\neq\{\}\), plus the generic stratum. Each stratum below is parametrised by free symbols \(s,t\) ranging over the unit circle, subject to the genericity conditions that no further family is present.

4.3 The stratum table

Every entry is proved: on each stratum the script verifies \(M\,v_f=0\) identically for every supported mode, certifies \(\mathrm{rank}\,M\) by exhibiting a minor whose every non-monomial irreducible factor divides one of the excluded locus polynomials (so it cannot vanish anywhere on the stratum) and by checking that all larger minors vanish identically, and certifies \(\dim\mathrm{span}\) of the modes the same way.

Counts: \(12+24+16+16=68\). Verdict on every one of the 68: SPANNED (f1_strata.log, summary table). Strata with a kernel not spanned by the modes: 0.

Three worked cases, each hand-checkable from the matrix of §4.1.

Type I, \(x=y=s\), \(z=t\) (family \(\{1,2\}\), axis \(z\)). The rows become

\[\begin{aligned} \text{row }0&=s^2(t^2-s^2)\,(0,\,t,\,0,\,-1),\\ \text{row }3&=s^2(s^2t^2-1)\,(0,\,t,\,0,\,-1),\\ \text{row }1&=s\,\bigl(-t^2(s^4-1),\,-s^2(s^2t^2-1),\,t(s^4-1),\,t(s^2t^2-1)\bigr),\\ \text{row }2&=s\,\bigl(t^2(s^4-1),\,s^2-t^2,\,-t(s^4-1),\,-s^2t(s^2-t^2)\bigr). \end{aligned}\]

Rows 0 and 3 are proportional. The vector \((1,0,t,0)\) is annihilated by all four (rows 0 and 3 have zero first and third entries; rows 1 and 2 give \(\mp t^2(s^4-1)\pm t\cdot t(s^4-1)=0\)), and it is minus the mode \(v_{\{1,2\}}=(-1,0,-t,0)\), since \(\chi(d_1)=x/yz=1/t\) here. The \(3\times3\) minor on rows \((0,1,2)\), columns \((0,1,3)\) is \[2s^4t^2(s^4-1)(s^2-t^2)^2(s^2t^2-1),\] whose factors are exactly the locus polynomials of the five absent families (\(s^4-1\) is \(\{0,3\}\); \(s^2-t^2\) is \(\{1,3\}\) and \(\{2,3\}\); \(s^2t^2-1\) is \(\{0,2\}\) and \(\{0,1\}\)), so it is nonzero at every point of the stratum. Rank 3, kernel 1, spanned. The other eleven type-I strata are the same computation with signs.

Type III, \(\ell=0\), \(x=y=z=t\), \(t^4\neq1\). Row 0 vanishes identically (\(A=B=0\)), and the rest are \(t^2(t^4-1)\) times \((-t,-t,1,1)\), \((t,0,-1,0)\), \((0,t,0,-1)\), the first being minus the sum of the other two. Rank 2 (minor on rows \((1,2)\), columns \((0,1)\) equals \(t^6(t^4-1)^2\), nonzero since \(t^4\neq1\)), kernel \(\{(a,b,ta,tb)\}\). The three supported modes are \(v_{\{1,2\}}=(-1,0,-t,0)\), \(v_{\{1,3\}}=(0,1,0,t)\), \(v_{\{2,3\}}=(1,-1,t,-t)\); they sum to zero (this is \(w_x+w_y+w_z=0\), the kagome-layer relation of the note, appearing here as a relation in Fourier space) and any two span the kernel. Spanned.

Type IV, \((x,y,z)=(i,i,i)\). Here \(x^2=y^2=z^2=-1\), so \(A=B=P=Q=0\) and by (S1) \(M\) is the zero matrix: the kernel is all of \(\mathbb{C}^4\). Every \(\chi(d_j)=-i\), so all six modes have the form \((w,\,i\,w)\) and span only 2 dimensions, while the constants are \((1,0,-i,0)\) and \((0,1,0,-i)\), of the form \((w,-i\,w)\), giving the remaining 2. The two constants are indispensable at all sixteen type-IV points and nowhere else; the script reports “dim span(chain modes alone) = 2” at each.

4.4 The special points, explicitly

The sixteen type-IV points are exactly \(K\), the characters trivial on \(\Lambda\): \(x^2=y^2=z^2=\sigma\) with \(\sigma=\pm1\), that is \((x,y,z)\in\{\pm1\}^3\) (eight points, \(\sigma=1\)) or \(\{\pm i\}^3\) (eight points, \(\sigma=-1\)). All sixteen sit over the single FCC wavevector \(q=0\); \((1,1,1)\) and \((-1,-1,-1)\) are two of the sixteen, and the note’s phrase “at \(k=(\pi,\pi,\pi)\) two further modes appear” is this point in the \((-1,-1,-1)\) lift. Treating only \((\pi,\pi,\pi)\) would have left fourteen points unexamined; all sixteen are done here and all sixteen behave identically (rank 0, kernel 4, chain modes 2, constants 2).

The other places where strata meet are already in the list, because the stratification is by the value of \(Z(k)\), which is defined at every point of the torus: a point where two type-I surfaces cross has \(|Z|\geq2\) and so is a type II, III or IV point, never a type-I point. The genericity conditions in the table are exactly the statement that the point is not in a deeper stratum, and every certifying minor was checked to be nonvanishing on the stratum in that precise sense.

Coverage audit (computed, f1_strata.log). Over the 13824 points of \(\mu_{24}^3\) the script computed \(Z(k)\) and checked that (i) only the fourteen classified patterns occur and (ii) every point with \(Z\neq\{\}\) satisfies the defining equations of a listed stratum with the matching \(Z\):

Uncovered points: 0. Patterns outside the classification: 0. The 16 is a direct sighting of \(K\).

4.5 The proof, in words

Let \(k\) be any point of the unit torus.

1. If \(Z(k)=\{\}\) then \(\det M\neq0\) by §4.1, so \(\ker M=0\), and no chain family is supported at \(k\): nothing to span.
2. Otherwise \(Z(k)\) is one of the thirteen nonempty closed patterns of §4.2, and \(k\) lies in one of the 68 strata.
3. On each stratum, \(M v_f=0\) for every supported \(f\) (verified symbolically; it is also the chain-mode lemma of the note, proved by hand there), the supported modes have the dimension stated, and \(\mathrm{rank}\,M=4-\dim\) by a minor that cannot vanish anywhere on the stratum together with the vanishing of all larger minors. Hence \(\ker M(k)\) equals the span of the supported modes, with the two constants added at the sixteen points of \(K\) and nowhere else.
4. For a cell \((a,b,c)\), \(H\otimes\mathbb{C}=\bigoplus_q\ker M(q)\) over the \(4abc\) FCC wavevectors of the cell, every one of which is a restriction of a point of the unit torus; the chain modes of family \(f\) span, at each \(q\) with \(\chi(u_f)=1\), exactly the line \(\mathbb{C}v_f(q)\) and nothing elsewhere, and the two constants span the antisymmetric part at \(q=0\). (The first of these is the transverse discrete Fourier transform on the set of parallel chains of the family, which is onto; consistently, the number of chains of family \(f\) equals \(\#\{q:\chi(u_f)=1\}\), and summing over \(f\) gives the cell’s chain count, checked on four cells in §4.6d.) By step 3 the two sides agree wavevector by wavevector, so they agree in total: the chain modes and the two constants span \(H\). Taking real points gives the real statement. \(\square\)

4.6 Cross-checks

Status computed throughout, f1_check.log.

The recomputed rank table, with the note’s seven cells first:

and seven cells the note did not test:

The mod-\(p\) ranks are sound in the direction used: \(\mathrm{rank}_{\mathbb{F}_p}\leq \mathrm{rank}_{\mathbb{Q}}\), so \(\mathrm{rank}_{\mathbb{F}_p}(A)=r\) gives \(\dim\ker_{\mathbb{Q}}A\leq2n-r\) and \(\mathrm{rank}_{\mathbb{F}_p}(N)=2n-r\) gives \(\dim\mathrm{span}_{\mathbb{Q}}(N)\geq2n-r\); since \(AN=0\) over \(\mathbb{Z}\) both are equalities. Each row of the table is therefore an independent proof of completeness on that cell, on top of the general theorem.

5. Residual

• Nothing of the target is left open. Completeness holds for every cell; the premise of the parametrisation theorem and of the partner identity is now proved, not computed. The note’s sentence “a hand proof of completeness is the determinant computation above; it was not written out” can be replaced by §4, and its status tag on the completeness table can be raised from computed to proved.

• One correction to the note’s phrasing. “At \(k=(\pi,\pi,\pi)\) two further modes appear” is right only in a particular lift; the invariant statement is “at the FCC wavevector \(q=0\)”, which in the \((x,y,z)\) parametrisation is the sixteen-point set \(K\). Similarly “on each locus the kernel is one-dimensional and is the chain mode of that family” is true only on the interior of a single locus; on the three deeper strata the kernel is 2 or 4 dimensional. Neither changes any conclusion drawn from the note, but the deeper strata are where a hand argument would have gone wrong, and they are the substance of this report.

• Not addressed here, because outside the brief: integrality. The spanning statement is over \(\mathbb{Q}\) and \(\mathbb{R}\); the Smith invariants \(2,8,8\) and the \((2,2,3)\) states with \(\alpha_0=\pm1/6\) (e16_f.py, e20_balance.py, e23_lattice.py) are untouched, and a frozen state’s chain weights still need not be integral.

• A by-product worth keeping. The relation structure among the chain modes is now read off the strata rather than guessed: relations appear exactly where a stratum supports more modes than its kernel dimension, which happens in only two places, one relation at each wavevector with \(|Z|=3\) (the three modes of a \((111)\) plane sum to zero) and four at \(q=0\) (six chain modes spanning two dimensions). Counting the cell’s wavevectors by \(|Z|\) therefore predicts the rank deficit exactly (computed, f1_check.py check (d)):

  cell	wavevectors by \(|Z|\) (\(0,1,2,3,6\))	chains	predicted relations	rank deficit
  (1,2,2)	4, 4, 7, 0, 1	24	4	4
  (2,2,2)	6, 12, 9, 4, 1	48	8	8
  (2,2,3)	24, 12, 11, 0, 1	40	4	4
  (3,3,3)	36, 48, 15, 8, 1	108	12	12

  On \((3,3,3)\) that is the note’s count of 12 relations among 108 chains, now with a reason: eight \(|Z|=3\) wavevectors contributing one each, and \(q=0\) contributing four. The four at \(q=0\) match the note’s three family relations plus the one per-axis relation \(w_x+w_y+w_z=0\), and the rest are its kagome-layer relations; but \((2,2,3)\) and \((1,2,2)\) have no \(|Z|=3\) wavevector at all, so on those cells there are only the four, and the note’s kagome-layer relations cannot all be independent there. Anyone counting relations on a new cell should count wavevectors by \(|Z|\) rather than layers (computed, not proved: the identification of which real-space relation sits at which wavevector was not carried out).

• A caution for reuse. The mode formula \(v_f(k)=(w_E,w_E/\chi(d_i))\) carries a sign convention in the exponent of \(\chi\). It was verified against real space on \((2,2,3)\) (§4.6a) rather than assumed, and any reuse in another script should re-run that check rather than copy the formula.

6. Solver checks run

No SAT solver, no CNF, no certificate: the whole probe is symbolic linear algebra in sympy plus exact integer ranks. Total wall-clock 22 seconds on the primary Mac in the project venv: f1_strata.py 18 s (builds \(M\) from the \((3,3,3)\) lattice, factors the determinant, classifies the strata by Hermite normal form, analyses all 68 strata with certified minors, audits coverage over 13824 points) and f1_check.py 3.2 s (orbit check, Fourier check on \((2,2,3)\), bookkeeping on three cells, exact rank table on fourteen cells, closed form and relation count). Both exit 0; both are assertion-heavy and will fail loudly rather than print a wrong verdict. Logs: experiments/08_frozen_structure/scratch_h/attack_2026-09-17/f1_strata.log, f1_check.log, f1_matrix.log.

To reproduce, from experiments/08_frozen_structure/scratch_h:

PYTHONPATH=~/repo/project/ice-mixing:\
~/repo/project/ice-mixing/experiments/08_frozen_structure \
  ../../../.venv/bin/python f1_strata.py

and the same for f1_check.py.

Update, 2026-10-01. Read by an independent checker, agent p1check (2026-10-01-opus-p1check.md), with its own model and its own stratification (a Smith-normal-form parametrisation of each closed pattern): CONFIRMED as a proof for every cell, the same 68 components (12 + 24 + 16 + 16) with 0 failures, and exact real-space ranks on 12 cells. Two cosmetic miscounts in this report: “fourteen closed subsets” should read fifteen (fourteen nonempty), and “thirteen nonempty patterns” in section 4.5 should read fourteen.