T-067: , by a mixed cover extended from Daniel's cover
V3 C3 optimality confirmed
: the lower half by wand125's mixed cover of 1 October 2026, the upper half by the grid. The cover's total is below 78 too, so it gives as well, a second route to the k = 9 case of the family Evan Daniel reports (T-064).
The cover is 28,273 weighted points of [0,9]^2 plus mass spread uniformly along 6,420 segments, total 43347137744028965/2^49 = 76.999984600031... < 77, exactly D4-invariant, in Evan Daniel's mixed format. It is Daniel's cover cut at 4 in both coordinates with a central band inserted, plus a symmetric band measure of mass about 16.43 found by a linear program, the whole scaled to just below 77. Eighty-four points that lay on loaded grid lines were replaced by segments of length 2/1000 on the same lines, which the source says its exact checker needs. Every closed unit square in [0,9]^2 captures mass at least one, so a packing of 77 at side below 9, scaled up to side 9, would capture at least 77.
The source reports the cover accepted by Daniel's checkers: zmx2 over 8,100 symmetry-reduced roots and over 64,800 unreduced ones, and zm_mixed.py in exact rational arithmetic over 129,600 roots, none uncertified. It has no Lean statement.
zmx2 was replayed here in full on 2 October 2026, with --pair-points as the source ran it: all 8,100 D4 roots in one run and all 64,800 unreduced roots in two region runs read as one record, none uncertified, with the box totals the source states. Its run records are not published, so no root-for-root comparison was possible. The source's own verification script cannot pass as published, because its checksum file lists run logs that are not in the repository, so its two zmx2 steps were run here as this repository's own sequence.
wand125, square-packing-bounds, building directly on Evan Daniel's cover, format and checkers. Registration was requested in jlevy/squares#279. The source says parts of the work were produced with AI assistance under human direction.
Significance, composition and next rung
- Significance
- An exact value for a case that was open, and a second route to : a substantive case result at S3, set beside T-062, whose cover it extends. The 2 October review of the and covers confirmed the draft: the band insertion that carries a side-8 cover to side 9 is the one new idea, and at one instance it is a case result, not yet a technique.
- Composition
- Compound, and the minimum is set by the lower half. The lower half is E-n077-wand125-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic); the equality is C3, as T-066 reads its own. The checker is Daniel's, which also decides T-062 and T-066. The zm_mixed.py sweep the source reports is not replayed here, and sets nothing.
takes the same certificate directly, its total being below 78, so no step is added. At registration this entry's scope was alone, since T-064 registers (result-import.md, register table); it took in at stage 4, on 2 October 2026, because the verified bound there rested on this replay alone, T-064's own route being unreplayed until its Valid7 replay and Lean build passed here on 2 and 3 October. The verified bound at still cites this replay alone. T-064 keeps its claim, which names this route. - Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. The source's zm_mixed.py sweep, about 94 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method (think-mx3k). V5 would need a Lean statement for this cover and a human expert's review of the formalization.
- Novelty
- previously-published Present in an identified source
The cases
Proven
- optimal
- exact
Citation record n-077
lowerwand125 after Daniel, Levy et al. 2026, GitHub (confirmed T-067)
The case record
Results on these cases
10 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007 ·
for
V0 C1 lower bound incomplete on these cases, superseded by T-064 and T-067
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 published T-085 ·
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-27 published T-045 ·
Rectangle-density lower bounds replayed at 15 counts in
V3 C3 lower bound confirmed superseded by T-064 and T-067
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046 ·
Rectangle-density lower bounds reported for 48 counts in
V0 C0 lower bound recorded superseded by T-064 and T-067
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register
2026-09-29 published T-058 ·
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsV3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083 ·
for every nonsquare
V3 C3 lower bound confirmed on these cases, superseded by T-064 and T-067
Karakuş · Karakuş 2026 · source · register
2026-09-30 published T-064 ·
for every integer from 6 up; are the cases held here
V3 C3 optimality confirmed on these cases, current best, reported
Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-10-01 published T-067 this result ·
, by a mixed cover extended from Daniel's cover
V3 C3 optimality confirmed
wand125 after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register
2026-10-03 published T-081 ·
for every integer from 5 up; are the cases held here
V0 C1 optimality reviewed on these cases, second certificate, reported
Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register
2026-10-07 published T-124 ·
Reported non-strict local minima for 178 source configurations
V0 C0 restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register
Links
- On this site
- Case record, · Frontier row, · Case record, · Frontier row, · T-067 in the results table
On GitHub, at main
- Register
- T-067 in
results.yaml, line 6013 - Evidence
E-n077-wand125-mixed-cover-report·E-n077-wand125-mixed-cover-zmx2-replay·E-basic-grid-upper- Proofs and certificates
- certificate
n77_mixed_cover_9.txt.gz· proofREADME.md· auditreview-2026-10-02-wand125-s59-s77-mixed-covers.md - Sources
- wand125 exact covers 2026-10-01 (its own site, retained copy)
- Source packet
resources/web/wand125-point-and-mixed-2026-10-01/README.md- Artifacts
16 artifacts and controls
frontier/n-077.mdfrontier/n-078.mdresources/web/wand125-point-and-mixed-2026-10-01/README.mdresources/web/wand125-point-and-mixed-2026-10-01/square-packing-bounds/certificates/k2m4_n77_L9/README.mdresources/web/wand125-point-and-mixed-2026-10-01/square-packing-bounds/certificates/k2m4_n77_L9/n77_mixed_cover_9.txt.gzresources/web/wand125-point-and-mixed-2026-10-01/receipts/n77_cover_audit.jsonresources/web/wand125-point-and-mixed-2026-10-01/receipts/n77_zmx2_d4_pairpoints_audit.jsonresources/web/wand125-point-and-mixed-2026-10-01/receipts/n77_zmx2_full_pairpoints_audit.jsondevtools/replay_evand_zmx2.pydevtools/audit_evand_mixed_covers.pydevtools/check_basic_bounds.pydocs/project/reviews/review-2026-10-02-wand125-s59-s77-mixed-covers.mdtests/test_replay_controls.pytests/test_audit_evand_mixed_covers.pyresources/web/wand125-point-and-mixed-2026-10-01/receipts/controls/n77_control_drop-heaviest-point_zmx2_d4_pairpoints_x44-44_y44-44.logresources/web/wand125-point-and-mixed-2026-10-01/receipts/controls/n77_control_drop-heaviest-segment_zmx2_d4_pairpoints_x5-5_y41-41.log- Case file
frontier/n-077.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-078.md(verified lower, verified upper, reported lower, reported upper)