T-184: , by a mixed cover of points and grid-line segments
V3 C1 Optimality reviewed
Greff reports : the lower half by a mixed cover, the upper half by the grid. It is the case k = 9 of the k^2 - 5 series.
The cover is 41,633 weighted points and 9,744 axis-parallel segments of [0,9]^2 in Daniel's mixed format, total 3788361049/50000000 = 75.76722098 < 76, exactly D4-invariant. Every closed unit square in [0,9]^2 captures mass at least one, so a packing of 76 at side below 9, scaled up to side 9, would capture at least 76.
The source reports the covering statement decided by two of Daniel's checkers: zmx2, in outward-rounded binary64, on 8,096 of the 8,100 root cells of the D4 region, and zm_mixed.py, in exact rationals, on the 64 cells that tile the other four. Its Lean wrapper on Daniel's Sqpack takes the covering statement as a hypothesis. Those statements are the author's.
At retention here the cover's data facts were recomputed, zmx2 was replayed over all 8,100 roots and zm_mixed.py over the 64 sub-roots from the bytes the source pins, each equal to the source's records, with two mutations refused by zmx2. The two checkers' runs are read as one decision over the D4 region, every cell certified once: a reproduction with the producer's code, counted as a confirmation once zm_mixed.py's mutated-certificate controls are held. The review of 16 October found no mathematical defect.
Credit Greff (https://github.com/bengreff/s76-certificate), building on Daniel's method at margin zero, mixed format, checkers and Lean library, and on Hosono's cover, reused for the corners, and band-insertion construction. Registration was requested in jlevy/squares#594. The source says the search, LP and verification pipeline were built and run with Claude (Anthropic) as an AI assistant, under the author's direction.
Significance, composition and next rung
- Significance
- An exact value for a case that was open, by Daniel's recipe at a new count, as T-066 settled : a substantive case result, not a new technique or a family. The 16 October review confirmed the draft.
- Composition
- Compound, and the minimum is set by the lower half: E-bengreff-594-cover-replay (interval-certified, zmx2 on 8,096 D4 roots and zm_mixed.py on the 64 sub-roots of the other 4, replayed here and read as one decision), the upper half the grid (E-basic-grid-upper, exact-algebraic). Both deciding programs are Daniel's and each cell rests on one of them.
The cited replay derives C3; the record declares C1, because stage 4 counts a replay as a confirmation only when two mutated certificates are refused by every checker that accepted the original and a test holds them (result-import.md, stage 4), and zm_mixed.py, which decides the 64 sub-roots, has refused one, the review's depth-12 pair, whose standing is owner question 16 (think-l3oo). The rung for a replay without a machine certificate does not fit a machine replay that is complete but for its controls. C1 is the review's read of the reported entry. V3 stands, since the certificate replays, which is what V3 asks of evidence of any origin. - Next rung
- C3 waits on stage 4's control rule for zm_mixed.py, which decides the 64 sub-roots: two mutated certificates refused by it and held by a test. The review's depth-12 pair is one if a refusal at a depth limit of 12 counts, which is owner question 16 (think-l3oo, the review's finding F8); a second is owed either way, and refusals at the source's limit of 24 did not finish. The rule is met for zmx2. V4 and C4 then need a second adversarial AI review by a distinct reviewer and a human oversight record; one adversarial review is retained. An unreduced zmx2 --full sweep (about 6 CPU-hours with its follow-up, think-eucc) would take the D4 reduction off the zmx2 part.
- Unfinished confirmations
- C3 (think-l3oo): zm_mixed.py's refusals of two mutated covers, held by a test, at a depth limit the owner accepts: the review's depth-12 pair and one more, or two at the accepted limit. Not priced.
C4: a second adversarial AI review of the cover and the composite, by a reviewer distinct from the 16 October one. Not priced.
C4: a human oversight record that checks the trust boundary, the certificate's meaning and the AI review's findings. Not priced. - Novelty
- previously-published Present in an identified source
The case
Results on the case
13 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-091
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 Correction confirmed
Karakuş; Vlasenko · 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-091
Hosono 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-091
Hosono 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
Hosono 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-091
Karakuş · Karakuş 2026 · source · register
2026-10-01 published T-068
Rectangle-density lower bounds verified at 34 counts in
V3 C3 Lower bound confirmed on this case, superseded by T-091
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-02 published T-072
Mixed rectangle-measure lower bound replayed at
V3 C3 Lower bound confirmed superseded by T-091
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds n76 2026-10-02 · packet · packet · source · review · register
2026-10-03 published T-082
Mixed rectangle-measure lower bounds verified at 22 counts in
V3 C3 Lower bound confirmed on this case, superseded by T-091
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · packet · source · review · register
2026-10-04 published T-091
Mixed rectangle-measure lower bounds verified at 17 counts in
V3 C3 Lower bound confirmed
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds evening 2026-10-04 · 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
2026-10-13 published T-180
Closed-form lower bound for every non-square , reported
V0 C1 Lower bound reviewed on this case, superseded by T-091
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-14 published T-184 this result
, by a mixed cover of points and grid-line segments
V3 C1 Optimality reviewed
Greff after Daniel, Hosono · bengreff s76 certificate 2026-10-14 · packet · source · review · register
Links
- On this site
- Case record, · Frontier row, · T-184 in the results table
On GitHub, at main
- Register
- T-184 in
results.yaml, line 25099 - Evidence
E-bengreff-594-cover-report·E-bengreff-594-cover-replay·E-basic-grid-upper- Proofs and certificates
- certificate
s76_cover_v5.txt.gz· proofREADME.md· auditreview-2026-10-16-greff-k2m5-mixed-covers-76-95.md - Sources
- bengreff s76 certificate 2026-10-14
- Source packet
resources/web/bengreff-s76-certificate-2026-10-14/README.md- Artifacts
16 artifacts and controls
resources/web/bengreff-s76-certificate-2026-10-14/README.mdresources/web/bengreff-s76-certificate-2026-10-14/s76-certificate/cover/s76_cover_v5.txt.gzresources/web/bengreff-s76-certificate-2026-10-14/s76-certificate/README.mdresources/web/bengreff-s76-certificate-2026-10-14/receipts/n76_cover_audit.jsonresources/web/bengreff-s76-certificate-2026-10-14/receipts/n76_zmx2_d4.logresources/web/bengreff-s76-certificate-2026-10-14/receipts/n76_triage_checks.logresources/web/bengreff-s76-certificate-2026-10-14/review/README.mddevtools/replay_evand_zmx2.pydevtools/audit_evand_mixed_covers.pydevtools/check_basic_bounds.pydocs/project/reviews/review-2026-10-16-greff-k2m5-mixed-covers-76-95.mdtests/test_replay_controls.pytests/test_audit_evand_mixed_covers.pyresources/web/bengreff-s76-certificate-2026-10-14/receipts/controls/n76_control_drop-heaviest-point_zmx2_d4_x15-15_y15-15.logresources/web/bengreff-s76-certificate-2026-10-14/receipts/controls/n76_control_drop-heaviest-segment_zmx2_d4_x5-5_y35-35.logresources/web/bengreff-s76-certificate-2026-10-14/review/outputs/zm_control/n76_scaled-199-200_j054_depth12.log- Case file
frontier/n-076.md(verified lower, verified upper, reported lower, reported upper)