records(L145): import #973, s(k^2 - 5) = k for every k >= 7, as T-298 (reported, V0/C1) - #974

What this branch cost

This branch is the import of #973 (lane L145, bead think-2vgx): Mohsen Khalili and Sara
Gharabaghi’s $s(k^2 - 5) = k$ for every $k \ge 7$, taken through triage, retention, a
time-boxed replay and registration as T-298, with the blind stage 4 review (lane L144,
think-h10k) merged and mapped. It took about 3.5 hours of agent wall on a four-core
container and about 2.5 CPU-hours of replay at nice -n 19, two jobs at most, inside the
lane’s box of about 4; the review lane spent about 3.1 more. It does not run the full
replay, priced at about 145 to 180 CPU-hours (up to about 320) and held for the owner on
think-0h7r, nor build the Lean reduction, nor review zmx2’s area-density and
first-order lemmas, which is held on think-kn13.
The senior review’s fixes (lane L147) took about 0.8 hours of agent wall to the push and
under 1 CPU-hour, nearly all of it the edit and records tiers, the touched tests and two
paper-render comparisons.

New Results and Their Significance

Results and Dispositions

Changes by Purpose

Review Fix (L146)

Lane L147 (bold-ritchie-l147) applied every B and S item of the senior review L146 and
the notes it asked for, in 4471544e0; then merged main at b526521e4 (#975, the
browser cache keyed on the Ubuntu release, for the two WebKit failures) and re-pinned.

• B1: the record no longer calls the review’s programs clean-room: T-298’s
  composition, the three report entries’ review notes, the partial-checks entry, the
  request notes, the packet README and the row above say “own exact programs
  (independent, not clean-room)”; §13 of the review gains a dated note on why its own
  word differs from V-khalili-973-review-check’s.
• B2: all nine case files carry the review, F1 on think-kn13, F2 and the held
  replay. B3: the News draft below, and the S4 box ticked.
• S1–S8: as given: §13’s F1/F2 split; the controls sentence with F8; 83 of the 443
  refusals at the cap; the tool’s custody change dated (8784343, 72db934, OR-16)
  in the README, the label and the verifier summary; F2 not wholly think-0h7r’s, in
  next_rung and think-2vgx’s notes; the score left as the import lane’s draft; the
  no-public-change record at V0/C1, with compare_paper_renders re-run (still only the
  explainer’s register count); and the receipts-equal-records test.
• S9: E-khalili-973-replay-sample (this lane’s runs) and
  E-khalili-973-review-replay-sample (the review’s), each replayed-here,
  same-implementation, coverage sample of 459 runs (59 and 18), cited by T-298, the
  request and the nine cases.
• Notes: N1 (headline in T-081’s words, with k plain so the results page keeps its
  projection under 1,700,000), N2, N3 (145 now follows: the price uses the review’s
  random-job Tight-Tile factor), N4, N5, N6, N7, N8, N9, N10, N11 (the review ran at
  tbd-strong, said wherever the record states its tier), N12 (the cropped sum is
  weight_sum; compare.json.gz rewritten from the same receipts, that key alone
  changed) and N14. N13 needed nothing.

Validation

• Local, lane L147: at 4471544e0, the edit tier (packing-validate --edit) passed 71 of
  71 steps, its full basedpyright run at 0 errors; on the merged tree, the records tier
  (--records --jobs 3) passed 55 of 55. check_requests (206 issues, every id
  resolves), check_results (298 results), site_urls --check,
  check_release_impact --base origin/main (every candidate has a disposition),
  check_integrity_ceremony, retained_data check on the packet and
  check_added_blobs --base origin/main (2.7 MB thin pack) pass. pytest on
  test_known_best_atlas.py, test_overview.py, test_result_status.py,
  test_apply_closed_form.py, test_validation_cli.py, test_replay_k2m5_family.py
  and test_t007_consumer_audit.py, then the first two again after the headline and
  credit fixes: all pass; test_release.py and test_pages_workflow.py after the merge
  and pin: 68 passed. The results page projects 1,699,269 bytes (298 results plus 20 at
  the 4,587-byte P90 row) against 1,700,000. compare_paper_renders against
  0db247de7: only the explainer’s HTML and Markdown differ, by the register count.
• Hosted: the run at 0b856c746 is on this pull request.

Documentation and Replanning

• Documentation review: the packet README states what ran, what did not, the review’s findings, the reconciled price and the authors’ questions; the reader-facing changes are the case records and generated views.
• Selected next entry: post the reply on s(k² − 5) = k for every k ≥ 7 (family k ≥ 10 by one periodic measure; k = 7, 8, 9 known) #973 from think-2vgx’s Reply draft once this merges (T-298 at V0/C1, the review’s F1 and F2, the held replay and lemma review, and the merged questions); the earlier Acknowledgement draft there is superseded.
• Deferred candidates: the full replay and Lean build (think-0h7r, owner budget; a pilot of two or three of the largest Tight-Tile jobs would narrow the price); the review of zmx2’s lemmas (think-kn13); a hosted release of tight_tile/cov.tar.xz before receipts compared with it are cited; a second implementation of the Tight-Tile Lemma, which no bead tracks (F2).
• PR has exactly one S1–S5 label, an editorial rationale and its News/changelog disposition: S4 (the S4 label), T-298’s draft score as a claim, which the stage 4 review did not score in its text; News: the draft under News below, for the changelog step after the merge. intake applied.

News

T-298 is registered at S4, so this pull request drafts its News item before the merge
(result-import.md, “Announce a Significant Result”). The entry is below, to land in
packing/site-changelog.yaml after the merge, dated the merge day and naming this pull
request by its retained merge commit; render_changelog needs the merged delivery row
first.

Khalili and Gharabaghi Report s(k² − 5) = k for Every k ≥ 7 (the merge day). Mohsen
Khalili and Sara Gharabaghi report that $k^2 - 5$ unit squares need a square of side
$k$ for every $k \ge 7$. One periodic family of measures reduces every $k \ge 10$ to a
single finite statement on an $11 \times 11$ board, decided with Evan Daniel’s interval
checkers and a new Tight-Tile Lemma where box subdivision stalls, and a Lean
development carries that statement to every $k \ge 10$. New to the record are eight
open counts, $n = 116$ to $319$ ($k = 11$ to $18$). T-298 is reported at V0/C1: a
stage 4 review here found no blocking defect, and no verified bound moves until the full
replay and the Lean build run.

- id: khalili-gharabaghi-k2m5-family-reported
  date: 'YYYY-MM-DD'  # the merge day of #974
  title: Khalili and Gharabaghi Report s(k² − 5) = k for Every k ≥ 7
  significance:
    score: 4
    rationale: >-
      T-298, scored S4 as a claim by the import lane: a bound family, the deficit-5 case
      of Friedman’s conjecture, that would settle eight open counts, n = 116 to 319
      (k = 11 to 18), with a new argument, the Tight-Tile Lemma, as T-064 and T-081 are
      S4 families. The stage 4 review stated no score. Reported at V0/C1: limited by the
      held replay, the held lemma review and the review’s F1 and F2.
  topics: [optimality, lower-bound]
  categories: [records]
  pull_requests: [974]
  issues: [973]
  result_ids: [T-298]
  summary: |-
    Mohsen Khalili and Sara Gharabaghi report that $k^2 - 5$ unit squares need a square
    of side $k$ for every $k \ge 7$. One periodic family of measures reduces every
    $k \ge 10$ to a single finite statement on an $11 \times 11$ board, decided with
    [Evan Daniel](packing/contributors/people/evan-daniel.md)’s interval checkers and a
    new Tight-Tile Lemma where box subdivision stalls. New to the record are eight open
    counts, $n = 116$ to $319$. T-298 is reported at V0/C1.
  details: |-
    - $k = 7$, $8$ and $9$ rest on certificates the record already holds (T-252, T-066
      and T-184), and $s(95) = 10$ is Greff’s T-191. At $n = 116$ to $319$ the reported
      lower bounds move to $k$; the verified ones are unchanged.
    - What ran here, about 2.5 CPU-hours: the source’s fast checks, 30 of the 55 columns
      of Daniel’s `zmx2` sweep, root 9632 with both checkers and 26 of the 326 Tight-Tile
      runs, each equal to the source’s records, and the source’s controls, refused as
      reported. That is a diagnostic, not a replay. The full replay, about 145 to 320
      CPU-hours, and the Lean build are held for the owner.
    - A stage 4 review by a separately prompted Claude agent, at the strong tier rather
      than the strongest the runbook asks for, found no blocking defect and two major
      findings: `zmx2`’s area-density and first-order lemmas, on which most of the
      board’s poses rest, have no review in this record (F1, held), and the Tight-Tile
      Lemma has one implementation and no full replay (F2).
    - 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. It builds on Daniel’s linear program, format, checkers and Lean
      reduction. Not peer reviewed.
  artifacts:
    - kind: result
      label: Current T-298 record
      target: https://squaremath.org/result/t-298.html
  references:
    - label: Source, retention and the checks made here
      target: packing/resources/web/moh63-dev-k2m5-family-2026-11-13/README.md
    - label: Stage 4 mathematical review
      target: docs/project/reviews/review-2026-11-14-khalili-gharabaghi-k2m5-973.md

Limits

T-298 is a reviewed report: nothing here replays Valid11 in full or builds the Lean
reduction, so no verified lower bound moves and $n = 116$ to $319$ stay open in their
verified lanes. The two lanes’ samples show that the source’s programs reproduce their
recorded outputs where they ran; zmx2’s area-density and first-order lemmas are unread
by any review here (F1), and the Tight-Tile Lemma rests on one implementation (F2). The stage 4 review ran at tbd-strong, not the tbd-strong-max tier the runbook asks for. This
branch records #973; the reply on the issue follows the merge.

https://claude.ai/code/session_01E8g3iMDhVT21veLdEABoxV

Generated by Claude Code