Closed-form lower bound s(N) ≥ a(N) for every non-square N ≥ 49, above the register for 156 n in 104–319: registration request

We would like to report a computer-assisted lower bound that holds for every non-square N ≥ 49.

Claim. With k = ⌊√N⌋, the interval (0, 1] of the fractional part is split into 34 intervals I_i = [d0_i, d1_i], each with exact rationals α_i, β_i, and

s(N) ≥ a(N) = max_i min( 2α_i + √(4α_i² + N + 4β_i − 4α_i k), k + d1_i ),

taken over the intervals whose root exceeds k + d0_i. a_of_n.py computes a(N) in exact rational arithmetic and prints a decimal rounded down.

Where.

Folder: https://github.com/wand125/square-packing/tree/main/problems/closed-form (README, SPEC.md, intervals.json, a_of_n.py, checker, indep-checker, receipts)
Certificates: Release closed-form-v1, https://github.com/wand125/square-packing/releases/tag/closed-form-v1 (one asset per interval)
Write-up: https://wand125.github.io/square-packing/paper-closed-form.html

Checks.

Structure of all 68 families checked (structure_all.py, ALL STRUCTURE OK).
Full replay of all 136 records, 187,183,108 leaves, with replay4d on fresh Ubuntu 24.04 (rustc 1.86.0); the published build replayed intervals 1 and 34 again from the published assets.
An independently written checker (Rust, from SPEC.md only, sharing no code with replay4d) accepted every leaf of intervals 1 and 34: 91,044 roots, 3,138,681 leaves, 0 refusals. Source, tests and reports: https://github.com/wand125/square-packing/tree/main/problems/closed-form/indep-checker
The proof does not use Nagamochi's Lemma 1 or Karakuş's bound. The certified saving exceeds δ/2 on all of (0, 1], so a(N) ≥ F(N) = 1 + √(N − 2k + 1) (capped at k + 1) for every non-square N ≥ 49.

Register comparison (packing/frontier at f73e9de, n ≤ 324). a(N) is above both the reported and the verified lower bound for these 156 n:

k	n
10	104–116
11	125–139
12	148–164
13	173–191
14	201–220
15	230–251
16	261–284
17	294–319

The largest gain is at n = 106: a(106) = 10.403976… against 10.327379… (reported) and 10.310708… (verified, Karakuş). python3 a_of_n.py 104-324 --json gives the values and the interval used for each n. For n < 104 the register already has better bounds.

Limits. Computer-assisted; not peer reviewed. The second checker covers intervals 1 and 34 only.

The search, the certificates, the checkers and this text were produced with AI assistance (Claude and Codex), under the direction of and reviewed by Hiroaki Hosono (wand125).

Credit: Hiroaki Hosono (wand125).

@wand125

@wand125, thank you for the report, and for opening an issue for it. Our intake read had already picked the folder up from your repository, so this answers both.

What we have retained. problems/closed-form at 9a28a84. That is the folder as eb0fd19 added it; no later commit changes it before 746e2c5. We also pinned the closed-form-v1 release by its ASSET.json digests, and all 35 assets match the API digests and SHA256SUMS. Your 746e2c5 (10:38Z today), which adds cfcheck under indep-checker/, came after that pin. We will retain it as a later revision and treat it as new evidence for the same claim.

What we have checked so far.

We computed a(N) here in two ways with our own code: from SPEC.md's definition by bisection, and in exact arithmetic. Both agree with a_of_n.py at all 3,498 counts N ≤ 3600.
We ran structure_all.py unchanged from the retained copy. It reports ALL STRUCTURE OK for all 68 families, the same as your receipt, and two mutated inputs were refused.
A mathematical review read the argument from the measure principle to the claim: the scaling, the total-mass identity, the §2.3 localization, every §5 leaf lemma, the tiling, the u = 0 case and the coverage of (0, 1]. It also read the Rust checker against SPEC.md. It found no blocking or major defect.
a(N) is above no recorded upper bound, and it equals m at m² − 1, m² − 2 and m² − 3 (m ≥ 8), where the record already has the exact value.
Against the record at f73e9de, a(N) is above the reported lower bound at the 156 counts you list, and above the verified lower bound at 189 counts. At 125, an earlier pending report (11.26) is above a(125) = 11.2545…, so the reported lane moves at 155 counts.

What we have not run. By your receipt, the full replay of the 136 records with replay4d takes 4,294 CPU-hours. That waits for a compute budget here. Next is cfcheck's replay of intervals 1 and 34, once it is retained.

Three small questions from the review:

receipts/structure.json records validate_family.py with SHA-256 fdd61866…, but the published file is 22e55f17…. Was the receipt made with an earlier revision of the script? The published script reproduces every result.
b3d_sort.rs is compiled into replay4d but is not part of the source hash replay4d prints. Could the hash include it?
Could the receipts record the B3_PLAIN_RF setting each run used?

The result will be registered in report order with this week's other reports. We will post again with its id and rungs once that is on main.

Generated by Claude Code

Thank you for the careful read. Answers to the three questions; the fixes are in wand125/square-packing@1c661b7.

validate_family_sha256 in receipts/structure.json. Yes. The receipt was written about 20 seconds before a last edit to validate_family.py, and we did not keep that intermediate revision. We reran structure_all.py with the published script on the published assets: ALL STRUCTURE OK, and the new receipt differs from the old one only in validate_family_sha256, which is now 22e55f17…. Every per-interval result is identical.
b3d_sort.rs and the source hash. Agreed. From replay4d 0.1.1 the source hash also covers seam4d_core/src/b3d_sort.rs; the published 0.1.1 sources hash to f8cafeab078e1de31bacdef9c5c08ad70938f1b1b20fd3a2e1e54de9f73f1742. Nothing else in the checker changed apart from item 3, and the 28 tests pass. The existing receipts keep their hashes (306ad4b5… for the replay, 92002e0e… for the published build). b3d_sort.rs has SHA-256 23be1db0de55790110ff97c966bf34a6046c1d224a0f5bad98c6639866895928 in the sources used for the replay and in the published sources, and has not changed since. README.md and SPEC.md now say this.
B3_PLAIN_RF. No run in the receipts set it. Neither the replay driver nor the commands recorded in published_checker.json set the variable, so every run used the default path. (With B3_PLAIN_RF=1 the rational-function arithmetic follows the Python reference step by step, for cross-checking; the reduced form, and so every decision, is the same.) From 0.1.1 each result records the value as env.B3_PLAIN_RF (unset when not set), and replay_all.py prints it.

intake: retain wand125's cfcheck at 746e2c5, check its independence, …

merge: the wand125-cfcheck lane (think-3n1x): wand125's independent c…

intake: retain wand125's cfcheck at 746e2c5, check its independence, …

requests: record the 14 October replies and entries; read evand to 62…

@wand125

@wand125, thank you; these answer all three. We read 1c661b7 against 9a28a84 and 746e2c5, and checked:

The source hash. We recomputed replay4d's source hash from main.rs's file list, reading each file from the commit. It is 92002e0e… over 10 files at 9a28a84, and f8cafeab… over 11 files at 1c661b7, as you state.
b3d_sort.rs is 23be1db0… at both commits. Only eb0fd19 has ever changed it.
validate_family.py is 22e55f17… at both commits. In receipts/structure.json, only validate_family_sha256 changed.

The record will note this about the existing receipts. The 4,294 CPU-hour replay receipts are still from 0.1.0, so their hash does not cover b3d_sort.rs. That file's bytes are unchanged, so this is now checkable. That no past run set B3_PLAIN_RF rests on your statement above, because those receipts predate the field.

We will retain 1c661b7 as a later revision of the same evidence, with b3d_sort.rs. The result's registration is unchanged.

Generated by Claude Code

intake: retain wand125's cfcheck at 746e2c5, check its independence, …

merge: the wand125-cfcheck lane (think-3n1x): wand125's independent c…

@wand125

@wand125, thank you. With #602 merged, the closed form is registered on main:

T-180, V0/C1, significance S4, reviewed: s(N) ≥ a(N) for every non-square N ≥ 49, credited Hosono, as this issue asks. C1 rests on the review of 14 October, which found no blocking defect; V0 because no record has been replayed here. The verified lanes are unchanged until a replay.
A correction to our first reply, which said the reported lane moves at 155 counts: the case records take a(n) at 154 of the 156 counts. At 148, as at 125, your own earlier report is stronger and pending adoption (306/25 at 145 to 149, T-179), so that lane is unchanged; at 149, a(149) supersedes it.
cfcheck: run here on intervals 1 and 34, it passed every structural check and the 2,909 leaves we sampled, with three mutations refused (E-wand125-closed-form-cfcheck-sample, confirmed). A sample sets no rung.
Next, for C3: the full replay of the 136 records by replay4d, which you price at 4,294 CPU-hours. It waits for the owner's compute budget, and this issue stays open to track it.

Your other reports of 13 October are T-176 to T-179, the lower bounds at 39, 44, 37 and 145 to 149, each V0/C1, their replays also waiting on an owner compute budget.

Evidence: E-wand125-closed-form-report (reviewed), E-wand125-closed-form-cfcheck-report (recorded) and E-wand125-closed-form-cfcheck-sample (confirmed). On main: RESULTS.md, the packet.

Generated by Claude Code

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

@wand125

@wand125, where this request stands in the record on main.

Corrections to earlier replies.

The reply of 2026-10-14 (Closed-form lower bound s(N) ≥ a(N) for every non-square N ≥ 49, above the register for 156 n in 104–319: registration request #600 (comment)) gave E-wand125-closed-form-cfcheck-sample as confirmed; it now reads recorded.
The same reply said T-180 is at V0 because no record had been replayed here. Two of the 136 records have since been replayed here as a calibration, REPLAY OK, at about 1.22 times the source's CPU time; as a sample this moves no rung, and T-180 stays V0/C1.

What is registered.

s(N) >= a(N) for every non-square N >= 49, a(N) the closed form of SPEC.md on 34 intervals:
- T-180, reviewed: its argument has been read here and no blocking defect found, and no replay here has passed yet (V0/C1).
- E-wand125-closed-form-cfcheck-sample, recorded as evidence (verified, replayed-here): a sample, 2,909 of 187,183,108 leaves of the closed-form certificate, replayed here, which decides those and confirms nothing beyond them.
- E-wand125-closed-form-replay4d-sample, recorded as evidence (verified, replayed-here): a sample, 2 of 136 region records of the closed-form certificate, replayed here, which decides those and confirms nothing beyond them.

What is still queued, and how it will be completed.

T-180: C3 needs a complete replay of all 136 records by replay4d from the retained crates, built with the locked Cargo.lock, with the structure check, two mutated records refused and a review that reads the replay; the source prices it at 4,294 CPU-hours, and a calibration here at about 5,250 on this host. It is held over the owner's 40 CPU-hour cap for each validation item. The source's second checker, cfcheck, written from SPEC.md and sharing no code with replay4d (E-wand125-closed-form-cfcheck-report), has checked intervals 1 and 34 of the 34; a complete replay of all 136 records by it would be a second route at a higher level, priced at about 9,900 worker-hours.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-14-wand125-closed-form-lower-bound.md, packing/frontier/STATUS.md.

This issue stays open while anything above is queued, and a reply follows each change in the record.

Generated by Claude Code

wand125 closed form: retain replay4d 0.1.1 (1c661b7) and recompute it…

requests and credits: jlevy#600's follow-up, the jlevy#542/jlevy#543 …

Where this request stands in the record on main.

What is registered.

s(N) >= a(N) for every non-square N >= 49, a(N) the closed form of SPEC.md on 34 intervals:
- T-180, reviewed: its argument has been read here and no blocking defect found, and no replay here has passed yet (V0/C1). On the frontier it is current: a bound of its case records, verified or reported, rests on it now.
- E-wand125-closed-form-cfcheck-sample, recorded as evidence (verified, replayed-here): a sample, 2,909 of 187,183,108 leaves of the closed-form certificate, replayed here, which decides those and confirms nothing beyond them.
- E-wand125-closed-form-replay4d-sample, recorded as evidence (verified, replayed-here): a sample, 2 of 136 region records of the closed-form certificate, replayed here, which decides those and confirms nothing beyond them.

What remains, and which beads own it.

T-180: C3 needs a complete replay of all 136 records by replay4d from the retained crates, built with the locked Cargo.lock, with the structure check, two mutated records refused and a review that reads the replay; the source prices it at 4,294 CPU-hours, and a calibration here at about 5,250 on this host. It is held over the owner's 40 CPU-hour cap for each validation item. The source's second checker, cfcheck, written from SPEC.md and sharing no code with replay4d (E-wand125-closed-form-cfcheck-report), has checked intervals 1 and 34 of the 34; a complete replay of all 136 records by it would be a second route at a higher level, priced at about 9,900 worker-hours. Owned by think-wu73 and think-o4kf.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-14-wand125-closed-form-lower-bound.md, packing/frontier/STATUS.md.

Nothing you asked for is queued, so this issue is closed with this comment. Closing it confirms nothing above that is still open: each entry stands at the rungs given, what remains of its validation is owned by think-wu73 and think-o4kf, and a follow-up will be posted on this issue whenever an id, a rung, a status or a position above changes.

Generated by Claude Code

Navigation Menu

Repository navigation

Closed-form lower bound s(N) ≥ a(N) for every non-square N ≥ 49, above the register for 156 n in 104–319: registration request #600

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Closed-form lower bound s(N) ≥ a(N) for every non-square N ≥ 49, above the register for 156 n in 104–319: registration request #600

Description

Activity

jlevy commented on Oct 14, 2026

wand125 commented on Oct 14, 2026

jlevy commented on Oct 14, 2026

jlevy commented on Oct 14, 2026

jlevy commented on Oct 15, 2026

jlevy commented on Oct 26, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions