T-298: $s (k^{2} - 5) = k$ for every integer k from 7 up; k = 7…18 are the cases held here

V0 C1 Optimality reviewed

2026-11-13 published · Khalili, Gharabaghi after Daniel · 12 cases, $n = 44$ to 319

Mohsen Khalili and Sara Gharabaghi's theorem s(k^2 - 5) = k for every integer k >= 7, published on 13 November 2026: the lower half at k = 7, 8 and 9 by the $s (44)$ , $s (59)$ and $s (76)$ certificates, and at every k >= 10 by one family of periodic measures; the upper half by the k x k grid.

This entry's scope is its projection onto n <= 324, k = 7 to 18: $s (44) = 7$ , $s (59) = 8$ , $s (76) = 9$ , $s (95) = 10$ , $s (116) = 11$ , $s (139) = 12$ , $s (164) = 13$ , $s (191) = 14$ , $s (220) = 15$ , $s (251) = 16$ , $s (284) = 17$ and $s (319) = 18$ . New to this record are k = 11 to 18; k = 7, 8 and 9 are T-252, T-066 and T-184, and $s (95) = 10$ is Greff's T-191, which this family reaches by a second, reported route.

For k >= 10 the measure on [0,k]^2 is a corner module in each corner, a wall pattern of depth 4 and period one on the lines of the 1/10 grid, and Lebesgue measure on [19/5, k - 19/5]^2, of total k^2 - 4D with D = 1340566927759/1000000000000, so 4D exceeds 5. The source reduces every k >= 10 to one finite statement on the 11 x 11 board, Valid11, and its Lean development, the source reports, kernel-checks that reduction; it does not prove Valid11.

Valid11 is decided at the source by Daniel's interval checker zmx2 at theta = 0 and on 12,024 of the 12,100 D4 roots, by zmx2 with his exact-rational qx2_zm.py on root 9632, and on the 75 roots where zmx2 stalls at wall tiles of mass exactly one by the authors' Tight-Tile Lemma, a blow-up argument in the tilt checked by exact rationals and outward-rounded intervals. The source reports one adversarial AI review of that lemma and none by outside mathematicians.

Here the source's fast checks, zmx2 on cert0 and 30 of the 55 columns, root 9632 with both checkers and 26 tight-tile jobs ran on the retained bytes, each equal to the source's records, and the source's controls refused as reported, though the Tight-Tile control's cell counts, run to a 2,000-cell cap, do not match the paper's (the review's F8); in all about 2.5 CPU-hours: a diagnostic, not a replay. The full replay and the Lean build are priced and held, so the verified lower bounds are unchanged. The blind stage 4 review of 14 November accepts the argument as written with no blocking defect; it finds that zmx2's area-density and first-order lemmas, on which most roots rest, have no review in this record, and that the Tight-Tile Lemma has one implementation and no full replay.

Mohsen Khalili and Sara Gharabaghi, k2m5-family, with the paper archived as Zenodo 10.5281/zenodo.24237740 and release 1.1, whose certificate is the same, as Zenodo 10.5281/zenodo.24237941, building on Daniel's families for k^2 - 3 and k^2 - 4, his linear program, format, checkers and Lean reduction, at the request of jlevy/squares#973. The paper says the search, the certificate, the Tight-Tile checker and its proof, and the verification runs were produced with Claude (Anthropic) under the authors' direction.

Significance, composition and next rung

Significance: Scored as a claim: a bound family, the deficit-5 case of Friedman's conjecture, which would settle eight open cases of this record, k = 11 to 18, and every later k if the finite premise and its reduction pass replay and review here, with a new argument, the Tight-Tile Lemma, for wall tiles where box subdivision stalls. S4 by the anchor "a reusable technique, bound family", as T-064 and T-081 are; not S5, since no case it settles is central to this project. The score gates nothing. The stage 4 review (L144) states no score in its text, and its hand-off proposed S4 (think-h10k), so this stays the import lane's draft until a review confirms it.
Composition: Compound, and the minimum is set by the lower half at k >= 10. The upper half is the k x k grid, E-basic-grid-upper. At k = 7, 8 and 9 the lower half is the certificates this record holds as T-252, T-066 and T-184, and this entry adds no evidence to them.

At k >= 10 it is two parts in series: the finite premise Valid11, reported by the source's runs (E-khalili-973-valid11-report), and the reduction from it to every k >= 10, the source's Lean (E-khalili-973-lean-report), not built here. Both are reports, so the entry is V0. The stage 4 review of 14 November reads the claim chain and is recorded as the reports' external_review with no blocking defect, so it is C1, as T-081 is.

Its own exact programs, independently re-implemented after reading the producer's code and not clean-room, decide in full the mass, the theta = 0 face, the coverage of the tight-tile roots and root 9632's closure (E-khalili-973-review-partial-checks), not the general-position roots or the Tight-Tile cells, so no rung beyond C1 follows. Both lanes' runs of the source's own programs on samples (E-khalili-973-replay-sample, E-khalili-973-review-replay-sample) decide the runs they repeated and set no rung.

