Verdict

RELATION. Two relations hold in every model found, dense and rigid, on all four cells, and both have a hand derivation uniform in g:

1. The wave equation (Lemma W, proved here, every cell). On each sublattice, with k[n][v] the number of type-x vertices of class value v (d = y - z, or s = y + z, mod 4g) on the plane of relative x = n: k[n+2][v] + k[n-2][v] = k[n][v+2] + k[n][v-2]. It is Law C summed over the holes of one class with one-hot. Its solutions are k = phi(w - u) + psi(w + u) (u = n/2, w = v/2): two sheets travelling one chain label per cube in opposite senses. This is the two senses of item 7, and it is a LINEAR law (in the row space of the window’s equations).
2. The defect e = (type-x on the A plane of a chain) - (type-x on its B plane). Linear part (Lemma D, proved here): e(n)[v+2] + e(n)[v-2] = 2 e(n-2)[v], hence on the torus e is one constant eps for every x-chain of both families (Lemma T; also from (C); checked on 5119 frozen states, every axis). Integral part (solver, four cells, with SAT controls): with the four literals of the pattern, e is the same constant eps on every chain of the window already on [-3,3]; eps >= 0 on [-3, 2g-2]; with the negation of (V) added, eps = 0 on [-3, 2g-1] and not on [-3, 2g-2]. So on the torus, given the pattern, (V) is equivalent to eps >= 1, that is to n_x(A) > n_x(B).

The exact gap (T3). The counts cannot close (V): two parallel unit sheets of one sense, one through each rod, with eps = 0, satisfy the wave equation, P^x per class, Lemma 6, the bounds, the pins of the pattern and the negation on the whole torus of every cell (h767, exact). Every enumerated profile, dense or rigid, extends by the recurrence round the whole x-circle within the bounds (h766). The obstruction at 2g + 1 lives in the positions of the kinks inside a class, not in their number. The root-of-unity sums of T1(b) are the Fourier coefficient chi_d (j = 1) of the moment report, not a different quantity; nothing of (a) or (b) holds in the dense models.

The object, exactly

Cell (a, b, c), quarter-cube coordinates modulo (4a, 4b, 4c), A = even coordinates with sum 0 mod 4, B = A + (1,1,1); bonds from A along d_0 = (1,1,1), d_1 = (1,-1,-1), d_2 = (-1,1,-1), d_3 = (-1,-1,1). A-hole O = (2,0,0); relative coordinates from O; a plane is one relative x = n (A for n even, B for n odd), 2bc vertices. g = gcd(b, c), class size L = 2bc/g.

Chains of axis x. Family {0,1}: step d_0 - d_1 = (0,2,2), constant d = y - z; the chain through the A vertex v has B vertices v + (1,1,1) + m(0,2,2), so it lies on the A plane n of v and the B plane n + 1. Family {2,3}: step (0,2,-2), constant s = y + z, on the A plane n and the B plane n - 1. The planes are therefore linked … A(n) -d- B(n+1) -s- A(n+2) -d- B(n+3) …: consecutive planes share one family of chains, alternately d and s. On a plane, d and s each take one residue r mod 4 and g values mod 4g, four apart; a class is the set of vertices of one value; it has L vertices and is the trace of exactly one chain (h760 checks this by walking every chain). The class value is the same on the two planes of a chain. A vertex is a kink of the two x-chains through it iff its type is x (curl-reduction, Lemma A).

Kink vector of a plane n and a family: k[n][v] = number of type-x vertices of the plane in the class of value v (v over the g values of the plane’s residue). The vector of a chain is the sum over its two planes. Lemma 6 is the statement that the sum over v is the same on every A plane and the same on every B plane.

Hypotheses throughout: form ng2 (rods (0,0,0), (4,0,0) of type x; (1,1,1) of type y; (3,-1,1) not of type y), type model of h360_lib, (T2) on the hexagons of the one-sided window [-3, Q], no R; the negation of (V) as the clause “some B vertex of plane -1 has type x”. The record’s threshold is Q = 2g + 1.

T1. Measurements

