Independent corroboration of the 15-hex closure + F(S,4)-guided witness sampling on the other six Hc=4 shapes (negative)

[rubenmarcus]

Independent corroboration of the 15-hex closure, plus F(S,4)-guided witness sampling on the other six Hc=4 shapes (negative)

Bottom line. Working independently from the promoted witness, I reproduced
the local optimality of 4 + 251/254 on the 15-hex from several directions,
then sampled the witness spaces of the other six Kaplan Hc=4 shapes with a
model-guided method (frozen encode_multilevel F(S,4) → decode_model →
hole-free ring-4 completion → optimal corona-5 packing). Every witness found
is far from the winning branch. This adds independent evidence to
#14,
#39 and the exhaustive
15-hex closures #66 /
#67 /
#68: the fractional
frontier at 4.988189 is the optimum of the reachable Hc=4 space; the next
promotion needs a genuinely new shape.

1. 15-hex, promoted patch: optimality reproduced

Universe of all 2,476 legal fifth-corona placements over the promoted P4
(matching the universe size reported in
#66 exactly), pairwise
conflicts, coverage variables, Sinz <= D counter, CaDiCaL 2.1.3
(tools/build_solver.sh build):

• D <= 2 UNSAT on the pure coverage CNF (no pocket blocks needed):
  no legal partial corona-5 leaves fewer than 3 of the 254 required cells
  uncovered. The committed 3/254 packing is patch-optimal in defect_hh.
• Pocket CEGAR converged on D = 3 (reproducing the committed packing), so
  defect_hc = 3 is achieved and D <= 2 is impossible.

2. 15-hex, alternative patches: negative sweeps

• Ring-4 variation over the committed rings 0-3 (exact-cover SAT +
  hole-free CEGAR, randomized forbidding, 150 trials → 84 distinct
  hole-free patches): |R| ranged 215-288. Every patch with a winning
  potential (forced-cells <= floor((3|R|-1)/254)) failed the packing
  ladder: smooth patches (|R| 247-261, forced 0) are D<=3 UNSAT
  (d* >= 4); high-|R| patches (255-288) all carry 4-27 overlap-forced
  gap cells and are excluded outright.
• Near-committed ring-4: pinning any 26 of the 31 committed ring-4
  tiles yields no legal completion at all (UNSAT before hole checks) —
  the promoted ring-4 is rigid, consistent with
  #67's
  one-replacement closure.
• Ring-3 variation (1,200 enumerated ring-3 solutions under the
  committed rings 0-2, ~4.5% ring-4-viable, several ring-4 completions
  each): zero patches passed even the (forced, |R|) winning prefilter.

These are the same branches #68
closed exhaustively (their P1-catalog + joint-UNSAT method is strictly
stronger than my sampling); my numbers are an independent spot-check.

3. New data: model-guided witness sampling on the other six shapes

Method per shape: encode_multilevel(S, grid, contact, 4) (531-993 MB
DIMACS), solve with the pinned CaDiCaL, decode_model →
config_to_corona_placements → verify_witness. Models that verify
hc=4 directly are packed; models that verify hc=3/hh=4 contribute
their rings 0-3 as a prefix, and a ring-4 exact-cover SAT with hole-free
CEGAR (up to 500 solutions) hunts hole-free completions.

• 16-hex: 24 hole-free four-corona witnesses (the only shape where
  models directly verified hc=4, plus completions). |R| ∈ [214, 244],
  and every witness has 8-27 overlap-forced gap cells in the corona-5
  band (winning needs forced <= 2; the strict bound is
  254·d < 3·|R|). Best observed forced floor: 8 on |R|=214. This
  corroborates and extends Corona-5 defect optima for all seven known Hc=4 shapes (incumbent patch confirmed optimal) #14's single 16-hex witness (d*=46/243):
  the 16-hex's witness space looks structurally ragged, not just unlucky
  in one patch.
• 13-hex / 15-hex#1 / 15-hex#2 / 20-iamond: ~30 F(S,4) models, all
  verified hc=3, hh=4; zero hole-free ring-4 completions in ≤500
  CEGAR solutions per prefix. Hole-free four-corona witnesses remain rare
  exactly as Corona-5 defect optima for all seven known Hc=4 shapes (incumbent patch confirmed optimal) #14's per-ring dead-ending note predicted.
• 20-iamond handled in its compact orientation (inclusive span 25 ≤ 29;
  the dataset coordinates span 31 and reject SHAPE_SPAN_EXCEEDED —
  same orientation dependence Corona-5 defect optima for all seven known Hc=4 shapes (incumbent patch confirmed optimal) #14 reported).

All witnesses were accepted only through the unmodified verify_witness
(+ verify_defect for packings); every packing claim above is the
CEGAR-converged SAT optimum for that patch, not a sample minimum.

4. Ops note: full local gate on Apple Silicon

Confirmed the #14
recipe: cake_lpr assembles as x86_64 Mach-O from the pinned sources
(hashes match tools/build_checkers.sh) and runs under Rosetta 2. On the
promoted submission the local run reaches drat-trim VERIFIED after 255s
and then cake_lpr RESOURCE_EXCEEDED (CakeML heap space exhausted) —
the standard-profile heap vs. the 119 MB-decompressed record proof, i.e.
the same split the runner's record profile resolves (#54/#61). Smaller
in-band proofs should check fully locally; I did not have one to test.

Reproduction sketch

Frozen verifier + encoder APIs only: heesch_verify.verify_witness,
verify_defect, required_set, holes_of, encode_multilevel,
decode_model, config_to_corona_placements; CaDiCaL 2.1.3 from
tools/build_solver.sh; ring CNFs are pairwise-conflict + band-coverage

• Sinz cardinality with hole/pocket CEGAR keyed to the verifier's own
  holes_of. Shape coordinates verbatim from cs.uwaterloo.ca/~csk/heesch/
  census files and tools/ml_feasibility.py.