The scope lists the cases this record holds; the theorem's own domain is every k >= 7, and a scope that can say so is think-kqi1.
Next rung: Valid11 replayed in full and the Lean reduction built (think-0h7r): the zmx2 sweep's remaining columns, the 75 coverage dumps, which the source's verify.sh --full does not regenerate, and the 323 tight-tile jobs with the coverage check, about 145 to 180 CPU-hours by both lanes' samples, up to about 320 if the unsampled large tight-tile jobs run no faster than at the source; and the build of lean/K2m5, a few CPU-hours on a host with at least 24 GB of memory or swap and about 10 GB of disk. Then replayed entries for Valid11 and the reduction, and the verified lower bounds at k = 11 to 18.

The stage 4 review's two major findings stand beside that: zmx2's area-density and first-order lemmas, on which the 12,024 general-position roots rest, have no review in this record (F1, a review held in think-kn13), and the Tight-Tile Lemma has one implementation and no full replay (F2): think-0h7r's replay reruns that implementation and closes only the second half, and no bead tracks a second implementation. V4 and C4 need a second adversarial review and a human oversight record.
Unfinished confirmations: C3 (think-0h7r): Valid11 replayed in full with the source's programs and the Lean reduction built from the retained bytes, each with its controls, as replayed entries: the zmx2 sweep (cert0 and 55 columns), the 75 coverage dumps, the 308 + 15 tight-tile jobs and 3 reruns with cov_check.py on the regenerated dumps, root 9632, and lean/K2m5 with #print axioms. About 145 CPU-hours, up to about 320 (priced 2026-11-14).

C3 (think-kn13): a review of zmx2's area-density Lemmas 1 to 3, K and K(d) and its first-order Lemmas U and V against zmx2.rs at e2bb84e9, the stage 4 review's F1, on which the 12,024 general-position roots rest. It is not a condition of C3, which the replay above reaches with this review already mapped; it is recorded at that rung as the trust point it would close beside it. About 1 CPU-hours (priced 2026-11-14).
Novelty: previously-published Present in an identified source

The cases

This result concerns 12 cases, too many to draw one by one. Each is listed with the film’s bounds, the proved lower bound and the best known side, and links to its case record, where its packing and number line are drawn.

n	Proved lower	Best known	Gap	Status	Records
44	7	7	0	provedO=	frontier n-044.md
59	8	8			frontier n-059.md
76	9	9			frontier n-076.md
95	10	10			frontier n-095.md
116	10.807764	11	0.19223593…	open=	frontier n-116.md
139	11.824751	12	0.17524834…		frontier n-139.md
164	12.838962	13	0.16103732…		frontier n-164.md
191	13.851029	14	0.14897007…		frontier n-191.md
220	14.861406	15	0.13859338…		frontier n-220.md
251	15.870426	16	0.12957385…		frontier n-251.md
284	16.878339	17	0.12166064…		frontier n-284.md
319	17.885338	18	0.11466134…		frontier n-319.md

Results on these cases

23 results in the register on these cases, oldest first

