s(n² − n + 1) < n for every n ≥ 15, and the F(n) excess (Kevin Fang): tracking an unreported result

@TheSnakeFang

This issue tracks a significant result that reached the project through a watched repository rather than an issue. Its author is Kevin Fang (@TheSnakeFang), and the source is TheSnakeFang/squarepack-certs, retained at 078789a. We opened it so that the result's intake, review and validation have one public place.

The claim, from draft v0.6 (13 October 2026) of Kevin Fang's note:

Theorem 1. s(n² − n + 1) < n for every integer n ≥ 15.
Theorem 2. s(n² − n + F(n)) < n, with F(n) = 1 + max{p + 2q : 16p + 21q ≤ n − 15}.

The proof, as retained:

Glue a squeezable 17 × 16 rectangle of 257 squares, or a 22 × 21 rectangle of 443 squares, onto a square packing. The gluing lemma is Arslanov, Mustafin and Shangitbayev's decomposition (Electronic Journal of Combinatorics 28(4), P4.22, 2021).
Induct on n from finitely many certificates. The construction gives side n − 1/20000 at every n ≥ 15.

What has been checked here (review of 14 October):

Both theorems were re-derived from the retained material, and every finite piece the chains use was decided.
All 76 inventory certificates were rebuilt byte for byte.
Both of the project's exact verification routes decided the six retained certificates, at 211, 241, 273, 307, 308 and 932, with their controls.
The four finite bounds it gives inside the record's cases (211, 241, 273 and 307) are each above the case's current bound. The theorem itself is implied by no other result at any n.

What is open:

The note itself, draft v0.6, is not in the repository, so its text has not been read. We would be glad to retain a copy.
A second independent adversarial review, and a human oversight record.
An exact replay of the 70 inventory certificates pinned by digest, about 99 CPU-hours. That replay is on hold under the project's current compute cap.
Section 5 composites (composites/ at bef5c42). These are the smallest reported side at 81 counts from 420 to 4035: shipped certificates at 28 of those counts and table-only rows at 53. Their import is pending. An exact replay of the 38 shipped certificates is about 122 CPU-hours and is also on hold.

Records. The theorem is being registered as a reported result in the records pull request #602. Kevin Fang's direct certificates at 380, 381 and 382 are covered in the intake ledger, #601. We will post the result's id and rungs here once it is on main, and update the open items as they close.

Generated by Claude Code

@TheSnakeFang

As this issue promised, the result's id and rungs now that #602 has merged. Thank you, @TheSnakeFang, for the theorem and for publishing its certificates.

T-163, V2/C1, significance S4, reviewed: s(n² − n + 1) < n for every n ≥ 15, and s(n² − n + F(n)) < n, credited Fang after Arslanov, Mustafin, Shangitbayev, Ellsworth, Stead, de Winter, Daniel, Couzo. It is dated by Theorem 1's first commit, 12 October. C1 rests on the review of 14 October, which re-derived both theorems from the retained material and found no blocking defect.
The finite bounds: both of this repository's exact routes, sqpack.verify and devtools.check_rational_witness_independent, our own implementations rather than the author's code, replayed the six retained certificates at 211, 241, 273, 307, 308 and 932 with their controls (E-fang-excess-theorem-exact-feasibility, confirmed). The four inside the case corpus, 211, 241, 273 and 307, are each above their case's bound, so the site marks them superseded; nothing supersedes the theorem itself.
Still open, and why this issue stays open: the owner's choice between V3, on the review's reading that the proof can be recovered from the public repository, and a lower rung; for C4, a second accepted adversarial review by a distinct reviewer and a retained human oversight record; the note, draft v0.6, which we would still be glad to retain; the 70 inventory certificates pinned by digest, which wait for a hosted-data release; and the import of the Section 5 composites.

Evidence: E-fang-excess-theorem-report (reviewed) and E-fang-excess-theorem-exact-feasibility (confirmed). On main: RESULTS.md, the packet.

Generated by Claude Code

requests: record #602's post-merge follow-ups and the 14 October verd…

Thanks for the review and for T-163.

Two of the open items are closed on my side:

The note (now draft v0.8, 2026-10-18) is in the bundle at note/fang-2026-n2-n-1.md, squarepack-certs commit 0e9be7961773aa78b879c4ee6ba584a67e2e5513. Changes since v0.6: Codex-review corrections already folded in, Theorem 2 in the (p, q) form, and a formal verification paragraph. I plan to post it to arXiv (math.CO) and will add the identifier here.
The Lean 4 formalisation is public at https://github.com/TheSnakeFang/squarepack-lean (commit 947bdae): Theorem 1, the side n − 1/10000 version, and the single-step form of Theorem 2, on top of Evan Daniel's Spec.lean unchanged. Axioms are the standard three, no sorry or native_decide; the README has the build and the checker.

