T-072: Mixed rectangle-measure lower bound replayed at n=76

V3 C3 lower bound confirmed superseded by T-091

2026-10-02 published · wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · n=76

s(76)≥447/50 = 8.94, by a rectangle density of wand125/square-packing-bounds checked at coverage one, published on 2 October 2026.

The certificate is a density of 317 uniform rectangles with no point mass, of total mass 7599999/100000, at core side 9977/10000 on 201 net half-angles of step 83/40000, such that the shrunken core of every rotated unit square at each net direction captures mass at least one. The source reports it accepted at every oblique net angle by code/mixed_rotated_verify.cpp, the research copy of Tokoharu's verify.cpp that its s(50) certificate (T-048) and the certificates of T-069 and T-071 use, which accepts coverage at least 1 where Tokoharu's requires 10001/10000, and at angle zero by exact integer tables. The least oblique lower bound it records is 1.00000000051.

The value exceeds the source's rectangle certificate at this count, 357/40 = 8.925 (T-068), which it says it supersedes, and Nagamochi's 1 + sqrt(61) = 8.8102....

Here the exact premises were recomputed from the retained bytes, and the certificate passed a complete replay on 2 October 2026 of the source's unchanged checker and per-angle functions on the pinned tarball: all 201 directions, each returning the certificate's own record. The replay runs the source's own algorithm and is not an independent decision of coverage.

wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 2 October 2026 on jlevy/squares#282. The source says parts of the work were produced with AI assistance under human direction.

Significance, composition and next rung
Significance
Raised the verified lower bound at n=76 by 0.05, over wand125's n=75 rectangle certificate by monotonicity (T-045), by the certificate kind of T-048, T-069 and T-071: a further size from one generator, a substantive case result at S3. The 2 October review of the certificate confirmed the draft.
Composition
One claim on one certificate. E-n076-wand125-mixed-894-source-replay replays it in full with the source's own checker: one interval-certified method, replayed here, C3. Coverage is decided by the source's C++ checker alone, and the axis tables are a second implementation for one direction and not a second method.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A second machine method would be a method-distinct decision of rotated coverage; the replay here runs the source's own checker. The checker's controls were made on the n=37 certificate of the same kind; a control on this certificate, devtools.audit_wand125_point_and_mixed mixed-control n76, would bind them to this measure as well.
Novelty
previously-published Present in an identified source

The case

Case record

n=76

8.969
8910
8.7189.718
nn+1

Proven

8.96500≤s(76)≤9

  • exact

Citation record n-076

lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-091)

Open

  • optimality

The case record

LowerUpper
Gap7200= 0.035

Results on the case

11 results in the register on n=76, oldest first, each with what it established and how it stands now.

  1. 2005 published T-007

    s(n)≥min(⌈n⌉,n−2⌊n⌋+1+1) for 4≤n≤324

    V0 C1 lower bound incomplete on this case, superseded by T-091

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-09-04 published T-085

    Nagamochi 2005, Lemma 1 is false for every container with a>3 and b>2

    V3 C3 correction confirmed

    Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

  3. 2026-09-27 published T-045

    Rectangle-density lower bounds replayed at 15 counts in n=18…78

    V3 C3 lower bound confirmed superseded by T-091

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register

  4. 2026-09-27 published T-046

    Rectangle-density lower bounds reported for 48 counts in n=18…95

    V0 C0 lower bound recorded superseded by T-091

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register

  5. 2026-09-29 published T-058

    Rectangle-certificate ceiling α·UB(n) proved for n=1..100; B·UB(n) on 64 grid rows

    V3 C3 method limit confirmed

    wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register

  6. 2026-09-29 published T-083

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤324

    V3 C3 lower bound confirmed on this case, superseded by T-091

    Karakuş · Karakuş 2026 · source · register

  7. 2026-10-01 published T-068

    Rectangle-density lower bounds verified at 34 counts in n=19…95

    V3 C3 lower bound confirmed on this case, superseded by T-091

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register

  8. 2026-10-02 published T-072 this result

    Mixed rectangle-measure lower bound replayed at n=76

    V3 C3 lower bound confirmed superseded by T-091

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds n76 2026-10-02 · packet · packet · source · review · register

  9. 2026-10-03 published T-082

    Mixed rectangle-measure lower bounds verified at 22 counts in n=51…96

    V3 C3 lower bound confirmed on this case, superseded by T-091

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · packet · source · review · register

  10. 2026-10-04 published T-091

    Mixed rectangle-measure lower bounds verified at 17 counts in n=53…95

    V3 C3 lower bound confirmed

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds evening 2026-10-04 · packet · source · review · register

  11. 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