T-163: s(n² − n + 1) < n for every n ≥ 15, and n² − n + F(n) squares below side n, from Kevin Fang

V3 C1 Upper bound reviewed superseded by T-174, T-182, T-188 and T-279

2026-10-12 published · Fang after Arslanov, Mustafin, Shangitbayev, Ellsworth, Stead, de Winter, Daniel, Couzo · $n = 211, 241, 273, 307$

Fang states two theorems, with their proofs, in a note, draft v0.9 of 18 October 2026, published on Zenodo: Theorem 1, s(n^2 - n + 1) < n for every integer n >= 15; and Theorem 2, s(n^2 - n + F(n)) < n with F(n) = 1 + max{p + 2q : 16p + 21q <= n - 15} over integers p, q >= 0. The proof glues a squeezable 17 x 16 rectangle of 257 squares, or a 22 x 21 rectangle of 443 that adds two, onto a square packing (Lemma 3) and inducts on n from finitely many certificates; the construction gives side n - 1/20000 at every n >= 15.

Inside the case corpus the theorem's inventory certifies $s (211) \leq 14.99995$ , $s (241) \leq 15.99995$ , $s (273) \leq 16.99995$ and $s (307) \leq 17.99995$ , the counts n^2 - n + F(n) for $n = 15$ to 18. Each is above its case's bound (T-149, T-098, T-098, T-136), so these four finite bounds are superseded; nothing supersedes the theorem itself, which no other result implies at any n.

The 14 October review re-derived both theorems from the retained material, before the note was public, and decided every finite piece the chains use, and rebuilt all 76 inventory certificates byte for byte; both maintained exact routes decided the six retained ones, at 211, 241, 273, 307, 308 and 932, with their controls. The note's theorems, hypotheses and conclusions, are the ones stated here; no review has yet read its proofs. Fang's own Lean proof covers Theorem 1 and the single-step bounds of Theorem 2, and nothing here has built it.

Credit the theorem and its certificates to Fang (note, https://github.com/TheSnakeFang/squarepack-certs). The gluing lemma is Arslanov, Mustafin and Shangitbayev's decomposition (Electronic Journal of Combinatorics 28(4), P4.22, 2021); the base packings are de Winter's 211, Ellsworth's and Stead's 241 and 273, the AMS21 and Ellsworth packings of m^2 - m squares, and the author's own; the rectangles grow from Ellsworth's, Stead's and Couzo's packings; the certificate format and the pieces' certificates are Daniel's.

The search, the verifiers, the gluing program and the bundle were written and run with Claude (Anthropic), directed and reviewed by the author, the note says; his comment of 18 October on issue 603 says the Lean project was written with Claude too.

Significance, composition and next rung

Significance: A bound family for every n >= 15 with an explicit construction: the deficiency bound c*(k) <= k - 1 - F(k) improves Arslanov, Mustafin and Shangitbayev's k - 1 at every k >= 15 and Ryu's Theorem 1.4 at 15 <= k <= 78 and at k = 86, his Theorem 1.3 at its best b at 15 <= k <= 68 and 70 <= k <= 75; it settles no case n <= 324, and its four in-corpus finite bounds trail the cases.
Composition: Compound. The finite bounds at 211, 241, 273 and 307 rest on the two-route replay of the retained certificates (E-fang-excess-theorem-exact-feasibility). The theorem for every n >= 15 rests on the published note (E-fang-excess-note-proof), a proof conditional on its finite premise: Lemma 3, the induction and the strict scaling are the published argument, which no machine replays here; Propositions 4 and 5, the 18 pieces the note gives as exact certificates, are its proof.conditional_on, discharged by E-fang-excess-pieces-exact-replay, the 14 October review's exact checker run here on all 18. Both parts are V3, the minimum. The 14 October review's reading of the argument, recorded on E-fang-excess-theorem-report, sets the theorem's C1; no Lean proof has been built here.

Until 24 October the entry held V2, as the rung nearest what the record then held and not as a finding that the proof could not be recovered: V2's premise ended when the author published the note on 18 October, and nothing the record cited was yet evidence the V3 predicate reads. Retaining the note, citing it as a published proof and recording the replay of its 18 pieces here (think-494l) is what moved the rung; the published text alone would have left the theorem the implication from an unexecuted premise. The stage 4 review of the note (think-pxxi) is toward C4 and was not needed for V3.
Next rung: C3 needs a build here of Daniel's Lean proof of both theorems with its axiom receipt (T-236, think-dgrc: about 1.5 to 3 CPU-hours, at most about 8 GB per chunk, and 10 GB of disk, as T-236 prices it). A build of Fang's own Lean proof, about 0.25 CPU-hours, would confirm Theorem 1 and the single-step bounds of Theorem 2 only, not the mixed-step Theorem 2, and would not move this entry on its own. C4 needs, beside the build of Daniel's, a second accepted adversarial review by a distinct reviewer, which the stage 4 review of the note would be (think-pxxi), and a retained human oversight record. The 70 inventory certificates pinned by digest wait for a hosted-data release or a W7 route; they move no rung of this entry.
Unfinished confirmations: C3 (think-dgrc): a build here of Daniel's Lean proof of Theorems 1 and 2, FangFinal from the 18 October Daniel Lean packet, the 18 piece modules generated and built one chunk at a time, with the axiom receipt of theorem1 and theorem2. About 2 CPU-hours, up to about 3 (priced 2026-10-23).

C4 (think-pxxi): the stage 4 adversarial review of the note, draft v0.9, by a reviewer distinct from the 14 October one: Lemma 3, Propositions 4 and 5, the induction and the strict scaling; with the C3 build and a retained human oversight record. Not priced.
Novelty: previously-published Present in an identified source

The cases

Case record

Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT)

As published

The packing as published, in its source’s pose, Ostashev 2026 [Couzo verified bounds 2026-10-14]

14.5414.994

141516

14.52615.526

\sqrt{n}

\sqrt{n} + 1

Proven

$14.54457$ $\leq s (211) \leq$ $14.993550$

exact

Citation record n-211

lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)

upperOstashev & Couzo, GitHub (confirmed T-188)

Open

optimality

The case record

LowerUpper

Verified14.54457190…14.99354962…

Reported14.60509269…14.99354962…

Gap0.44897772…

Case record

Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT)

As published

The packing as published, in its source’s pose, Ostashev 2026 [Couzo certificates 2026-10-13]

15.5415.987

151617

15.52416.524

\sqrt{n}

\sqrt{n} + 1

Proven

$15.54160$ $\leq s (241) \leq$ $15.987118$

exact

Citation record n-241

lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)

upperOstashev & Couzo, GitHub (confirmed T-182)

Open

optimality

The case record

LowerUpper

Verified15.54160895…15.98711709…

Reported15.60000000…15.98711709…

Gap0.44550813…

Case record

Regularized by the Squares Project with its own axis tool (regularize_axis_components/2)

As published

The packing as published, in its source’s pose, Couzo 2026 [PingYou PR 574 certificates 2026-10-13]

16.5316.984

161718

16.52317.523

\sqrt{n}

\sqrt{n} + 1

Proven

$16.53901$ $\leq s (273) \leq$ $16.983926$

exact

Citation record n-273

lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)

upperCouzo et al., GitHub (confirmed T-174)

Open

optimality

The case record

LowerUpper

Verified16.53901493…16.98392596…

Reported16.60000000…16.98392596…

Gap0.44491103…

Case record

Regularized by the Squares Project with its own axis tool (regularize_axis_components/2)

As published

The packing as published, in its source’s pose, ntumlnoob 2026 [Özden s307 upper bound 2026-11-09]

17.5317.979

171819

17.52118.521

\sqrt{n}

\sqrt{n} + 1

Proven

$17.53672$ $\leq s (307) \leq$ $17.979231$

exact

Citation record n-307

lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)

upperntumlnoob et al., GitHub (confirmed T-279)

Open

optimality

The case record

LowerUpper

Verified17.53672503…17.97923096…

Reported17.59416114…17.97923096…

Gap0.44250592…

Results on these cases

20 results in the register on $n = 211, 241, 273, 307$ , oldest first, each with what it established and how it stands now.

2005 published T-007 · $n = 211, 241, 273, 307$
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
V0 C1 Lower bound incomplete on these cases, superseded by T-083 and T-180 (reported)
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 published T-085 · $n = 211, 241, 273, 307$
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
2026-09-16 published T-057 · $n = 211$
$s (211) \leq 14.99796070496771500150 < 15$ , the first packing of 211 squares below the grid on record
V3 C3 Upper bound confirmed superseded by T-188
de Winter · de Winter n211 2026-09-16 · packet · register
2026-09-27 published T-056 · $n = 241, 273, 307$
Smaller packings for 49 counts from $n = 68$ to $307$ , each certified two independent ways
V3 C3 Upper bound confirmed superseded by T-174, T-182 and T-279
Couzo · franciscouzo square-packing 2026-09-27 · packet · register
2026-09-29 published T-083 · $n = 211, 241, 273, 307$
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
V3 C3 Lower bound confirmed
Karakuş · Karakuş 2026 · source · register
2026-10-05 published T-098 · $n = 211, 241, 273, 307$
Exact optima of 48 known-best packings: s(n) ≤ S', 3.5e-13 to 5.0e-11 below each printed side
V3 C3 Upper bound confirmed on these cases, superseded by T-174, T-182, T-188 and T-279
Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · register
2026-10-09 published T-136 · $n = 307$
Seventeen exact rational packings from SQUISH's third request
V3 C3 Upper bound confirmed superseded by T-279
Chaoweeraprasit after Couzo, Xu, Göbel, Schadt, Ellsworth, Hajba, Levy · SQUISH third request 2026-10-09 · packet · register
2026-10-11 published T-149 · $n = 211$
New packings of 155, 156 and 211 squares, each with an exact rational certificate
V3 C3 Upper bound confirmed superseded by T-188
Ostashev after Nakajima, Levy, Xu · Ostashev records 2026-10-11 · packet · register
2026-10-12 published T-163 this result · $n = 211, 241, 273, 307$
s(n² − n + 1) < n for every n ≥ 15, and n² − n + F(n) squares below side n, from Fang
V3 C1 Upper bound reviewed superseded by T-174, T-182, T-188 and T-279
Fang after Arslanov, Mustafin, Shangitbayev, Ellsworth, Stead, de Winter, Daniel, Couzo · Fang excess theorem 2026-10-13 · packet · packet · packet · source 1 · source 2 · register
2026-10-13 published T-174 · $n = 211, 241, 273, 307$
Tighter certificates at 68 counts from PingYou Ltd, of others' packings and its own
V3 C3 Upper bound confirmed
PingYou Ltd after Friedman, Ellsworth, Daniel, Xu, Barnett, Couzo, Ostashev, Chaoweeraprasit, Gupta, Fang, Polkovskyi, Levy · PingYou PR 574 certificates 2026-10-13 · packet · register
2026-10-13 published T-175 · $n = 211, 241$
New packings of 211, 241 and 304 squares, two with merged tilted bands, each certified exactly
V3 C3 Upper bound confirmed superseded by T-182 and T-188
Ostashev after Nakajima, Daniel, de Winter, Couzo, Levy, Xu · Ostashev merged bands 2026-10-13 · packet · register
2026-10-13 published T-180 · $n = 211, 241, 273, 307$
Closed-form lower bound $s (N) \geq a (N)$ for every non-square $N \geq 49$ , reported
V0 C1 Lower bound reviewed
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-13 published T-181 · $n = 211, 241$
Exact rational certificates at 211, 241 and 302 from Couzo
V3 C3 Upper bound confirmed superseded by T-182 and T-188
Couzo after Daniel, Ostashev, Fang, Ellsworth, Levy; Couzo after Daniel, Ostashev, BuddenPing, Fang, Ellsworth, Levy · Couzo issue-583 certificates 2026-10-13 · Couzo certificates 2026-10-13 · packet · packet · register
2026-10-13 published T-182 · $n = 211, 241$
Exact rational certificates at 154, 211 and 241 from Couzo
V3 C3 Upper bound confirmed
Couzo after Daniel, Ostashev, BuddenPing, Fang, Ellsworth, Levy · Couzo certificates 2026-10-13 · packet · register
2026-10-14 published T-188 · $n = 211$
A tighter exact certificate for 211 squares from Couzo, of Ostashev's arrangement
V3 C3 Upper bound confirmed
Couzo after Ostashev, Daniel, Levy · Couzo verified bounds 2026-10-14 · packet · register
2026-10-18 published T-236 · $n = 211, 241, 273, 307$
Daniel reports Lean proofs of Fang's Theorems 1 and 2, $s (n^{2} - n + 1) < n$ for $n \geq 15$
V0 C0 Formalization recorded
Daniel after Fang, Arslanov, Mustafin, Shangitbayev, Levy · Daniel Fang and Ryu Lean 2026-10-18 · packet · source · register
2026-10-23 published T-253 · $n = 211, 241$
Polkovskyi's sub-print re-certifications of nine house packings, 1.3e-19 to 1.7e-19 below each
V0 C1 Upper bound reviewed
Polkovskyi after Daniel, Couzo, Ostashev, de Winter, Chaoweeraprasit, Levy · Mishapolk refinements 2026-10-23 · packet · packet · register
2026-10-28 published T-255 · $n = 307$
Couzo's certificates of ntumlnoob's Kaggle packings at 260 and 307, below T-225 and T-174
V3 C3 Upper bound confirmed superseded by T-279
Couzo after ntumlnoob, Daniel, Levy · Couzo a5a5d76 2026-10-28 · packet · packet · register
2026-10-28 published T-256 · $n = 307$
Couzo's packings from Kaggle notebook packings at 232, 260 and 307, below T-186, T-225 and T-174
V3 C3 Upper bound confirmed superseded by T-279
Couzo after Chilton, ntumlnoob, Lavrentev, Ellsworth, Daniel, Levy · Couzo issue 844 2026-10-28 · packet · register
2026-11-09 published T-279 · $n = 307$
Özden's further arrangement at 307 of Couzo's T-256 packing, one to one, 2.03e-5 below it
V3 C3 Upper bound confirmed
Ozden after ntumlnoob, Couzo, Daniel, Levy · Özden s307 upper bound 2026-11-09 · packet · packet · register

Links

On this site: Case record, $n = 211$ · Frontier row, $n = 211$ · Case record, $n = 241$ · Frontier row, $n = 241$ · Case record, $n = 273$ · Frontier row, $n = 273$ · Case record, $n = 307$ · Frontier row, $n = 307$ · T-163 in the results table
Issues: Issue #603

On GitHub, at main

Register: T-163 in results.yaml, line 21068
Evidence: E-fang-excess-theorem-report · E-fang-excess-theorem-exact-feasibility · E-fang-excess-pieces-exact-replay · E-fang-excess-note-proof · E-fang-excess-lean-report
Proofs and certificates: certificate source · certificate theorem · certificate PIECES.md · proof fang-2026-n2-n-1.pdf · certificate Main.lean · proof Main.lean
Sources: Fang excess theorem 2026-10-13 · Fang excess note 2026-10-19 · Fang excess Lean 2026-10-18
Source packet: resources/web/fang-excess-note-2026-10-19/README.md · resources/web/fang-excess-lean-2026-10-18/README.md · resources/web/fang-excess-theorem-2026-10-13/README.md
Artifacts: 21 artifacts and controls in 15 directories. Complete artifact list in the result entry. docs/project/reviews packing/cases/asymptotic packing/devtools packing/resources/web/fang-excess-lean-2026-10-18 packing/resources/web/fang-excess-lean-2026-10-18/source/Sqlean packing/resources/web/fang-excess-note-2026-10-19 packing/resources/web/fang-excess-note-2026-10-19/source/note packing/resources/web/fang-excess-note-2026-10-19/zenodo packing/resources/web/fang-excess-theorem-2026-10-13 packing/resources/web/fang-excess-theorem-2026-10-13/acquisition packing/resources/web/fang-excess-theorem-2026-10-13/receipts packing/resources/web/fang-excess-theorem-2026-10-13/review/programs packing/resources/web/fang-excess-theorem-2026-10-13/source/theorem packing/resources/web/fang-excess-theorem-2026-10-13/source/tools packing/tests
Case file: frontier/n-211.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-241.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-273.md (verified lower, verified upper, reported lower, reported upper) · frontier/n-307.md (verified lower, verified upper, reported lower, reported upper)