Skip to content

s(153) ≤ 12.870013850408: registration request #504

New issue
New issue
Closed
Closed
s(153) ≤ 12.870013850408: registration request#504
Labels
intakeTracking intake (saving, validation, tabulation, credits) of new results

Description

@BuddenPing
BuddenPing
opened on Oct 11, 2026

Certificate refinement — 12 October 2026

Please re-verify and update T-148 using the smaller exact certificate below. The original accepted submission is preserved after this update. This refinement is awaiting maintainer review; the original acceptance applies to the earlier certificate.

  • Previous accepted exact side: 6435006925203522001385040447/500000000000000000000000000 = 12.870013850407044002770080894.
  • Refined exact side: 3217503462601758500692520223/250000000000000000000000000 = 12.870013850407034002770080892.
  • Exact reduction: 5000000000001/500000000000000000000000000 = 1.0000000000002E-14.
  • Safe upward-rounded bound: s(153) ≤ 12.870013850408.

The existing A=C return, rational orientations and guard 5000000000001/5000000000000 are unchanged. The finite centre/side realization is tighter; some free centres move substantially. The upward-rounded twelve-decimal bound is unchanged.

Pinned evidence and reproduction

Extract the package, enter n153-squares-project, and run python3 VERIFY.py with Python 3.10+ (standard library; without -O). The package checks its hashes, all 153 squares, 612 wall constraints and 11628 unordered pairs using three exact implementations, the recorded rational construction/owner replay, native conversion identity, and deliberately invalid controls. Both unchanged Squares Project verifiers at 074ac28d4ceb9a1897303f936d794771cfc6a7bd also pass; source, licenses and fresh receipts are included. These are implementation-level checks, not independent human audits or an optimality proof.

SHA-256:

2a0e1affdd82cf613af58cfed03fad41b68a5392ae1de34450578c590ced6121  n153-squares-project.zip
1ca754f0238f958597ecddc645aa16f5c44c3afc9cf2614b40ce2fd1f6dea670  n153.cert.json
7cc142202fc39acfdd01060a6f89744a3f5815d6f193f03dfdb14d8c1f5c3567  pingyou-n153-rational.yaml

Construction and refinement credit: PingYou Ltd. The underlying N70 construction credit remains Ryan Xu; the retained exact N70 source and checking-tool credits remain Evan Daniel. The earlier comparison construction is by Nate Chaoweeraprasit (SQUISH). Upstream software/schema credits and licenses are retained in the package.

Original accepted submission (T-148)

Claim. Please register the following exact feasible upper bound for 153 congruent unit squares:

s(153) ≤ 6435006925203522001385040447/500000000000000000000000000
       = 12.870013850407044002770080894
       < 12.870013850408.

The final display is rounded upward. The certificate includes the exact centre/container dilation 5000000000001/5000000000000; every small square still has side exactly 1.

The strongest prior exact certificate located on 11 October 2026 is Evan Daniel's regularization of the SQUISH N153 packing, registered as T-146:

402250932783786874180075932249/31250000000000000000000000000
= 12.872029849081179973762429831968.

The exact side reduction is 0.002015998674135970992348937968, approximately 0.015662%. T-146 is registered at V3/C3 but awaits adoption into the N153 case page; this comparison includes that stronger certificate rather than the older case-page ceiling. No local or global optimality is claimed.

Certificate. The complete release is pinned at commit bc328a7d727aedd0eabebd6ea80285f572b65d2d in BuddenPing/square-packing-certificates.

The certificate and PDF are published unchanged byte-for-byte; evidence/document-binding.json records their hashes, and evidence/PROVENANCE.txt maps the historical source-path labels. The PDF retains its original pre-submission status caption. All published files were fetched back from the pinned revision and checked against the local release.

The JSON gives rational centre/half-angle triples [x,y,t], with (cos θ,sin θ)=((1−t²)/(1+t²),2t/(1+t²)), and the exact container side. The package retains the construction table, source/control packings, both prior N153 certificates, replay scripts and receipts.

Checking. Extract the archive, enter n153-squares-project, and run:

python3 VERIFY.py
python3 evidence/reproduce.py
python3 native/convert_witness.py evidence/packing.cert.json native/pingyou-n153-rational.yaml --check

These checks use exact rational arithmetic and need Python 3.10+ with its standard library. Run without -O. The construction replay reproduces every centre, orientation and the guard exactly. Vertex projections, centre/support-radius separating axes, and rational polygon clipping accept all 153 unit squares, 11,628 unordered pairs and every wall. The source/control packings and prior certificates also pass the three geometric checks. The native conversion is checked against the exact source geometry.

For the Squares Project's own verifier, from the pinned checkout's packing/ directory:

uv run --frozen packing-witness verify /path/to/pingyou-n153-rational.yaml --json
uv run --frozen python /path/to/native/replay_upstream.py --checkout .. --witness /path/to/native/pingyou-n153-rational.yaml

Both unchanged implementations at commit 5b0eb012e09b48b5044aacb439b4cfacf38935f5 passed all 153 squares and 11,628 pairs: sqpack.witness.exact_verify in 1.89 seconds and devtools.check_rational_witness_independent in 0.89 seconds. Both report minimum wall clearance 1/10000000000000 and positive minimum pair separation of approximately 1.8858260897e-13. native/native-replay.json records the exact results, source revision and timings; native/upstream-source-manifest.json pins the used source files. The recorded runs invoked the unchanged verifier functions; a full repository test suite was not run.

What the checkers share. All use the same rational geometry. The separating-axis implementations share that mathematical criterion; polygon clipping supplies a different geometric test. The construction replay and conversion checks are additional checks of representation identity, not independent proofs of optimality. No symmetry reduction omits any pair. These checks are not independent human audits.

Not done. The release does not prove optimality, improve a lower bound, or certify that the undilated algebraic contact solution is feasible. Replay starts from the supplied explicit rational construction table; it does not repeat the exploratory owner selection or floating linear solve. The degree-seven equation described in the construction notes explains the chosen design parameter; the stated bound rests on the full rational witness. The public comparison is dated and cannot exclude unpublished work.

Lineage and credit. Please credit PingYou Ltd for the new N153 construction. Its starting geometry is Ryan Xu's N70 packing, announced in #432, retained through Evan Daniel's pinned exact N70 certificate. The construction develops the boundary-patch approach used in our N207 result, #503, by changing which complete squares and contact constraints survive, then reclosing the contact pattern at a new angle. It contains 121 upright squares and two tilted populations of 17 and 15.

Credit for the previous N153 packing remains with Nate Chaoweeraprasit (SQUISH), #481, and for its refined exact certificate with Evan Daniel. Source, refinement, and software credits remain in the package; no claim is made to invent N70 or patch composition in general.