On V3 versus a lower rung: your call. The proof is recoverable from the bundle plus the note, and the Lean repo is a second route to Theorem 1 that doesn't go through my checkers at all.

No rush on the digest replay or the Section 5 composites from my side; the composites are a byproduct of the construction, not part of the proof. Happy to answer questions on either.

The search, checkers, bundle and Lean project were written with Claude as a coding and research agent, directed and reviewed by me.

Thanks for the note update and the public Lean pin. I've added squarepack-certs@0e9be796 and squarepack-lean@947bdae to the 19 October intake, with a separate review of the Lean route to T-163.

T-163 remains V2/C1 while we compare the formal statements and hypotheses with the registered theorem, inspect the proof and axiom closure, and reproduce the build. The earlier independent derivation still supports its current C1; the new source claim alone does not establish a higher verification rung. I'll report the outcome here after those checks. The Section 5 composites remain a separate intake item and do not hold up this theorem review.

The note is now archived with a DOI: https://doi.org/10.5281/zenodo.23463481 (v0.9, 2026-10-18, CC BY; PDF and LaTeX source). Same text as note/fang-2026-n2-n-1.md in the bundle at 6e26525. arXiv is on hold for now.

Thanks for the DOI update. The 19 October intake now records note v0.9 and DOI 10.5281/zenodo.23463481, alongside the bundle update and the unchanged Lean pin. The DOI assets and their binding to the registered statements remain queued with the note and Lean review; T-163 remains V2/C1.

The source now explicitly scopes that Lean pin to Theorem 1 and the unmixed bounds of Theorem 2. We will keep the statement, axiom/build checks and publication custody separate from the Section 5 composite import, and report the reviewed outcome here. No new rung or completed DOI-asset review is claimed by this acknowledgement.

@TheSnakeFang

@TheSnakeFang just a note (from me, human) this is a great result!

Are you on Twitter? If you DM me x.com/ojoshe I'd be glad to invite you to our group chat.

