T-081: $s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here

V0 C1 optimality reviewed

2026-10-03 published · Daniel after Burns, Massaccesi · 14 cases, $n = 21$ to 320

Evan Daniel's theorem s(k^2 - 4) = k for every integer k >= 5, published in his repository on 3 October 2026: the lower half at k = 5, 6 and 7 by his $s (21)$ , $s (32)$ and $s (45)$ certificates, and at every k >= 8 by one family of periodic measures; the upper half by the k x k grid.

This entry's scope is the projection of that theorem onto the cases this record holds, n <= 324, which is k = 5 to 18: $s (21) = 5$ , $s (32) = 6$ , $s (45) = 7$ , $s (60) = 8$ , $s (77) = 9$ , $s (96) = 10$ , $s (117) = 11$ , $s (140) = 12$ , $s (165) = 13$ , $s (192) = 14$ , $s (221) = 15$ , $s (252) = 16$ , $s (285) = 17$ and $s (320) = 18$ . The reported theorem does not end at k = 18. New to this record are k = 10 to 18; $s (21)$ , $s (32)$ and $s (45)$ are T-052, T-051 and T-053, with T-054 a second route at k = 7, $s (60) = 8$ is T-062, and wand125 published $s (77) = 9$ first, on 1 October (T-067).

For each k >= 8 the measure on [0,k]^2 is a corner module on [0,3]^2 in each corner, a profile of period one in a band of width 3 along each wall, and Lebesgue measure on [14/5, k - 14/5]^2, of total mass k^2 - 4D with D = 214770225571/200000000000, so that 4D exceeds 4. The source states that every closed unit square in [0,k]^2 has mass at least one, and reduces that, for every k >= 8, to one finite statement on the 9 x 9 box, Valid9.

Its Lean development kernel-checks, the source reports, that the tilted part, ValidTilt9, implies the theorem for every k >= 8, with the D4 reduction and the axis-parallel face proved; it does not prove ValidTilt9. ValidTilt9 is the claim of the source's exact-rational checker qx2_zm.py, the program that decided T-064's Valid7, which the source reports accepting all 16,200 root boxes in 115,268 leaves. The source reports three adversarial reviews of the certificate by AI agents and none by outside mathematicians.

A second, separately written exact checker reports ValidTilt9 too: wand125's, the checker whose Valid7 run was replayed here for T-064, in valid7-independent-check on 6 October 2026, over centres [0, 9/2]^2 and u in [0, 7/16] with no symmetry used, in 28,350 roots and 9,537,343 leaves, none uncertified. Its read log says qx2_zm.py was not read; both checkers were written with Claude models, by their sources' own statements.

Here the bundle's fast verify.sh passed on the retained bytes; it recomputes no tilted leaf. wand125's verify_tilt9.sh and an audit of its records passed here, 30 of its roots were certified again here, 21 of them with their published leaves, and two lighter covers were refused; that re-decides about 3% of its recorded cost. The reduction was built here from the retained bytes on 3 October, with only the three standard axioms. Nothing here has yet replayed either run of ValidTilt9 in full, and the verified lower bounds are unchanged.

Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method, at the request of jlevy/squares#316. The source's CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.

Significance, composition and next rung

Significance: Scored as a claim: a bound family, the deficit-4 case of Friedman's conjecture, which would settle nine open cases of this record, k = 10 to 18, and every later k if the finite premise and its reduction pass replay and review here. S4 by the anchor "a reusable technique, bound family", as T-064 is; not S5, since no case it settles is central to this project. The score gates nothing.
Composition: Compound, and the minimum is set by the lower half at k >= 8. The upper half is the k x k grid, E-basic-grid-upper. At k = 5, 6 and 7 the lower half is the source's earlier certificates, which this record holds as T-052, T-051 and T-053 (with T-054 beside it at k = 7), and this entry adds no evidence to them.

At k >= 8 it is two parts in series: the finite premise ValidTilt9, reported by the source's run (E-k2m4-evand-validtilt9-qx2-report) and by wand125's independent run (E-k2m4-wand125-validtilt9-report), and the reduction from it to every k >= 8, the source's Lean (E-k2m4-evand-lean-report), built here with its axiom receipt (E-k2m4-evand-bentz4-lean-build). The reduction is replayed and the finite premise is not: both runs of ValidTilt9 are reports, so the premise sets the minimum, the entry is V0, and the claim-chain review of 3 October reads it, C1.

The scope lists the cases this record holds; the theorem's own domain is every k >= 5, and a scope that can say so is think-kqi1.
Next rung: ValidTilt9 replayed in full by either checker: qx2_zm.py on the box-9 cover, about 226 CPU-hours at the source, in the shards the evand packet's replay plan gives, compared root for root with the published record (think-4uir); or wand125's run, the independent route, priced here from a sample at about 435 CPU-hours as published, or about 118 under its last options (think-hwpr). The Lean reduction is replayed already (E-k2m4-evand-bentz4-lean-build), and the claim chain is reviewed. Then a replayed entry for ValidTilt9, and the verified lower bounds at k = 10 to 18.

A replay of wand125's run lifts the ValidTilt9 part only, and with Daniel's own Lean beside it the result's code relation stays that of the producer's reduction.

The clean-room verifier's Milestone C (docs/project/specs/active/plan-2026-10-03-measure-verifier-milestone-c.md) remains a first-party route; it plans points and segments only, and box 9 also needs a uniform-polygon primitive and an exact argument inside the Lebesgue block, where every square has mass exactly one.
Unfinished confirmations: C3 (think-hwpr): ValidTilt9 replayed in full by either checker, with the route's controls, as a replayed entry beside the Lean reduction's build: wand125's run, the independent route, or qx2_zm.py on the box-9 cover in the shards of the evand packet's replay plan, compared root for root with the published record. About 118 CPU-hours, up to about 435 (priced 2026-10-06).
Novelty: previously-published Present in an identified source

The cases

This result concerns 14 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
21	5	5	0	provedO=	frontier n-021.md
32	6	6			frontier n-032.md
45	7	7			frontier n-045.md
60	8	8			frontier n-060.md
77	9	9			frontier n-077.md
96	9.970000	10	0.03	open=	frontier n-096.md
117	10.856157	11	0.14384241…		frontier n-117.md
140	11.868817	12	0.13118299…		frontier n-140.md
165	12.879418	13	0.12058159…		frontier n-165.md
192	13.888427	14	0.11157216…		frontier n-192.md
221	14.896180	15	0.10381995…		frontier n-221.md
252	15.902921	16	0.09707819…		frontier n-252.md
285	16.908839	17	0.09116091…		frontier n-285.md
320	17.914074	18	0.08592523…		frontier n-320.md

Results on these cases

23 results in the register on these cases, oldest first