Enumeration (h761). One h560 worker child per (cell, Q), blocking on the type-x variables of both sublattices in the window, cap 120 s, seed 1. Solver wall for all twelve: 10.3 s.

One model in full ((12,4,4), Q = 6, model 0; classes in the order of their values from the plane’s residue; “n_x” the type-x count of the plane):

Read off: k_d is the same on the two planes of each d-chain (A n, B n+1) and k_s on those of each s-chain (A n, B n-1); on the A planes k_d obeys 6 + 4 = 2 + … in the wave form (e.g. at hole plane 0: k[2] + k[-2] = (2,6,0,0) + (4,2,2,0) = (6,8,2,0) = k[0][v+2] + k[0][v-2] = (6,2,0,0) shifted both ways = (6+0, 2+6, 0+2, 0+0)); the s-profile is flat and the d-profile is not a single travelling sheet (both senses present). A model of (12,4,8), Q = 6, with defect 2 on every chain (model 29): A -2: d = (2,9,6,9), B -1: d = (0,7,4,7); A +0: d = (6,7,7,6), B +1: d = (4,5,5,4); A +2: d = (10,4,8,4), B +3: d = (8,2,6,2); s likewise (A -2: (6,7,6,7), B -3: (4,5,4,5)); every chain of the window has A = B + 2, and the wave equation holds on the A planes as it does when the defect is 0.

(a) Determination and cyclic shifts (h762). “coll” = pairs (model, plane) whose vector occurs with two different successors; “shift” = successor is a cyclic shift of the vector.

No first-order determination (collisions on every cell but (12,6,6), where 60 models are too few to collide in 72 entries) and no cyclic-shift rule; the “shift” count for the next plane is the A = B equality of the chain’s two planes, not a rotation. The true rule is second order: with the wave equation, two consecutive A planes determine every further A plane (h766: 0 violations in 25 000 instances), and the B planes follow from P^x per class.

(b) Root-of-unity sums. F_m[n] = sum_ell k[n][ell] w^(m ell), w = exp(2 pi i/g). Since w^ell = exp(2 pi i (v - r)/(4g)) = const x exp(2 pi i (y -+ z)/(4g)), F_1 of the d-family is the coefficient chi_d (j = 1) of the moment report and F_m its harmonic j = m. Not a new quantity. Ratios F_m[n+2]/F_m[n] over the models, m = 1: (12,4,4) Q 6: 480 pairs, 28 with F = 0, 63 distinct ratios, 38 phases; (10,5,5) Q 8: 600 pairs, 219 ratios, 147 phases; (12,6,6) Q 10: 720 pairs, 107 ratios, 73 phases; the s-family alike. No fixed phase per cube in the dense models (the moment report’s finding, repeated). On the rigid models the wave equation makes each harmonic rotate by exp(+-i pi m/g) per A plane as a two-step recurrence, not a one-step phase.

(c) Every linear relation (h762, h763). Exact null space over Q of the data matrix of w consecutive planes (both families, constant column), pooled by the parity of the first plane, each basis relation tested at every position against the row space of the window’s equations (one-hot, (T2) as “six sum to two”, the four literals; SVD, residual < 1e-6, and exact on the models):

“Flatness” = in the span of the row space and the functionals e(chain) - e(chain’); “e = 0” = the per-chain equality k[A n][v] = k[B n+-1][v] itself, which is in the sample on the square cells only because the sampler never found eps >= 1 there (the solver shows it exists, Table E). So the complete set of linear relations between the kink vectors of consecutive planes that hold in every model is: the linear laws, plus the flatness of the defect, plus its value. The laws in these coordinates are the wave equation on each sublattice, P^x summed over a class, and their consequences (Lemma 6; the relations F_j(n + 2g/gcd(j,g)) = +-F_j(n) of the moment report). The per-class laws of Lemmas W and P are each in the row space (h763 (1), (6): 48, 56 and 80 laws on the three windows, residual < 2e-14), and hold exactly on every model.

(d) Parity. Every chain of every model has an even number of type-x vertices (0 odd of 2160 to 5040 per window), a consequence of eps even here, and in a frozen state of Lemma P0 below.

Table E. The defect by solver (h765). One h32_cap batch per row (cap 120 s), one selector per cardinality constraint (sequential counter), control SAT in every row. “flat” = every query e(c) - e(c’) >= 1 and <= -1 UNSAT (c’ the next class of the family, and the s-chain of the same class); “eps >= 1” and “eps <= -1” = the verdict of e(c) >= 1, e(c) <= -1 for every chain.

Reading: (i) the pattern alone makes the defect one constant on every chain of the window, already on [-3,3] at g = 4 (and wherever decided); (ii) the pattern alone makes it non-negative on [-3, 2g-2] (not on [-3,5] at g = 4); (iii) the negation makes it zero on [-3, 2g-1] and not on [-3, 2g-2]; (iv) without the pattern both signs occur and flatness is undecided. (12,4,8) separates nothing here: gcd(a,b) = gcd(a,c) = g on all four cells.

Torus check of Lemma T (h764). On every frozen state of the odd corpora of side 3 (637) and side 4 (720) and of the files frozen_122 (762), frozen_133 (1500 of 12282), frozen_223 (1500 of 175314), for each axis all chains of the axis have one defect: 5119 of 5119 states, three axes. Values seen: 0, +-2, +-4, +-6, +-8; never odd. Flat eps is a theorem of the torus (Lemma T), and the corpus is its check.

Lemmas

Tags: proved here, no second reader (hand proof by me, checked exactly on the data named); computed; solver; conjecture.

Lemma P (P^x per class; proved here, no second reader; checked exactly, residual 0 on every model, h762, two forms). Let n be a hole plane (A-holes for n even, B-holes for n odd) and v a class value of the holes (their residue is that of the planes n +- 2). For an A-hole O of value v, in the d-family, the upper bridgeheads O + (1,1,-1), O + (1,-1,1) on B(n+1) have d = v + 2, v - 2 and the lower ones O + (-1,1,1), O + (-1,-1,-1) on B(n-1) have d = v; in the s-family the roles of upper and lower are exchanged; at a B-hole the sides are exchanged for both families. Summing P^x over the L holes of value v on plane n, every vertex of A(n+-2) of value v is a methylene of exactly one of them and every bridgehead of the split side is a bridgehead of two: k_d[n+2][v] - k_d[n-2][v] = k_d[n+1][v+2] + k_d[n+1][v-2] - 2 k_d[n-1][v] (A-holes), and the three other forms with the split moved as stated. Summed over v this is the recurrence of Lemma 6. Proof. The bridgehead algebra above and P^x. \(\square\)

Lemma W (wave equation; proved here, no second reader; in the row space of the window’s equations and exact on every model, h763 (6), h766 (2)). For every hole plane n, both families, every class value v of the holes: k[n+2][v] + k[n-2][v] = k[n][v+2] + k[n][v-2]. Proof. Law C at a hole O: X(O+2e_x) + X(O-2e_x) + Y(O+2e_y) + Y(O-2e_y) + Z(O+2e_z) + Z(O-2e_z) = 2. The methylenes O +- 2e_y have d = v +- 2 and O +- 2e_z have d = v -+ 2 (for s, both have s = v +- 2). Sum over the L holes of value v on plane n. The x-methylenes give k[n+2][v] + k[n-2][v]. Each vertex u of A(n) of value v + 2 is O + 2e_y for the hole O = u - 2e_y and O’ - 2e_z for O’ = u + 2e_z, both of value v, so it contributes Y(u) + Z(u) = 1 - X(u); likewise for v - 2. With L vertices in each of the two classes, k[n+2][v] + k[n-2][v] + 2L - k[n][v+2] - k[n][v-2] = 2L. \(\square\) Its general solution on the lattice (u, w) = (n/2, v/2) is k = phi(w - u) + psi(w + u): the counts on each sublattice are a superposition of two sheets, each advancing one class per cube (delta v = 4 per delta n = 4), in opposite senses. Two consecutive A planes determine all A planes, and (12,4,4)‘s model 0 above has both sheets present (phi carries the rods’ class, psi the rest). This is the structure item 7 saw and could not name: the two rigid models are the two cases in which the data on the cage plane pair leaves one sense, and the dense models are sums.

