T-191: s(95)=10, by a mixed cover of points and grid-line segments

V3 C1 Optimality reviewed

2026-10-15 published · Greff after Daniel, Hosono · n=95

Greff reports s(95)=10: the lower half by a mixed cover, the upper half by the 10×10 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 s(59)=8 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 s(59)=8 and s(76)=9: 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 s(95) 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

Case record

n=95

9.9610
91011
9.74710.747
nn+1

Proven

9.96500≤s(95)≤10

  • exact

Citation record n-095

lowerHosono after Tokoharu, Levy et al. 2026, GitHub (confirmed T-090)

Open

  • optimality

The case record

LowerUpper
Gap7200= 0.035

Results on the case

14 results in the register on n=95, 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-090

    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ş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

  3. 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-090

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

  4. 2026-09-28 published T-070

    Rectangle-density lower bounds replayed at 25 counts in n=29…95

    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

  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

    Hosono 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-090

    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-090

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

  8. 2026-10-01 published T-074

    Rectangle-density lower bounds replayed at 31 counts in n=19…95

    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

  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-090

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

  10. 2026-10-04 published T-090

    Mixed rectangle-measure lower bounds verified at 17 counts in n=42…96

    V3 C3 Lower bound confirmed

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

  11. 2026-10-04 published T-091

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

    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

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

  13. 2026-10-13 published T-180

    Closed-form lower bound s(N)≥a(N) for every non-square N≥49, reported

    V0 C1 Lower bound reviewed on this case, superseded by T-090

    Hosono · wand125 closed form 2026-10-14 · packet · packet · register

  14. 2026-10-15 published T-191 this result

    s(95)=10, 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