Geometric conflict memory completes the nonacube proof
An exact anchor-constraint encoding of learned failures completes the two-corona search. The resulting certificate independently verifies \(H<2\). The working construction uses many private channels; compact rank-one and rank-three markings remain experimental.
Which variants worked?
| Variant | Outcome | Search time | Scope |
|---|---|---|---|
| Ordinary Glucose, placement-only formula | UNSAT; checked | 26.3 s | Baseline |
| Placement-only failure learning; ordinary watchers | UNSAT; checked | 54.4 s | All learned literals name selected tiles |
| Affine anchor counters | UNSAT; checked | 113.7 s | Published proof and patched solver |
| Anchor counters plus 16 root symmetries | Stopped; unknown | 385.8 s last checkpoint | 25.6 million patterns; no completed certificate |
| Compact rank-one / rank-three allowed sets | Fit one core | Under 0.2 s per fit | Uncertified outside the training subsets |
Single exploratory runs on the same host; branching and propagation orders differ. The portable geometric rerun took 107.1 seconds and produced the identical proof. The symmetry run overran its requested 300-second limit because of an interruption-polling bug, then was terminated; the portable source fixes that bug. A fit is not a full search.
Inspect a learned geometric channel
These are actual nonoverlapping patterns extracted from the completed proof. Each has its own channel at the fixed root anchor. Toggle roles to see why that channel rejects its full pattern and accepts every proper subset.
How the geometric encoding works
Give a forbidden pattern of \(k\) roles a shared vector at the root anchor:
\[z_1+\cdots+z_k=1.\]A tile in role \(i\) contributes \(z_i=0\). Put its atom at prototype offset \(-c_i\), where \(c_i\) is its center relative to the root. That atom reaches the active anchor exactly when the intended placement is selected. A missing role is a wildcard.
All roles force every coordinate to zero, contradicting the unit sum. If role \(j\) is absent, \(z=e_j\) satisfies this channel. The solver compiles those equations into counters: one missing role excludes its tile; no missing roles produce a conflict.
This may also be read as a scalar allowed-state channel: begin with \(\{1,\ldots,k\}\), and role \(i\) deletes state \(i\). That changes the algebra, but leaves the large alphabet and channel store to carry the information.
What the small-rank trials found
The training example was the previous five-tile cold-search core, including all 31 proper subsets. Membership variables were tied by the full cubic symmetry group, including each tile’s own symmetries.
With a freely chosen failure anchor, scalar trivial action, scalar determinant action, and the natural three-coordinate action all fitted the example. Requiring disagreement at the actual dead point made both tested scalar models unsatisfiable; the rank-three model still fitted.
But that rank-three fit rejected 40 of 686 neighboring pairs at the smaller successful anchor range. The first rejected pair has minimum frontier degree 28 and no forced move. It passes the unmarked frontier test. The free-anchor trivial scalar and rank-three fits each rejected 288 pairs, with a first example of degree 41.
The scalar determinant fit passed all pair tests, but has no certification for larger patches. None of these small-rank hypotheses was used to prune the completed proof search.
The boundary conditions matter
The root is a planar cross of nine unit cubes on the integer lattice. All three planar orientations are allowed. A two-corona must cover the full face/edge/vertex halo of the root and every selected tile touching it. Outer tiles do not acquire another surround obligation. All overlaps remain forbidden, including outside the required region.
The exact reduction has 8,140 physical placement variables, no auxiliary variables, and 569,020 clauses. Its UNSAT certificate establishes the upper bound under these conditions. The previously checked one-corona witness supplies the lower bound, hence \(H=1\) for this lattice-corona convention.
Learned failures retain the fixed root and its two-corona obligations. They are not automatically forbidden unrooted packings. Only the root anchor is active. Translating or rotating a rule requires transporting its context as well. The completed run’s learned store is not closed under all root symmetries.
What this does—and does not—establish for GCTS
It establishes that a complete proof can use arbitrary-order failure constraints expressed as anchor sections. The counter engine directly made 1,423,533 exclusions and detected 13,726 conflicts. Learned units are root-level exclusions; learned clause objects remain as proof reasons, and newly learned asserting exclusions enter the common trail directly.
It is intentionally an exact re-encoding of learned conflict memory. The geometric lookup compiles back to the same placement identifiers. There are 34,893,205 cumulative role atoms, with separate channels for separate patterns; deleted rules cease to propagate. The maximum active storage was not measured. This is not a bounded-rank marking on an unadorned tile.
The reference GCTS frontier scheduler is also not implemented here: Glucose uses its own branching, restarts, and backjumps. Base overlap and coverage clauses still propagate conventionally. Affine sections are an experimental extension of the fixed-value agreement rule.
The next substantive step is compact, reusable, equivariant markings with every extra exclusion justified, followed by an independent frontier-search implementation. The rank-three fit shows why testing proper subsets of one bad patch is insufficient: other viable patterns must also be protected.
Finite synthesis details
The scalar alphabet was \(\{-2,-1,0,1,2\}\); the vector alphabet was \(\{-1,0,1\}^3\). A mark is an allowed subset; the full alphabet is a wildcard. Anchor coordinates were odd half-unit integers in \([-e,e]^3\). The free-anchor fits succeeded at \(e=5,7\) and failed at \(e=3\). Gap-anchored fits were tested at \(e=5,7\).
The finite scalar failures do not rule out all rank-one encodings. Pairwise frontier viability does not prove a complete corona or infinite extension. These results identify extra, unproved restrictions in the fitted marking; they do not supply global positive tiling witnesses.