2005 published T-007 · 12 of these cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
Lower bound incomplete on these cases, superseded by T-066, T-083, T-184, T-191, T-252 and T-298 (reported)
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 published T-085 · 12 of these cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
Correction confirmed
Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-27 published T-045 · case 76
Rectangle-density lower bounds replayed at 15 counts in $n = 18 \dots 78$
Lower bound confirmed superseded by T-184
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046 · cases 44, 59, 76, 95
Rectangle-density lower bounds verified at 48 counts in $n = 18 \dots 95$
Lower bound confirmed superseded by T-066, T-184, T-191 and T-252
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register
2026-09-28 published T-070 · cases 44, 59, 95
Rectangle-density lower bounds replayed at 25 counts in $n = 29 \dots 95$
Lower bound confirmed superseded by T-066, T-191 and T-252
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 · cases 44, 59, 76, 95
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
Method limit confirmed
Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083 · 12 of these cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
Lower bound confirmed
Karakuş · Karakuş 2026 · source · register
2026-10-01 published T-066 · case 59
$s (59) = 8$ , by a mixed cover of points and grid-line segments
Optimality confirmed
Hosono after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register
2026-10-01 published T-068 · cases 44, 76, 95
Rectangle-density lower bounds verified at 34 counts in $n = 19 \dots 95$
Lower bound confirmed on these cases, superseded by T-184, T-191 and T-252
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-01 published T-074 · cases 44, 95
Rectangle-density lower bounds replayed at 31 counts in $n = 19 \dots 95$
Lower bound confirmed on these cases, superseded by T-191 and T-252
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · packet · source · review · register
2026-10-02 published T-072 · case 76
Mixed rectangle-measure lower bound replayed at $n = 76$
Lower bound confirmed superseded by T-184
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 · cases 76, 95
Mixed rectangle-measure lower bounds verified at 22 counts in $n = 51 \dots 96$
Lower bound confirmed on these cases, superseded by T-184 and T-191
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 · cases 44, 95
Mixed rectangle-measure lower bounds verified at 17 counts in $n = 42 \dots 96$
Lower bound confirmed on these cases, superseded by T-191 and T-252
Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-04 · packet · source · review · register
2026-10-04 published T-091 · cases 76, 95
Mixed rectangle-measure lower bounds verified at 17 counts in $n = 53 \dots 95$
Lower bound confirmed on these cases, superseded by T-184 and T-191
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 · 12 of these cases
Reported non-strict local minima for 178 source configurations
Restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register
2026-10-11 published T-235 · case 59
Hosono reports a Lean kernel proof that $s (59) = 8$ , on Daniel's mixed-measure checker
Formalization recorded
Hosono after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 n59 Lean kernel 2026-10-11 · packet · source · register
2026-10-12 published T-261 · 12 of these cases
Reported grade-C local minima for 233 source configurations of field degree at most 4
Restricted optimality incomplete
Daniel after Schadt, Ellsworth, Levy · Daniel exact and local reports 2026-10-12 · packet · packet · register
2026-10-13 published T-177 · case 44
Mixed rectangle-measure lower bound $s (44) \geq 2799 / 400$ reported, on a 2,073-direction declared net
Lower bound reviewed superseded by T-252
Hosono after Tokoharu and Levy · wand125 fine-net n37 n39 n44 2026-10-13 · packet · register
2026-10-13 published T-180 · 11 of these cases
Closed-form lower bound $s (N) \geq a (N)$ for every non-square $N \geq 49$ , reported
Lower bound reviewed on these cases, superseded by T-066, T-083, T-184, T-191 and T-298 (reported)
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-14 published T-184 · case 76
$s (76) = 9$ , by a mixed cover of points and grid-line segments
Optimality confirmed
Greff after Daniel, Hosono · bengreff s76 certificate 2026-10-14 · packet · source · review · register
2026-10-15 published T-191 · case 95
$s (95) = 10$ , by a mixed cover of points and grid-line segments
Optimality confirmed
Greff after Daniel, Hosono · bengreff s95 certificate 2026-10-15 · packet · source · review · register
2026-10-26 published T-252 · case 44
$s (44) = 7$ , by a closed mixed cover of points and grid-line segments
Optimality confirmed
Khalili, Gharabaghi after Daniel · Khalili Gharabaghi s44 cover 2026-10-29 · packet · source · review · register
2026-11-13 published T-298 this result · 12 of these cases
$s (k^{2} - 5) = k$ for every integer k from 7 up; k = 7…18 are the cases held here
Optimality reviewed
Khalili, Gharabaghi after Daniel · Khalili Gharabaghi k2m5 family 2026-11-13 · packet · packet · packet · register

Links

On this site: Frontier Survey · T-298 in the results table
Issues: Issue #973

On GitHub, at main

Register: T-298 in results.yaml, line 46152
Evidence: E-khalili-973-k2m5-family-report · E-khalili-973-valid11-report · E-khalili-973-lean-report · E-khalili-973-review-partial-checks · E-khalili-973-replay-sample · E-khalili-973-review-replay-sample · E-basic-grid-upper
Proofs and certificates: certificate sol_exact_box11.txt.gz · certificate Inst.lean
Sources: Khalili Gharabaghi k2m5 family 2026-11-13 (its own site, retained copy)
Source packet: resources/web/moh63-dev-k2m5-family-2026-11-13/README.md · resources/web/evand-square-packing-2026-10-24/README.md · resources/web/khalili-gharabaghi-k2m5-973-review-2026-11-14/README.md
Artifacts: 12 artifacts and controls
resources/web/moh63-dev-k2m5-family-2026-11-13/README.md resources/web/moh63-dev-k2m5-family-2026-11-13/k2m5-family/README.md resources/web/moh63-dev-k2m5-family-2026-11-13/k2m5-family/certificate/sol_exact_box11.txt.gz resources/web/moh63-dev-k2m5-family-2026-11-13/k2m5-family/paper/k2m5.pdf resources/web/moh63-dev-k2m5-family-2026-11-13/k2m5-family/lean/K2m5/Inst.lean resources/web/moh63-dev-k2m5-family-2026-11-13/receipts/verify_fast.log resources/web/moh63-dev-k2m5-family-2026-11-13/receipts/compare.json.gz resources/web/evand-square-packing-2026-10-24/README.md resources/web/khalili-gharabaghi-k2m5-973-review-2026-11-14/README.md docs/project/reviews/review-2026-11-14-khalili-gharabaghi-k2m5-973.md devtools/replay_k2m5_family.py tests/test_replay_k2m5_family.py
Case file: each case’s file is linked from its row above

T-298: s(k2−5)=ks(k2−5)=k for every integer k from 7 up; k = 7…18 are the cases held here

The cases

Results on these cases

Links

T-298: $s (k^{2} - 5) = k$ for every integer k from 7 up; k = 7…18 are the cases held here