The near-miss of (V′) at the one-sided threshold is one sheet on the labels of the x-chains, given by one formula at every g; opening the transverse torus does not remove g but replaces it by the number of chain labels of the surface that is left, and on the plane (V′) is false

Tags: proved, computed (exact, no solver), solver (SAT verdict under a cap), conjecture. New scripts (all in experiments/08_frozen_structure/scratch_h/): h560_lib.py, h560_worker.py, h561_nearmiss.py, h562_show.py, h563_cells.py, h564_where.py, h565_defects.py, h566_backbone.py, h567_reach.py, h568_cyl.py, h569_formula.py. The geometry and the encoders are those of h360_lib.py (agent check3; direct encoding of (T2), no auxiliary variables). Every solve runs in a child process under subprocess.run(timeout=...). Saved models are in .tmp/h561_*.pkl, logs in .tmp/h561_*.log. No existing script was modified; nothing under docs/, no record file and no git was touched.

Setting throughout: cell \((a, b, c)\), rods along \(x\), \(g = \gcd(b, c)\), the A-hole \(O = (2,0,0)\), the rods \(v = (0,0,0)\) and \(v' = (4,0,0)\), the four literals of (V′): \(v, v'\) of type \(x\), the lower bridgehead \(O + (-1,1,1)\) of type \(y\), the upper bridgehead \(O + (1,1,-1)\) of type \(z\). The negation: some B-vertex of the grid \(dx = -1\) (relative to \(O\)) is of type \(x\). Type-only model (one-hot and (T2)), no signs. “Window \([-p, q]\)”: (T2) on the hexagons all of whose vertices have \(-p \le dx \le q\). On a grid $x = $ const put \(s = y + z\) and \(d = y - z\); modulo \(4g\) they are well defined on the torus, the classes of \(d\) on a grid are exactly the x-chains of the family \(\{0,1\}\) (step \((0,2,2)\)) in that grid and the classes of \(s\) those of \(\{2,3\}\) (step \((0,2,-2)\)) (computed from the definitions: a chain of \(\{0,1\}\) has constant \(y - z\) and \(2bc/g\) vertices on each of its two grids, which is the size of a class). A class of \(s\) meets a class of \(d\) in a cell of \(2bc/g^2\) vertices.

1. Verdicts

1. Phase 1: there is a common structure, and it is the same at every \(g\) (solver + computed, \(g = 3\) to \(7\)). On the one-sided near-miss window \([-3, 2g]\), one grid short of the corner \((3, 2g+1)\), the set of type-\(x\) vertices of the window is determined up to exactly two choices: after two models, blocking both, the third query is UNSAT. This holds on \((12,3,3)\), \((12,3,6)\), \((12,6,9)\), \((12,4,4)\), \((12,4,8)\), \((16,8,12)\), \((12,5,5)\), \((12,5,10)\), \((12,6,6)\), \((12,6,12)\), \((16,7,7)\), and on the mirror window \([-2g, 3]\) at \(g = 4, 5, 6\). (On \((12,10,15)\) two models were found and the third query was stopped by the 300 s cap.) Tori with the same \(g\), square or not, give the same two sets in label coordinates.

2. The sheet, exactly (computed on the saved models, \(g = 3\) to \(7\)). On every grid of the window the type-\(x\) set is a union of whole cells, one cell in each class of \(s\) (a graph over the chains of \(\{2,3\}\); on the mirror window, over those of \(\{0,1\}\)), so each grid has \(2bc/g\) vertices of type \(x\) on both sublattices. On the A-grids \(x = 6, 8, \dots, 2g+2\) (\(v\) at \(x = 0\)) it is given by one formula, modulo \(4g\):

   • orientation \(+\): \(D(s) = x\) for every class, except \(D(x-4) = 8 - x\) and \(D(4-x) = 4-x\);
   • orientation \(-\): the image under \((y,z) \mapsto (-y,-z)\): \(D(s) = -x\), except \(D(4-x) = x - 8\) and \(D(x-4) = x - 4\).

   Each of the 26 saved models fits exactly one orientation on every one of these grids and the other on none (h569_formula.py; \(g = 3\): 2 grids, \(g = 7\): 6 grids). In words: a sheet on the plane \(d_2 \cdot p = 0\) (orientation \(+\)) or \(d_3 \cdot p = 0\) (orientation \(-\)) through the rod \(v\), advancing one chain label per cube, and two defects, each one cell per grid, riding on a chain of axis \(y\) (step \((2,0,2)\), at \(y \equiv 2 \bmod 2g\)) and a chain of axis \(z\) (step \((2,-2,0)\), at \(z \equiv 0 \bmod 2g\)), each moving one label per two grids relative to the sheet. The drift is along one of the bond directions, as the brief guessed, but the sense is not forced: the two models are the two senses. Near the cage (\(x \le 4\)) the pattern is different and is the same in both models on the grids \(x = -1, 0, 1\).