2005 published T-007 · 14 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-051, T-052, T-053, T-062, T-067, T-081 (reported), T-082 and T-083
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 established T-020 · case 21
$s (n) \geq 24 / 5 = 4.80$ for $n = 19, 20, 21$
lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-04 published T-085 · 14 of these cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-05 established T-021 · case 21
$s (n) \geq 97 / 20 = 4.85$ for $n = 20, 21$
lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 established T-034 · case 21
$s (21) \geq 122 / 25 = 4.88$
lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 published T-050 · case 21
$s (21) \geq 5000 / 1001 = 4.995004995 \dots$
lower bound confirmed superseded by T-052
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · source · review · register
2026-09-26 published T-051 · case 32
$s (32) = 6$
optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · review 3 · register
2026-09-27 published T-045 · cases 32, 77
Rectangle-density lower bounds replayed at 15 counts in $n = 18 \dots 78$
lower bound confirmed superseded by T-051 and T-067
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046 · cases 60, 77
Rectangle-density lower bounds reported for 48 counts in $n = 18 \dots 95$
lower bound recorded superseded by T-062 and T-067
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register
2026-09-27 published T-052 · case 21
$s (21) = 5$ , by a mixed cover of points and grid-line segments
optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-09-28 · packet · source · review · register
2026-09-27 published T-053 · case 45
$s (45) = 7$ , by a mixed cover of points and grid-line segments
optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-09-28 · packet · source · review · register
2026-09-28 published T-054 · case 45
$s (45) = 7$ by a second, point-only route
simplification confirmed
wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point and mixed bounds 2026-09-28 · packet · source · review · register
2026-09-28 published T-055 · case 21
$s (21) = 5$ by a point-only route
simplification confirmed
wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point and mixed bounds 2026-09-28 · packet · source · review · register
2026-09-28 published T-062 · case 60
$s (60) = 8$ , by a mixed cover of points and grid-line segments
optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · source · review · register
2026-09-28 published T-070 · case 60
Rectangle-density lower bounds replayed at 25 counts in $n = 29 \dots 95$
lower bound confirmed superseded by T-062
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register
2026-09-29 published T-058 · 6 of these cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083 · 14 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-067 · case 77
$s (77) = 9$ , by a mixed cover extended from Daniel's $s (60)$ cover
optimality confirmed
wand125 after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register
2026-10-02 published T-075 · case 96
Mixed rectangle-measure lower bounds replayed at nine counts in $n = 83 \dots 96$
lower bound confirmed on these cases, superseded by T-081 (reported) and T-082
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds afternoon 2026-10-02 · packet · source 1 · source 2 · review · register
2026-10-03 published T-081 this result · 14 of these cases
$s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here
optimality reviewed
Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register
2026-10-03 published T-082 · case 96
Mixed rectangle-measure lower bounds verified at 22 counts in $n = 51 \dots 96$
lower bound confirmed
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · packet · source · review · register
2026-10-04 published T-090 · case 96
Mixed rectangle-measure lower bounds verified at 17 counts in $n = 42 \dots 96$
lower bound confirmed on these cases, superseded by T-081 (reported) and T-082
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-04 · packet · source · review · register
2026-10-07 published T-124 · 14 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

Links

On this site: The frontier survey · T-081 in the results table

On GitHub, at main

Register: T-081 in results.yaml, line 7697
Evidence: E-k2m4-evand-family-report · E-k2m4-evand-validtilt9-qx2-report · E-k2m4-wand125-validtilt9-report · E-k2m4-evand-lean-report · E-k2m4-evand-bentz4-lean-build · E-basic-grid-upper
Proofs and certificates: certificate K4_k008_box9.txt.gz · certificate run_k4x_k008_leaves.jsonl.gz · certificate ValidSplit9.lean · proof ValidSplit9.lean · audit review-2026-10-03-evand-k2m4-claim-chain.md
Sources: evand square-packing 2026-10-03 (its own site, retained copy) · wand125 valid7 independent check 2026-10-06
Source packet: resources/web/evand-square-packing-2026-10-03/README.md · resources/web/wand125-valid7-independent-check-2026-10-06/README.md
Artifacts: 12 artifacts and controls
resources/web/evand-square-packing-2026-10-03/README.md resources/web/evand-square-packing-2026-10-03/square-packing/s12/certificates/k2m4/README.md resources/web/evand-square-packing-2026-10-03/square-packing/s12/lean/Sqpack/ValidSplit9.lean resources/web/evand-square-packing-2026-10-03/receipts/k2m4_verify_fast.log resources/web/evand-square-packing-2026-10-03/receipts/valid9/qx2_replay_plan.json devtools/plan_valid9_replay.py resources/web/evand-square-packing-2026-10-03/receipts/lean/build_bentz4.log resources/web/evand-square-packing-2026-10-03/receipts/lean/axioms_bentz4.log resources/web/wand125-valid7-independent-check-2026-10-06/README.md resources/web/wand125-valid7-independent-check-2026-10-06/receipts/validtilt9_records_audit.json resources/web/wand125-valid7-independent-check-2026-10-06/receipts/validtilt9_sample_compare.json devtools/audit_validtilt9_independent.py
Case file: each case’s file is linked from its row above

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

The cases

Results on these cases

Links

T-081: $s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here