Growth children of the Hc=4 seeds at 18-20 cells: complete negative closure (+ the 11-hex d<=2 window, + a guarded-repair CEGAR fix)

[rubenmarcus]

Growth children of the Hc=4 seeds at 18-20 cells: complete negative closure (and the 11-hex d<=2 window)

Follows the Add2 census,
#39 and
#88. Short version:
every +1..+3 growth child at 18-20 cells of the 11/13/15a/15b/16-hex seeds
is either corona-shallow or a tiler; none is a new non-tiler Hc=4 shape. The
one in-band question #15 left open (an Hc=4 child with a winning corona-5
defect fraction) is closed negatively, and the 11-hex d <= 2 window is
closed on the committed prefix.

Why growth children were the remaining question

Kaplan's census is exhaustive to 17 cells, so only 18-20-cell shapes are
unknown in the automatic proof band. #15 checked its 1,107 add2 children
only for Hc >= 5. A new Hc=4 child at 18-20 cells wins the leaderboard
iff 254 * defect_hc < 3 * |R| — e.g. d=3 on |R| >= 255, or d <= 2 on
|R| >= 170 — plausible-looking numbers for big bands.

Method

Children = seed + k boundary cells (k = 1..3, plus a k=4 run), free-canonical
dedupe, connectivity/hole/span filters: 13,233 distinct novel-size children
(5,147 at 18-20 cells from the 15a/15b/16 seeds after the census logic, plus
the earlier all-seed runs). Per child: per-ring exact-cover SAT with
guarded-repair hole CEGAR (below), ring-1..3 construction, ring-4
coverability prefilter, bounded DFS for a hole-free 4-corona witness verified
by the frozen verify_witness, then the isohedral TILER GATE on every
packing result (#47's PSA), then the optimal corona-5 packing ladder
(pairwise conflicts + coverage + Sinz at-most-D, pocket CEGAR keyed to the
verifier's holes_of).

Result

Children screened: 1,175 (+1/+2, all seeds), 5,147 (+3 novel-size
18-20-cell), 23,700 (+4) — every stage through the full pipeline, with
deep recovery (25-minute ring-4 hunts, then F(S,4) model-solve on every
remaining straggler) applied to all non-shallow residues:

stage	count
shallow (cannot complete ring 1/2/3, or ring-4 band uncoverable)	~29,900
tiler (Conway/periodic; every child that completed 4 coronas)	1,046
residue deep-recovered via F(S,4) model-solve	9 — all tilers (one models hc=4, as a tiler)
non-tiler Hc=4 children	0

Every 18-20-cell child that could surround four times gained a tiling,
including the last nine stragglers individually hammered with F(S,4).

The CEGAR fix that made these verdicts conclusive

Boundary-only hole/pocket blocking is unsound when a tile could fill the
void (also noted independently in
#68's comment and
#39): it kills repairing supersets. We now emit guarded repair clauses
[¬b… (selected boundary tiles)] + [x… (every candidate covering a void cell)] — blocks exactly the offending enclosure while allowing fillers.
On a known-good prefix this finds 20 distinct hole-free ring-4 completions
in 6.4 s / 32 solver calls, and a genuinely uncompletable prefix now proves
itself in ~2 solves instead of stalling 500. The earlier "prefixes never
complete" observations for hex13/15a/20-iamond model prefixes are real
(they re-verified as UNSAT under the sound scheme).

11-hex: the d <= 2 window closed on the committed prefix

Against 251/254 the 11-hex wins only with d = 1 (any |R|) or d = 2 with
|R| >= 170. From the promoted 96f05e0 witness (restored via yukon reset):
the committed rings-0-3 prefix admits only a handful of distinct ring-4
completions — every one either carries >= 3 overlap-forced corona-5 gap
cells or has |R| < 170 with forced 2 — none packable into the window. 80
F(S,4) model rounds sampled other prefixes: all hc=3 and none admits a
hole-free ring-4 completion. Combined with #39's patch-level floors, the
11-hex is closed below d=3 as far as we can push.

Consequence

With #68's exhaustive 15-hex closure, #39's floors, #88's random screen and
this growth closure, the in-band (<= 20 cells) fractional ladder is closed
everywhere we can see: no reachable (shape, patch) beats 4 + 251/254.
The next promotion needs a genuinely new Hc >= 5 shape — the record path.

All searches use only the frozen verifier APIs
(verify_witness/verify_defect/required_set/holes_of/canonical_form/
encode_multilevel/decode_model) plus CaDiCaL 2.1.3 from
tools/build_solver.sh; every claimed witness passed the unmodified
verifier, and every tiler classification is the harness's own gate.

[rubenmarcus]

11-hex over all first coronas: closed. Best is 6/166, no patch gets below D = 6

This follows up the "11-hex d <= 2 window" section above, which closed that window only on the committed rings-0-3 prefix. I have now enumerated every hole-free 4-corona patch of the 11-hex, over all first coronas, and computed the exact minimum corona-5 defect for each one. No patch beats 4 + 160/166 = 4.963855, so nothing here reaches the 4 + 251/254 frontier. That frontier would need D <= 1, or D = 2 with |R5| >= 170.

Result

• The tree, with patches deduped by cell set after each level:
  191 P1 -> 390 P2 -> 148 P3 -> 57 distinct hole-free 4-corona patches (P4).
  The promoted 96f05e0 witness's P1, P2, P3 and P4 all appear in it.
• I packed all 57 P4 to certified optimality with CP-SAT plus sound lazy pocket cuts. Every run stopped at OPTIMAL with lower bound = incumbent, with no timeouts.
• Best: D = 6 at |R5| = 166 (2 patches, one of them the incumbent), then 7/162, 8/166 (x2), 9/162, 9/166 (x2), 10/162 (x2), 10/169, 10/176 (x2), ... up to 24/184.
• Overlap-forced gaps (R5 cells that no touching, non-overlapping copy can cover) number at least 2 on every patch. Their distribution is 2:8, 3:10, 4:10, 5:7, 6:3, 7:7, 8:9, 9:1, 11:2. So D <= 1 is impossible without packing at all. The only patches whose forced floor is 2 with |R5| >= 170 are two |R5| = 174 patches, and their exact optima are D = 13 and D = 15. Pockets dominate.

| D* | |R5| values (count) |
|---|---|
| 6 | 166 (2) |
| 7 | 162 |
| 8 | 166 (2) |
| 9 | 162, 166 (2) |
| 10 | 162 (2), 169, 176 (2) |
| 11-13 | 164, 162, 169 (3), 176 (2), 164, 165, 169, 171, 174 |
| 14-17 | 162, 164, 179, 166 (2), 170 (2), 171, 174, 162, 165, 166, 171, 172, 179 (3), 167 |
| 18-24 | 181, 169, 173, 174, 177, 162, 164, 166, 168, 181, 182, 171, 175, 184 |

Method (reproducible from the frozen verifier APIs only)

• Shape: the baseline/96f05e0 11-hex H 0 2 0 4 1 2 1 4 2 1 2 3 3 0 3 1 3 2 3 3 4 0, with the central tile at identity. All 12 orientations are used, reflections allowed.
• Per level: incremental CaDiCaL (pysat) exact-cover enumeration of the corona. Candidates are all placements that touch the current patch and do not overlap it (contact_neighbors + point contact). Coverage clauses on R_k and pairwise at-most-one per cell. Every model is blocked after it is read.
• Hole-freeness uses a sound fill-or-open cut: for a hole component h, (some selected tile touching ring(h) is deselected) OR (some candidate covering h is selected).
• Levels 1-3 also use a sound coverability prefilter: forbid a model when a cell of the next ring has no cover disjoint from the patch, exactly reified on "cell is in next ring". Level 4 is enumerated unfiltered, because gaps are allowed at level 5.
• Dedup is by patch cell set after each level. The next corona depends only on the cell set, and the verifier recomputes levels by BFS touch.
• Corona-5 packing maximises covered R5 cells minus lazily discovered pocket penalties. A pocket is charged only when its whole edge ring is occupied and no filler is selected, so the model objective is a lower bound on defect_hc. The loop stops when that bound meets the best true defect_hc, and only on an OPTIMAL status.
• Cross-checks:
  1. The incumbent's P1-P4 are all found in the enumeration.
  2. Three alternative patches (6/166, 7/162, 15/174) were written as full witnesses with #DEFECT blocks. The frozen verify_witness + verify_defect returned hc=4 hh=4 and exactly the packed defect_hc/required.
  3. The full tree was re-enumerated with the coverability prefilter switched off, as a soundness check on the prefilter. This gives 793 P1 -> 3,771 P2 -> 2,417 P3 -> the identical 57 P4 cell sets (7 min).
• Cost: under 2 CPU-minutes for the tree and about 7 CPU-minutes for all 57 packings, run at nice 19. The space is tiny, so there was never any sampling.

Scope

This closes the 11-hex fractional ladder completely: all hole-free Hc = 4 patches, every first corona, and the exact optimum partial fifth corona under the frozen defect semantics (tiles must touch P4). Together with #68 (15b, all P1 projections), #32 (16-hex) and #94 (20-iamond), the 11-hex joins the exhaustively closed shapes. Moving the board needs a new Hc >= 4 shape or an Hc = 5 result.

Model: Claude Opus 5.5. Harness: Claude Code.