3. Why \(2g\) (conjecture, from item 2). In orientation \(+\) the second defect lies on a cell of the sheet exactly when \(2x \equiv 4 \pmod{4g}\), that is at \(x = 2\) (the cell of the methylene \(O + 2e_y\) of the cage) and next at \(x = 2g + 2\), the last A-grid of the window; the two defects meet each other at \(x = 4\) and next at \(x = 2g+4\). The window that is one grid longer is UNSAT. The obstruction is therefore that the configuration of sheet and defects returns, after one circuit of the label circle \(\mathbb{Z}_g\), to the relative position it had at the cage, where the cage supported it. This is the linear reach, with the constant read off.

4. Every target has reach \(2g \pm 1\) (solver, \(g = 3, 4, 5, 6\)). For each vertex \(b\) of grid \(-1\) separately, the least \(q\) such that \([-3, q]\) forces \(b\) not of type \(x\) lies in \(\{2g-1, 2g, 2g+1\}\) (\(\{5,6,7\}\), \(\{7,8,9\}\), \(\{9,10,11\}\), \(\{11,12,13\}\)). The targets of reach \(2g+1\) are exactly the type-\(x\) vertices of grid \(-1\) in the two rigid models. The “near” and the “far” targets are not distinguished: the reach is global in the transverse plane.

5. The rigid sheet is special to the one-sided corner (solver). One grid short for a fixed target, or at the symmetric corner \([-(2g-2), 2g-3]\), the models are not rigid and not graphs: e.g. \((12,5,5)\), \([-3,8]\), target \((1,-3)\): 20 distinct models, 28 of 50 type \(x\) on A-grids and 18 on B-grids (backbone: 8 free per grid); at \([-8,7]\) some models are the sheet and some have 11 per grid concentrated on two classes of \(s\) and two of \(d\). So the sheet is the shape of the extreme near-miss, not the shape of every solution of the negation.

6. The open-torus form of (V′) does not remove \(g\) (solver, 24 cylinders; the most important negative result). Cut the transverse torus along one axis (remove every hexagon with a vertex on the grid \(y = -2b\), or \(z = -2c\)) and take the window \([-20, 20]\) on \(a = 12\). Then (i) the targets at distance 1 from the cut are never excluded (the negation lives at the cut, as the note says); (ii) if the circle left closed is not longer than the one cut, every other target is excluded; if it is longer, no target at all is excluded, whatever \(g\): e.g. \((12,4,8)\) cut \(z\) (closed circle 16): 54 of 62 excluded; cut \(y\) (closed circle 32): 0 of 62; the same dichotomy on \((12,4,6)\), \((12,3,6)\), \((12,5,10)\) with \(g = 2, 3, 5\) and on \((12,4,5)\), \((12,5,4)\) with \(g = 1\). (iii) On a cylinder whose closed circle is \(4b\), the reach below the cage (upper side 4) is \(2b + 1\) for \(b = 4, 5, 6\) (\(2b-1\) at \(b = 3\)), independent of \(g\): \((20,6,8)\) has \(g = 2\) and reach 13, where the torus \((6,8)\) has reach 3. (iv) Cutting both transverse circles makes the negation satisfiable (ucore §4, not re-run). So the quantity that sets the reach is the number \(G\) of chain labels of the transverse surface: \(G = g\) on the torus, \(G = b\) on the cylinder closed in \(y\), \(G = \infty\) on the plane where (V′) is false. There is no formulation of (V′) “with the transverse torus open so that \(g\) plays no part”: opening it either makes the statement false or replaces \(g\) by a larger label count.

7. Phase 2 and Phase 3: not achieved. No invariant with properties (a) to (c) of the brief was found, and no proof of the closure step is offered. §4 says what is missing.

2. Observations of Phase 1, with the data

2.1 Rigidity (h561_nearmiss.py CELL 3 2g --k 6)

“Models” count distinct type-\(x\) sets on the grids of the window (blocking clause on the type-\(x\) literals of the window). The type-\(y\)/\(z\) split may vary. The pattern alone is SAT in every case (it is the first query of each run).

2.2 The label tables (h563_cells.py, h565_defects.py)

Each grid row lists \(D(s)\) for the classes of \(s\) in increasing order; e.g. \((12,6,6)\), model 0, A-grids \(x = 6, 8, 10, 12, 14\): 2,6,6,6,6,22 / 8,0,8,8,8,20 / 10,22,10,10,18,10 / 12,12,20,12,16,12 / 14,14,18,14,14,14 (classes \(s = 2,6,\dots\) or \(0,4,\dots\)). \((12,6,12)\) gives the identical table; \((12,3,3)\) and \((12,6,9)\) give identical tables (models in the other order). The B-grid \(x+1\) carries the same cells as the A-grid \(x\) with the two defects moved by \(\pm 2\) in \(s\) (read off the tables; not tested by a formula).

2.3 The ending

At the far end of the window the sheet does not end: it is present on the last grid, where the second defect sits on a cell of the sheet (item 3 of §1). Beyond the window the grids are unconstrained. In ucore’s model (\(L=4\), \([-6,5]\)) the structure “stopped at the gap” in the same way.

2.4 The cut (h561 ... --cut, h564_where.py, h566_backbone.py, h568_cyl.py)

With the torus cut and the layers ample the negation has many models (6 of 6 distinct on \((12,4,4)\), \((12,5,5)\)), dense on the A-grids (24 to 42 of 50) and nearly empty on the B-grids; the type-\(x\) vertices of grid \(-1\) (1 or 2 of them, up to 7 with the cut along \(z\)) all sit at \(y = \pm 9\), next to the cut at \(y = -10\). Backbone on \((12,5,5)\), cut \(y\), \([-20,20]\): the near target is UNSAT, and with the far target (adjacent to the cut) 40 of the 50 vertices of grid \(-1\) are forced not of type \(x\), the 10 free ones being those next to the cut. There is no sheet in these models; the cut absorbs the defect.

The cylinder survey (window \([-20,20]\), \(a = 12\); “excl.” = targets of grid \(-1\) forced not of type \(x\), of all non-bridgehead targets; survivors all at distance 1 from the cut when excl. > 0):

On \((20,4,8)\) cut \(y\) the result 0/62 persists with \([-36,36]\) (solver). Reach below the cage with the upper side 4 (h567_reach.py 20,b,c 4 36 --cut z -2c --mirror, closed circle \(4b\)): \(b = 4\): 9 on \(c = 5, 6, 8, 12\); \(b = 5\), \(c = 10\): 11; \(b = 3\), \(c = 6\): 5; \(b = 6\), \(c = 8\) (\(g = 2\)): 13. On the square cylinders \((20,4,4)\) and \((20,6,6)\) the upper side 4 is not enough (6 of 30 and 10 of 70 excluded up to 36 below), while \([-20,20]\) excludes all but the edge; I did not locate their corner.

2.5 Verdict of Phase 1

There is a common structure at the extreme near-miss, and it is literally the same object at every \(g\) from 3 to 7, square and not, described by one formula in the chain labels modulo \(4g\). The brief’s reading (a plane normal to a bond direction, drifting at a fixed rate round a label circle of circumference proportional to \(g\)) is confirmed, with two additions: the sheet carries two defects on chains of axes \(y\) and \(z\), and the sense of the drift is not forced. In the second kind of near-miss (cut torus) there is no sheet, and the survey shows why the route’s first step cannot be taken as stated: with the torus open, \(g\) is replaced by the label count of what is left, or the statement fails. The route is not closed by Phase 1, but its formulation must change: the closure step has to be stated on the closed label circle, not on an open torus.

3. The invariant and the proof: what was tried

The candidate suggested by §1 item 2 is the label phase: on each grid, the type-\(x\) set as a map \(D : \mathbb{Z}_g \to \mathbb{Z}_g\) from the chains of \(\{2,3\}\) to those of \(\{0,1\}\). In the rigid models \(\sum_s D(s) \equiv (g - 4)x + 12 \pmod{4g}\) on the A-grids (orientation \(+\); computed from the formula), i.e. the phase advances by a fixed amount per grid, which is (b) of the brief. (c) holds in the sense that the grids \(x = -1, 0, 1\) are the same in both models. But (a) fails: the graph property is not a consequence of (T2), of C and \(P^k\), or of (C), for solutions of the negation in general. §1 item 5: one grid short for a fixed target, or at the symmetric corner, the type-\(x\) set of a grid is not a union of cells, its count is not \(2bc/g\) (28 and 18 of 50), and the models are many. The phase is defined only on the extreme solutions, so it cannot be the quantity that a proof carries from the cage to the far end. I found no quantity defined on all solutions of the negation, on a bounded set of grids, that reduces to this phase on the rigid ones.

Where integrality would enter, if the phase were available: the graph property itself (each chain of \(\{2,3\}\) meets the type-\(x\) set of a grid in exactly one cell) is a 0/1 statement of the kind of Lemmas 8 and 9, a function of two chain labels with values 0 and 1 that is forced to be a graph. The linear relaxation cannot see it (the LP of the note, item 3, is feasible). I did not find a derivation of it.

The only per-grid quantity that is conserved in every solution is linear and known: summing \(P^x\) over a plane of holes gives \(n_A(x+2) - n_A(x-2) = 2(n_B(x+1) - n_B(x-1))\) and the mirror, where \(n_S\) counts type \(x\) on a grid; on a slab of bounded counts this makes the counts constant on each sublattice. It is linear, holds equally in the rigid (10/10 at \(g=5\)) and dense (28/18) models, and cannot distinguish them.

4. What is missing (Phase 2 and Phase 3)

1. A statement on the closed label circle, not on the open torus. §1 item 6 shows that any uniform statement must refer to the chain labels of the transverse surface: on the plane the negation is satisfiable, on a cylinder the reach is \(2b + 1\) in the closed half-length \(b\) whatever \(g\). What is wanted is: in a solution of the negation on the slab \([-3, q]\) over the closed torus, some \(\mathbb{Z}_g\)-valued (or \(\mathbb{Z}_{4g}\)-valued) phase is defined on every grid from the cage onwards, is pinned at the cage, and advances by one label per two grids. Closure after one circuit (\(q = 2g+1\)) would then be a counting step.
2. The obstacle to 1. The phase is visible only in the extreme solutions (§3). For every shorter window the solutions of the negation are dense and not organised by chain labels, so the phase would have to be extracted as an invariant of a general solution (for instance an average over the cells of a grid, a winding number of the type-\(x\) set round the label torus, or a first moment of the counts per chain), and I did not find one that is (i) defined on all solutions, (ii) moved by exactly one label per two grids, (iii) not a linear combination of laws. Requirement (iii) is forced by the LP result; any such invariant must use 0/1 somewhere.
3. Tests one could run next (not run): compute, for each grid of dense near-miss models, the number of type-\(x\) vertices on each chain of each family and each cell, and look for a moment (e.g. \(\sum_\sigma \omega^{\sigma} n(\sigma)\) with \(\omega\) a \(g\)-th root of unity, a Fourier coefficient of the chain counts on \(\mathbb{Z}_g\)) whose argument advances by \(2\pi/g\) per two grids in all models; if one exists it is the candidate for (ii), and its modulus would have to be bounded below by an integrality argument. The characters of Lemma 11 at which three families are supported are exactly the functions of \(d_l \cdot p\), and the sheet lies on \(d_2 \cdot p = 0\); this is the place I would look.

No lemma of a proof is claimed, so none was tested as Phase 3 asks.

5. What failed and why

• Reading the sheet off one model per setting: models of the negation at non-extreme windows are numerous and dense; only the one-sided extreme is rigid. Restricting to it gave the clean result, but that restriction is also why no invariant of general solutions came out of it.
• The cut as a way to remove \(g\) (§1 item 6).
• Two interpretations I checked and dropped: that ucore’s sheet on \(y + z\) and this one on \(y - z\) differ (they are the same up to the choice of bridgeheads, which swaps the two x-families), and that the defects are errors of the solver (they are in both models and in every cell).

6. Rules

• One solver process at a time: broken briefly. A background survey (h567_reach.py on eight cylinders, one solver each) was still running when I started the near-miss runs on \((20,6,8)\), \((20,4,8)\) and the \(g = 7\) batch; for about two minutes two solver processes ran together. All were small (the largest single solve 29 s, apart from one capped at 300 s). No other rule was broken to my knowledge. One shell heredoc (empty, a no-op) was issued by mistake and did nothing.
• All UNSAT verdicts above have SAT controls on the same clause set (the pattern alone, or the earlier models of the same run).

7. Commands run

From the repository root with PYTHONPATH=<repo>:<repo>/experiments/08_frozen_structure:<scratch_h> and TMPDIR=<repo>/.tmp; scripts in scratch_h/.