fix(#446): answer Reviews A and B of #688 on the T-205 to T-207 records

requests: review A of #696, the 19 and 20 October reply records say w…

@jlevy

@jlevy thanks! And yes, I'm at x.com/sofangtastic - just sent a dm

records: the nine pending reviews with no issue get tracking issues #772

devtools(check_requests): --pending lists held and closed-only tracke…

merge: main 11d0ab0 (#770, the pending reviews' tracking issues) into…

Where T-163 stands now that #770 has merged.

T-163, V2/C1, significance S4, reviewed. The rungs are unchanged.
The theorem-wide bound is now assessed against its family, and it is current. Theorem 2's deficiency bound, c*(k) <= k - 1 - F(k), is strictly the smallest bound any statement of the family gives at k = 15 to 68 and k = 70 to 75. The family here is Arslanov, Mustafin and Shangitbayev's k - 1 and every bound in Sungjoon Ryu's two deficiency preprints. At k = 69 and 76 it ties Ryu's Theorem 1.3, which was reported first (9 October), so the tie stays with Ryu. From k = 77 on, Ryu's Theorem 1.3 is smaller. The record's gate recomputes the comparison (cases/asymptotic/deficiency_family.py) on every change, so a new bound in the family reopens it. T-163 now counts among Kevin Fang's Records on his profile, and the "Review pending" note there is gone.
A correction to what we said before. We wrote that Theorem 2 improves on Ryu's bound for 15 <= k <= 78 and at k = 86. That compared it with Ryu's Theorem 1.4 alone. Ryu's Theorem 1.3, taken at its best b, is smaller at 77, 78 and 86, and equal at 69 and 76. The record now states both comparisons.
What would move V2 to V3. The note is public now (v0.9, DOI 10.5281/zenodo.23463481), so the reason for V2, a proof that is not publicly recoverable, no longer holds. The rung moves when the record holds an entry for the theorem itself. The next route is to retain the note v0.9 here, bind it to T-163's statement as a published proof, and review it at stage 4; that costs no CPU. The other route is a build here of Evan Daniel's Lean proofs of both theorems, which the record now holds as a reported formalization (T-236), about 1.5 to 3 CPU-hours. Because that build reproduces his proof with his own code, it would also take the theorem to C3. We will report the outcome here.
Still open: C4 needs a second accepted adversarial review by a distinct reviewer and a retained human oversight record. The 70 inventory certificates pinned by digest are waiting for a hosted-data release, and the Section 5 composites are a separate import.

Generated by Claude Code

records(#294, #603, #772 to #786): the replies posted after #770's de…

merge: main 6808d29 (#787, the stage 7 records) into the Fang note br…

@TheSnakeFang

Thank you, @TheSnakeFang, for publishing the note and the Lean pin. Where T-163 stands in the record on main now that the retention has merged:

T-163 is now V3/C1. Our reply of this morning (6381479105) had it at V2/C1 and expected V3 after a stage 4 review of the note. It moved sooner, for a different reason. The note, draft v0.9 (10.5281/zenodo.23463481), is retained from the Zenodo record (the PDF, the LaTeX source and their checksums), with the same text in Markdown from squarepack-certs at 9ffba0f, and is recorded as a published proof (E-fang-excess-note-proof), which is what V3 asks for. Because the proof is computer-assisted, our rules treat its 18 pieces (Propositions 4 and 5) as a premise that has to be executed here, not only read. So the exact checker written for the review of 14 October was run again on all 18 (E-fang-excess-pieces-exact-replay): every one is strict-valid, with the least squeeze, 0.000690…, at 308. C1 still rests on the review of 14 October, which re-derived both theorems from the bundle before the note was out, and the four finite bounds at 211, 241, 273 and 307 stay re-verified here on both of our exact routes.
The statements match. The note's Theorems 1 and 2, hypotheses and conclusions, are the ones T-163 states, and so is the construction's side n − 1/20000.
Your Lean proof is retained, not yet built. squarepack-lean at 947bdae is in its own packet. theorem1 is Theorem 1 over Evan Daniel's Spec.lean (the same bytes as his), and main is stronger, at side n − 1/10000. theorem2 uses jExc n, the larger of the two single-step bounds. That equals F(n) for 15 ≤ n ≤ 51; after that it falls one short wherever n − 15 leaves 16 to 20 on division by 21 (n = 52–56, 73–77, 94–98, …), where one step of each kind gains, and equals F(n) otherwise. It is never more than one short. We read the axiom claim and the absence of sorry and native_decide from the source text only. No build ran here: the toolchain and the Mathlib cache need about 9 GB of disk this host does not have.
Two small points, neither about the mathematics. The squarepack-lean README's first line still says "Kernel-checked Lean 4 proof of Theorems 1 and 2", and Theorem2.lean calls jExc "The excess of Theorem 2", where the note and the squarepack-certs README say Theorem 1 and the unmixed bounds. And Section 6's "the mixed-step bound is proved here [FanL26]" can be read as citing the Lean repository for the mixed-step bound.
Still to come. A build here, with its axiom receipt, of Evan Daniel's Lean proof of both theorems (T-236, about 1.5 to 3 CPU-hours) would take T-163 to C3. A build of yours (about a quarter of a CPU-hour) would confirm Theorem 1 and the single-step bounds but not the mixed-step Theorem 2, so it would not move T-163 on its own. C4 needs, beside that build, a stage 4 review of the note's own proofs against the 14 October reconstruction and a human oversight record. Nothing is needed from you for any of this.

Evidence: E-fang-excess-note-proof (published proof), E-fang-excess-pieces-exact-replay (the 18 pieces, replayed here), E-fang-excess-lean-report (reported). On main: RESULTS.md, the note packet, the Lean packet.

Generated by Claude Code

merge: main 830dfb4 (#781, #603's row) into the Couzo answers branch

records(#603): the follow-up of 11:29:46Z after #781, T-163 at V3/C1

release: the survey re-measured after #603's follow-up record (think-…

merge: main 90a5437 (#790 Couzo's answers, the watch reads, #534/#536/#…

Navigation Menu

Repository navigation

s(n² − n + 1) < n for every n ≥ 15, and the F(n) excess (Kevin Fang): tracking an unreported result #603

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

s(n² − n + 1) < n for every n ≥ 15, and the F(n) excess (Kevin Fang): tracking an unreported result #603

Description

Activity

jlevy commented on Oct 14, 2026

TheSnakeFang commented on Oct 18, 2026

jlevy commented on Oct 19, 2026

TheSnakeFang commented on Oct 19, 2026

jlevy commented on Oct 19, 2026

jlevy commented on Oct 19, 2026

TheSnakeFang commented on Oct 24, 2026

jlevy commented on Oct 24, 2026

jlevy commented on Oct 24, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions