T-163: s(n² − n + 1) < n for every n ≥ 15, and n² − n + F(n) squares below side n, from Kevin Fang
V2 C1 Upper bound reviewed superseded by T-174, T-182 and T-188
Fang states two theorems of a note, draft v0.6 of 13 October 2026, which is not in his repository: 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}. 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, tools/glue.py) 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 , , and , the counts n^2 - n + F(n) for 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 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 itself has not been read.
Credit the theorem and its certificates to Fang (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 verifier and the bundle were written and run with Claude (Anthropic), directed and reviewed by the author.
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 at 15 <= k <= 78 and at k = 86; 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 Lemma 3, the scaling lemma and the induction, which no machine replays, and on the 14 October review's reading of them, which sets the minimum: C1. The entry declares V2, the minimum over its parts: no evidence entry records that reading as a proof audit. The review reads the proof as recoverable from the public repository, which would support V3, and the import plan read it as not publicly recoverable; the owner decides between the two readings.
- Next rung
- C4 needs a second accepted adversarial review by a distinct reviewer and a retained human oversight record; the note, draft v0.6, is asked of the author, and its own text has not been read. The 70 inventory certificates pinned by digest wait for a hosted-data release or a W7 route; they move no rung of this entry.
- Novelty
- previously-published Present in an identified source
The cases
As published
Proven
- 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
As published
Proven
- 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
As published
Proven
- 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
As published
Proven
- exact
Citation record n-307
lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)
upperChaoweeraprasit & PingYou Ltd, GitHub (confirmed T-174)
Open
- optimality
The case record
Results on these cases
15 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 these cases, superseded by T-083 and T-180 (reported)
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-16 published T-057 ·
, the first packing of 211 squares below the grid on record
V3 C3 Upper bound confirmed superseded by T-188
2026-09-27 published T-056 ·
Smaller packings for 49 counts from to , each certified two independent ways
V3 C3 Upper bound confirmed superseded by T-174 and T-182
Couzo · franciscouzo square-packing 2026-09-27 · packet · register
2026-09-29 published T-083 ·
for every nonsquare
V3 C3 Lower bound confirmed
Karakuş · Karakuş 2026 · source · register
2026-10-05 published T-098 ·
Exact optima of 48 known-best packings:
s(n) ≤ S',3.5e-13to5.0e-11below each printed sideV3 C3 Upper bound confirmed on these cases, superseded by T-174, T-182 and T-188
Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · register
2026-10-09 published T-136 ·
Seventeen exact rational packings from SQUISH's third request
V3 C3 Upper bound confirmed on these cases, superseded by T-174
Chaoweeraprasit after Couzo, Xu, Göbel, Schadt, Ellsworth, Hajba, Levy · SQUISH third request 2026-10-09 · packet · register
2026-10-11 published T-149 ·
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 ·
s(n² − n + 1) < n for every n ≥ 15, and n² − n + F(n) squares below side n, from Fang
V2 C1 Upper bound reviewed superseded by T-174, T-182 and T-188
Fang after Arslanov, Mustafin, Shangitbayev, Ellsworth, Stead, de Winter, Daniel, Couzo · Fang excess theorem 2026-10-13 · packet · register
2026-10-13 published T-174 ·
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 ·
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 ·
Closed-form lower bound for every non-square , reported
V0 C1 Lower bound reviewed
Hosono · wand125 closed form 2026-10-14 · packet · packet · register
2026-10-13 published T-181 ·
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 ·
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 ·
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
Links
- On this site
- Case record, · Frontier row, · Case record, · Frontier row, · Case record, · Frontier row, · Case record, · Frontier row, · T-163 in the results table
On GitHub, at main
- Register
- T-163 in
results.yaml, line 20521 - Evidence
E-fang-excess-theorem-report·E-fang-excess-theorem-exact-feasibility- Proofs and certificates
- certificate
source· certificatetheorem - Sources
- Fang excess theorem 2026-10-13
- Source packet
resources/web/fang-excess-theorem-2026-10-13/README.md- Artifacts
13 artifacts and controls
resources/web/fang-excess-theorem-2026-10-13/README.mdresources/web/fang-excess-theorem-2026-10-13/acquisition/claims.jsonresources/web/fang-excess-theorem-2026-10-13/source/theorem/n015_F1.certresources/web/fang-excess-theorem-2026-10-13/source/theorem/n016_F1.certresources/web/fang-excess-theorem-2026-10-13/source/theorem/n017_F1.certresources/web/fang-excess-theorem-2026-10-13/source/theorem/n018_F1.certresources/web/fang-excess-theorem-2026-10-13/receipts/exact-certification.json.xzresources/web/fang-excess-theorem-2026-10-13/source/tools/glue.pyresources/web/fang-excess-theorem-2026-10-13/receipts/inventory-and-deficiency.jsoncases/asymptotic/fang_excess_inventory.pydocs/project/reviews/review-2026-10-14-fang-excess-theorem-and-direct-certificates.mddevtools/upper_bound_reports.pytests/test_upper_bound_reports.py- 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)