T-062: , by a mixed cover of points and grid-line segments
V3 C3 optimality confirmed
: the lower half by Evan Daniel's mixed cover of 28 September 2026, the upper half by the grid.
The cover is 23,744 weighted points of [0,8]^2 plus mass spread uniformly along 5,216 segments of length 1/50 on the interior grid lines, total 748233441/12500000 = 59.85867528 < 60, exactly D4-invariant. Every closed unit square in [0,8]^2 captures mass at least one, a boundary point and a segment along an edge counting in full, so a packing of 60 at side s below 8, its centres scaled by 8/s, would give 60 pairwise disjoint closed unit squares in [0,8]^2 capturing at least 60.
The source certifies that at margin zero with two separately written checkers: zm_mixed.py in exact rational arithmetic over 102,400 root boxes, and the Rust zmx2 with outward-rounded binary64 enclosures over 6,400 symmetry-reduced roots and 51,200 unreduced ones, none uncertified. It has no Lean theorem for this cover.
zmx2 was replayed here in full on 2 October 2026, over all 6,400 D4 roots and all 51,200 unreduced roots, every root's census equal to the source's; zm_mixed.py was not run. wand125's (T-066), replayed here the same day with the same checker, gives this value a second route by monotonicity.
Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method. Registration was requested in jlevy/squares#256. The source's CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.
Significance, composition and next rung
- Significance
- An exact value for a case that was open, by the line-cover recipe of T-052 and T-053 carried to side 8, adding no technique: a substantive case result, S3. The 2 October review of the geometric premises confirmed the draft, and noted that the family argument that lifted T-053 to S4 applies here exactly as there, so the two should carry one score; which one is the rescoring pass's (think-qh3s).
- Composition
- Compound, and the minimum is set by the lower half. The lower half is E-n060-evand-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic). As for T-052 and T-053, the two machine entries certify different halves; the lower half stands on one replayed method, and the equality is C3. The second route, T-066's cover, was made from this cover and decided by the same zmx2, so it adds a certificate and not a method.
- Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review, of the geometric premises, is retained. A complete zm_mixed.py sweep, about 20 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method (think-mx3k); the shared author, agent and pose-space architecture stay the residual common-mode risk. V5 would need a Lean data file and top theorem for this cover, which the source has not attempted, and a human expert's review of the formalization.
- Novelty
- previously-published Present in an identified source
The case
Results on the case
9 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 this case, superseded by T-062
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-046
Rectangle-density lower bounds reported for 48 counts in
V0 C0 lower bound recorded superseded by T-062
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register
2026-09-28 published T-062 this result
, by a mixed cover of points and grid-line segments
V3 C3 optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · source · review · register
2026-09-28 published T-070
Rectangle-density lower bounds replayed at 25 counts in
V3 C3 lower bound confirmed superseded by T-062
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · 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 this case, superseded by T-062
Karakuş · Karakuş 2026 · source · register
2026-10-03 published T-081
for every integer from 5 up; are the cases held here
V0 C1 optimality reviewed on this case, 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, · T-062 in the results table
On GitHub, at main
- Register
- T-062 in
results.yaml, line 5444 - Evidence
E-n060-evand-mixed-cover-report·E-n060-evand-mixed-cover-zmx2-replay·E-basic-grid-upper- Proofs and certificates
- certificate
s60_mixed_cover_8.txt.gz· proofREADME.md· auditreview-2026-10-02-evand-s60-geometric-premises.md - Sources
- evand square-packing 2026-10-01 (its own site, retained copy)
- Source packet
resources/web/evand-square-packing-2026-10-01/README.md- Artifacts
17 artifacts and controls
frontier/n-060.mdresources/web/evand-square-packing-2026-10-01/README.mdresources/web/evand-square-packing-2026-10-01/source/s12/certificates/s60/README.mdresources/web/evand-square-packing-2026-10-01/source/s12/certificates/s60/s60_mixed_cover_8.txt.gzresources/web/evand-square-packing-2026-10-01/receipts/s60_cover_audit.jsonresources/web/evand-square-packing-2026-10-01/receipts/s60_zmx2_d4_compare.jsonresources/web/evand-square-packing-2026-10-01/receipts/s60_zmx2_full_compare.jsondevtools/replay_evand_zmx2.pydevtools/audit_evand_mixed_covers.pydevtools/check_basic_bounds.pydocs/project/reviews/review-2026-10-01-evand-source-coverage.mddocs/project/reviews/review-2026-10-01-evand-mathematical-transfer.mddocs/project/reviews/review-2026-10-02-evand-s60-geometric-premises.mdtests/test_replay_controls.pytests/test_audit_evand_mixed_covers.pyresources/web/evand-square-packing-2026-10-01/receipts/controls/s60_control_drop-heaviest-point_zmx2_d4_x16-16_y17-17.logresources/web/evand-square-packing-2026-10-01/receipts/controls/s60_control_drop-heaviest-segment_zmx2_d4_x5-5_y38-38.log- Case file
frontier/n-060.md(verified lower, verified upper, reported lower, reported upper)