Lemma D (the defect equation; proved here, no second reader; a law, h763 (6)). With e_d(m) = k_d[A m] - k_d[B m+1] and e_s(m) = k_s[A m] - k_s[B m-1]: for every A-hole plane n, e_d(n)[v+2] + e_d(n)[v-2] = 2 e_d(n-2)[v] and e_s(n)[v+2] + e_s(n)[v-2] = 2 e_s(n+2)[v]. Proof. Lemma W on the A planes minus Lemma P at the A-holes, both families. \(\square\)

Lemma T (one defect per axis on the torus; proved here, no second reader; two proofs; checked on 5119 frozen states, h764). In every real solution of one-hot + (T2) on the whole torus, every x-chain of both families has the same defect eps_x = (#type-x on its A plane) - (#type-x on its B plane); likewise eps_y, eps_z. Proof 1. Over Z_g the map e -> (e[v+2] + e[v-2])/2 multiplies the m-th Fourier mode by cos(pi m/g) times a phase; by Lemma D, going once round the x-circle (2a A planes) multiplies each mode of e_d on a fixed plane by cos(pi m/g)^(2a), so every mode with 0 < m < g vanishes, e_d(n) is flat for every n, and the m = 0 mode is the same on all A planes; e_s alike. Proof 2. In the parametrisation (C), X = 1 - F_y + F_z - sigma(alpha + beta) with sigma = +1 on A, -1 on B. The B vertices of a d-chain are b_i = a_i + d_0 = a_(i+1) + d_1, so b_i lies on the {0,2} and {0,3} chains of a_i and on the {1,3} and {1,2} chains of a_(i+1); the sums of F_y and of F_z over the A and over the B vertices of the chain therefore agree, and the difference of the X sums is -2L(alpha + beta), the same for every chain; for the s-family use b_i = a_i + d_2 = a_(i+1) + d_3. \(\square\) Proof 1 uses the closing of the rod axis and nothing of the transverse circles; the labels’ modulus 4g enters only through the class structure. On the window neither e = 0 nor flatness is linear (h763 (2): not in the row space on any chain of any window), so Table E’s flatness is an integral consequence: by Lemma D the defect of the cage pair is a binomial smoothing of the far pair’s, integral at every step.

Lemma P0 (parity; proved here, trivial). In any ice state every closed chain has an even number of kinks, so every x-chain has an even number of type-x vertices and eps_x is even (corpus: only even values). Not used.

Corollary (the reformulation; solver on four cells for the integral step). Given the pattern on the torus, (V) holds iff eps_x >= 1 iff n_x(A) > n_x(B): (V) gives eps >= 1 on the chain of the lower rod, hence everywhere by Lemma T; the negation gives eps = 0 on [-3, 2g-1] by Table E. “Pattern + eps = 0” is satisfiable on [-3, 2g] (the two rigid models) and unsatisfiable on [-3, 2g+1] (it would be a model of (V) with a type-x vertex on B(-1)): the reformulation keeps the reach of (V) and reduces nothing.

Proposition N (the counts admit the negation; computed exactly, h767, four cells). Put, on every plane and both families, k[n][v] = [w - u = 1] + [w - u = -1] mod 2g, u the A plane of the chain over 2, w = v/2: two unit sheets of one sense, one through v_0 = (0,0,0) (A plane -2, d = s = 0) and one through v_1 = (4,0,0) (A plane 2, d = s = 0), B planes equal to their A plane. It satisfies Lemma W on every plane, Lemma P at every hole plane, Lemma 6, eps = 0, the bounds 0 <= k <= L, the pins (both rods’ classes >= 1; the class of beta on B(-1) <= L - 1), and the negation (B(-1) has a positive class), round the whole torus of (12,4,4), (12,4,8), (10,5,5), (12,6,6). So no induction in the kink vectors, with every law they satisfy and the integral facts of Table E, can reach a contradiction. The same is shown by h766 (5): the A-plane profile of every one of the 488 enumerated models, including the two rigid ones per cell, extended by the recurrence of Lemma W round the x-circle, returns to itself and stays within [0, L].

T2. The hand step, and where it stops

Done: Lemmas W, P, D, T are the relations between the kink vectors of consecutive grid pairs, uniform in g and cyclic in the label; the closing of the torus enters in Lemma T through the rod axis, and the modulus 4g through the classes. Not done, and not doable in this object: the closing. Iterating Lemma W round the g labels against the pins at the hole contradicts nothing (Proposition N), because the counts are blind to which L-vertex class positions are kinked. The integral facts of Table E (flat eps with the pattern; eps >= 0 at 2g-2; eps = 0 with the negation at 2g-1) are not derived by hand; their reach 2g-1 is one less than (V)’s, and by the corollary they do not shorten (V).

T3. What is left, and a stop rule

1. The one relation which, if proved, closes (V): with the pattern, the chain of the lower rod has more kinks on its A plane than on its B plane (eps_x >= 1). Status: equivalent to (V) given Table E; reach 2g+1 on the four cells; no easier.
2. The object that could carry the obstruction is the next refinement: the joint matrix M[n][v_d][v_s] of type-x counts per (d, s) cell (L/g vertices each), on which the rigid sheet is a graph (sheet report). Law C summed over a (d, s) class of holes gives X[n+-2] on the cell plus Y and Z on four different cells, so the wave structure becomes a three-type system; I did not pursue it (stop rule: no new quantity).
3. A hand proof of the integral flatness of Table E (i) would be a lemma of reach 3 with the pattern, uniform in g if true on every cell; it is the cheapest unexplained integral fact here.
4. Stop rule for this object: the kink vectors per chain class are closed as a route to (V) by Proposition N. Do not enumerate more models or sweep windows for them.

Scripts and timings

All new, in experiments/08_frozen_structure/scratch_h/, none existing modified, nothing committed; saved models .tmp/h761_*.pkl; logs .tmp/h761_enum.log, h762_*.log, h763_*.log, h764_corpus.log, h765_all.log, h765_sweep.log, h765_sweep2.log, h766_all.log, h767_witness.log.

Solver wall in all 1034 s = 17.2 min of the 30 allowed; five batches were killed at the 120 s cap (the plain runs and (10,5,5) at [-3,4], [-3,5]), their finished queries kept. One solver child at a time. Every UNSAT row of Table E has a SAT control in the same child, and the enumerations’ final UNSAT (completeness at Q = 2g) has the two models before it.

Rules kept or broken

Kept: the reading list in order; cells, form, type model, no R; the 30-minute solver budget; one child at a time, this Mac only, no job over ten minutes; scripts h760 to h767 with docstrings and usage lines, no existing script modified, no commits; temporary files in .tmp/ and $TMPDIR; no Fourier coefficients or phases of the types on windows beyond the root-of-unity sums the brief asked for, which I have identified with chi_d; no weights or heights of (C) except in Proof 2 of Lemma T, which is a derivation, not a computation; no Statement R; no certificates; no reach sweep for (V).

Bent: (1) the model enumeration runs through the h560 worker (CaDiCaL in a child under subprocess.run(timeout=), SIGKILL at the cap), as agent screw’s did, because h32_cap.run_batch has no blocking-clause mode; the cardinality queries of h765 go through h32_cap.run_batch. (2) Table E goes beyond the enumerations: 23 batches of cardinality queries on windows from [-3,3] to [-3, 2g-1], with and without the negation, and three on (T2) alone. They test the relation T1 found, not (V), and they are what turned a sample property into a solver fact; the window sweep for flatness is a sweep for the defect, not for (V). (3) Four short inline python -c patches edited my own new scripts; three shell heredocs were used early for the same purpose, against the standing note, and none touched anything outside .tmp/ and the new scripts. (4) Lemmas P, W, D, T are proved by me with no second reader; W, P and D are verified to lie in the row space of the window’s equations, T on 5119 states.