Activity

  1. jlevy commented on Oct 11, 2026

    @jlevy
    jlevy
    on Oct 11, 2026
    Owner

    @BuddenPing thanks! agents will validate/follow up!

  2. jlevy
    added 3 commits that reference this issue on Oct 12, 2026

    intake: register PingYou Ltd's #503 and #504 as T-147 and T-148 at V3/C3

    3c9dd26

    release: re-pin DATA_REVISION to 3c9dd26

    640b3cf

    rollups: the lanes behind layer 2 (#503, #504, #501, #505 imports, re…

    6d67212
  3. jlevy
    added
    intakeTracking intake (saving, validation, tabulation, credits) of new results
    on Oct 12, 2026
  4. jlevy
    added 3 commits that reference this issue on Oct 12, 2026

    merge: main at ad00d7f into the imports layer

    f5488ef

    integrity-ceremony: name the download boundary's class, not its issues

    4c9acae

    Merge pull request #516 from jlevy/claude/wizardly-meitner-wqn4x3-imp…

    4a49105

  5. jlevy commented on Oct 12, 2026

    @jlevy
    jlevy
    on Oct 12, 2026
    Owner

    @BuddenPing, thank you again. Your n = 153 certificate is registered on main through #516, and it is confirmed:

    • T-148, V3/C3: s(153) ≤ 6435006925203522001385040447/500000000000000000000000000 = 12.870013850407044002770080894, the exact fraction your issue prints.

    It is 9.67e-03 below the ceiling the case record holds, T-127 (Nate Chaoweeraprasit's packing as improved by Siddharth Gupta). It is below Evan Daniel's pending T-146 by exactly 0.002015998674135970992348937968, the figure your issue gives, and below SQUISH's pending T-136 by 2.02e-03. It is the smallest side the register holds at 153.

    How it was confirmed. It was re-verified here by an independent implementation. Your three checkers, reconstruction, conversion and SymPy derivation did not run here.

    • Both maintained exact routes, sqpack.verify and devtools.check_rational_witness_independent, decided the certificate again, with a duplicate-square and an outside-container control, and matched the retained rows.
    • A third exact route, devtools.check_half_angle_area (half-extent containment and exact intersection area), decided it with six controls. It also held the record's derived fact to n153.cert.json and pingyou-n153-rational.yaml fetched at bc328a7.
    • Your release ran the two maintained routes itself. The independence rests on their authorship, which predates your release, and on the third route, which you did not run.
    • A separately prompted AI review of 11 October accepted it for finite feasibility with no blocking defect. intake 2026-10-11 (2/6): #503, #504, #501, #505 replayed, reviewed and registered as T-147 to T-150 at V3/C3 #516 had two further reviews before it merged.
    • The record keeps your report as E-pingyou-504-certificate-report (reviewed) and this replay as E-pingyou-504-exact-feasibility (confirmed).

    Credit. The results table credits PingYou Ltd, after Xu, Daniel and Levy, the last for this project's checkers that your release ran. The n153 construction is yours. By your account it starts from Ryan Xu's n70 construction (#432), taken from Evan Daniel's exact n70 certificate, and its contacts are reclosed at a new angle. The record states that lineage as your account of the construction. Measured pose by pose, no placement of the n70 puts more than one of its squares exactly on a square of this packing, which fits contacts reclosed at a new angle.

    A question from the review. This issue and its release make no statement about AI assistance, and the issue omits the template's section on it. Your #503 release disclosed AI assistance and then removed the disclosure. Which account applies here? The question is asked on #503 as well, and one answer there that covers both issues is enough.

    What happens next. The case record at 153 still shows T-127. The adoption layer, #518, is in review; it adopts T-148 as the house at 153 and keeps the earlier house as history. A reply will follow when it merges. This is finite feasibility only: no optimality is registered, and V4/C4 would need a second adversarial review by a distinct reviewer and a human oversight record.

    Generated by Claude Code

  6. jlevy
    added a commit that references this issue on Oct 12, 2026

    Merge pull request #551 from jlevy/claude/wizardly-meitner-wqn4x3-rep…

    25de5a4

  7. jlevy commented on Oct 12, 2026

    @jlevy
    jlevy
    on Oct 12, 2026
    Owner

    @BuddenPing, thank you. As our reply of 12 October promised, here is the follow-up: the case-record adoption (#518) has merged, and T-148, V3/C3, confirmed, is now the house of the n = 153 case, s(153) ≤ 12.8700138504070441. Siddharth Gupta's refinement of SQUISH's packing (T-127), the earlier house, stays there as history.

    Still open: the AI-assistance question, asked on #503; one answer there covers both issues, and it is still read into the record after the issues close.

    Closing as integrated.

    Generated by Claude Code

  8. jlevy
    closed this as completedon Oct 12, 2026
  9. jlevy
    added a commit that references this issue on Oct 12, 2026

    records: #506's reply against think-9fjl's plan, and the AI question …

    1f6d9b6

  10. BuddenPing commented on Oct 12, 2026

    @BuddenPing
    BuddenPing
    on Oct 12, 2026
    Author

    A refined certificate for the same N153 construction is now published. Please re-verify it and update T-148 if accepted.

    Exact side: 3217503462601758500692520223/250000000000000000000000000 = 12.870013850407034002770080892. This reduces the previously accepted side by 1.0000000000002E-14; the safe reporting bound is s(153) ≤ 12.870013850408.

    The existing A=C return, rational orientations and guard 5000000000001/5000000000000 are unchanged. The finite centre/side realization is tighter; some free centres move substantially. The upward-rounded twelve-decimal bound is unchanged.

    The pinned portable package, native witness, checksums, and updated comparison are linked in the dated update at the top of this issue. All three exact geometry checks and both unchanged native verifiers pass; construction replay and invalid-input controls are included.

    Construction and refinement: PingYou Ltd, with the original Ryan Xu, Evan Daniel, SQUISH and upstream software credits preserved. The original acceptance history remains intact; the refinement awaits review.

  11. jlevy commented on Oct 14, 2026

    @jlevy
    jlevy
    on Oct 14, 2026
    Owner

    @BuddenPing, the thank-you for your AI-assistance answer is on #503, and it covers this issue too. T-148 now carries your statement. We are replaying your refined N153 certificate above, and we will report back here.

    Generated by Claude Code

  12. jlevy commented on Oct 14, 2026

    @jlevy
    jlevy
    on Oct 14, 2026
    Owner

    @BuddenPing, following up on the comment above: your refined N153 certificate (pinned at 431186b, n153.cert.json, SHA-256 1ca754f0…) replayed and passed both of our exact checkers, and both refused the two controls. It is the same packing as your earlier n153 entry with two squares moved, and 1.0e-14 below that entry, as you state. We retain it as derived exact facts beside the earlier one, which keeps its own claim. Registration comes next. PR #574 states further n153 certificates; it is a separate import.

    Generated by Claude Code

  13. jlevy
    added 2 commits that reference this issue on Oct 14, 2026

    records: the #503 thank-you and the #504 pointer of 14 October (think…

    eeafde7

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

    60e5ffa

  14. jlevy commented on Oct 14, 2026

    @jlevy
    jlevy
    on Oct 14, 2026
    Owner

    @BuddenPing, thank you. With #602 merged, your refined N153 certificate is registered on main:

    Evidence: E-pingyou-504-refinement-report (your report, recorded). On main: RESULTS.md, the packet.

    Generated by Claude Code

  15. jlevy
    added a commit that references this issue on Oct 14, 2026

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

    38775ff
  16. BuddenPing
    added 4 commits that reference this issue on Oct 15, 2026

    render: the synopsis glance rows after the significance confirmation …

    3fa57fe

    intake: retain and replay PingYou Ltd's seven certificates of 12 October

    6801238

    merge: the PingYou intake lane of 14 October (jlevy#564, jlevy#566-jl…

    02dac55

    records: the 14 October reviews raise T-161 to T-175 and T-181 to T-1…

    fd717f2

  17. jlevy commented on Oct 15, 2026

    @jlevy
    jlevy
    on Oct 15, 2026
    Owner

    @BuddenPing, thank you. Where this request stands in the record on main.

    Corrections to earlier replies.

    What is registered.

    • s(153) <= 6435006925203522001385040447/500000000000000000000000000 = 12.870013850407044002770080894, by n153.cert.json (SHA-256 31b3fb3cba73528fab21d085a34f3209684a868e7116059ea5c21e664bca1ff2) and its corners Witness/v2 pingyou-n153-rational.yaml (SHA-256 963d6ca7cce053e7ff22baf6438bdf5776b7b06d01e1509e654c73966b9e4d41):
      • T-148, confirmed at V3/C3: re-verified here by an independent implementation (sqpack.verify, run by each case's verify_exact module and the packing-witness command, devtools.check_rational_witness_independent, devtools.evand_arrangement_reports, devtools.upper_bound_reports, devtools.check_half_angle_area, devtools.evand_exact_certificates).
      • E-pingyou-504-exact-feasibility, confirmed here: re-verified here by an independent implementation (sqpack.verify, run by each case's verify_exact module and the packing-witness command, devtools.check_rational_witness_independent, devtools.evand_arrangement_reports, devtools.upper_bound_reports, devtools.check_half_angle_area, devtools.evand_exact_certificates).
    • A refined certificate for the same n153 construction, 1.0e-14 below the earlier one:
      • T-166, confirmed at V3/C3: re-verified here by an independent implementation (sqpack.verify, run by each case's verify_exact module and the packing-witness command, devtools.check_rational_witness_independent, devtools.evand_arrangement_reports, devtools.upper_bound_reports, devtools.check_half_angle_area, devtools.evand_exact_certificates).

    On the case page. Our reply of 14 October said T-148 still held the case at 153. It was the house at 153 from 11 to 15 October 2026. On 15 October the case adopted Mykhailo Polkovskyi's arrangement of your n = 153 design (T-173, #573), 2.56e-12 below T-148 and 2.55e-12 below T-166. T-148 stays retained as history; T-166 is registered and confirmed, and is not the house.

    On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-11-upper-bound-imports-503-504.md, packing/frontier/n-153.md, docs/project/reviews/review-2026-10-14-upper-bound-imports-561-593.md.

    The issue stays closed; this brings what the record says up to date.

    Generated by Claude Code

  18. jlevy
    added 2 commits that reference this issue on Oct 15, 2026

    fix(records): #613 is not a counterexample report; #622 notes its AI-…

    f04a38e

    Merge pull request #630 from jlevy/claude/ecstatic-edison-8en33t-repl…

    9f0c1aa
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    intakeTracking intake (saving, validation, tabulation, credits) of new results

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions