T-191: , 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 = 10 of the k^2 - 5 series, after T-066 (k = 8) and T-184 (k = 9).
The cover is 48,352 weighted points and 11,438 axis-parallel segments of [0,10]^2 in Daniel's mixed format, total 3791753447/40000000 = 94.793836175 < 95, exactly D4-invariant. Every closed unit square in [0,10]^2 captures mass at least one, so a packing of 95 at side below 10, scaled up to side 10, would capture at least 95.
The source reports the covering statement decided by two of Daniel's checkers: zmx2, in outward-rounded binary64, on 9,981 of the 10,000 root cells of the D4 region, and zm_mixed.py, in exact rationals, on the 304 cells that tile the other 19. 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 10,000 roots and zm_mixed.py over the 304 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/s95-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#610. The source's README states: "Greff directed the work. The search, LP and verification pipeline were built and run with Claude (Anthropic) as an AI assistant."
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 and T-184 settled and : a substantive case result, not a new technique or a family. The third instance of the k^2 - 5 series does not make it a family: each cross is re-optimised by LP, and nothing carries to another k. The 16 October review confirmed the draft.
- Composition
- Compound, and the minimum is set by the lower half: E-bengreff-610-cover-replay (interval-certified, zmx2 on 9,981 D4 roots and zm_mixed.py on the 304 sub-roots of the other 19, 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 304 sub-roots, has refused none. 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 304 sub-roots: two mutated certificates refused by it and held by a test. None has run for this cover, so two are owed whatever the answer to owner question 16 (think-l3oo, the review's finding F8) on whether a refusal at a depth limit of 12 counts. 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; none has run. 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
14 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-090
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-046
Rectangle-density lower bounds reported for 48 counts in
V0 C0 Lower bound recorded superseded by T-090
Hosono 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-070
Rectangle-density lower bounds replayed at 25 counts in
V3 C3 Lower bound confirmed superseded by T-090
Hosono 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
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-090
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-090
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-01 published T-074
Rectangle-density lower bounds replayed at 31 counts in
V3 C3 Lower bound confirmed on this case, superseded by T-090
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · 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-090
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · packet · source · review · register
2026-10-04 published T-090
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 2026-10-04 · 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 on this case, superseded by T-090
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-090
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-15 published T-191 this result
, by a mixed cover of points and grid-line segments
V3 C1 Optimality reviewed
Greff after Daniel, Hosono · bengreff s95 certificate 2026-10-15 · packet · source · review · register
Links
- On this site
- Case record, · Frontier row, · T-191 in the results table
On GitHub, at main
- Register
- T-191 in
results.yaml, line 26570 - Evidence
E-bengreff-610-cover-report·E-bengreff-610-cover-replay·E-basic-grid-upper- Proofs and certificates
- certificate
s95_cover_v2.txt.gz· proofREADME.md· auditreview-2026-10-16-greff-k2m5-mixed-covers-76-95.md - Sources
- bengreff s95 certificate 2026-10-15
- Source packet
resources/web/bengreff-s95-certificate-2026-10-15/README.md- Artifacts
13 artifacts and controls
resources/web/bengreff-s95-certificate-2026-10-15/README.mdresources/web/bengreff-s95-certificate-2026-10-15/s95-certificate/cover/s95_cover_v2.txt.gzresources/web/bengreff-s95-certificate-2026-10-15/s95-certificate/README.mdresources/web/bengreff-s95-certificate-2026-10-15/receipts/n95_cover_audit.jsonresources/web/bengreff-s95-certificate-2026-10-15/receipts/n95_zmx2_d4.logdevtools/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-s95-certificate-2026-10-15/receipts/controls/n95_control_drop-heaviest-point_zmx2_d4_x15-15_y15-15.logresources/web/bengreff-s95-certificate-2026-10-15/receipts/controls/n95_control_drop-heaviest-segment_zmx2_d4_x5-5_y45-45.log- Case file
frontier/n-095.md(verified lower, verified upper, reported lower, reported upper)