The Program at a Glance

The Program at a Glance

$s(n)$$s(n)$ is the side of the smallest square that contains $n$$n$ non-overlapping unit squares, which may be rotated freely. The program covers every $n$$n$ and goes into most depth where there is recent progress; $n=11$$n=11$, a central case, is now solved at Walter Trump’s exact algebraic side.

This project works under four independent principles, defined at the top level in README.md: Correctness (Soundness) owns mathematical truth and may veto promotion; Process (Discipline) owns reproducible research operations and adds only the controls needed to preserve consequential evidence and handoffs; Insight (Creativity) owns hypotheses and strategy but cannot certify them; and Efficiency (Infrastructure) owns stable, measured throughput without relaxing mathematical assurance. These are quality dimensions, not session types. Routine work chooses a workflow and bounded output; a versioned multi-phase session also declares one primary focus per phase while the other principles continue to constrain and contribute to the work.

Those principles govern four capabilities built so far:

1. Know the frontier. A schema-validated reported and formal claim register for every $n\le 324$$n\le 324$, reconciled against a dated named-source inventory, with a generated reader-first status view and a local archive of the primary literature.
2. Inspect, check, and verify witnesses. One interchange accepts supported decimal, rational, and algebraic geometry. Decimal data can be inspected or numerically checked under explicit arithmetic; rational and certified algebraic witnesses can be verified exactly, including field irreducibility and unique-root preconditions.
3. Search, under an experiment contract. A hypothesis registry with kill criteria written before the run, a metric vector, an accept rule, a declared timebox, and a ledger generated from the artifacts rather than typed.
4. Account for what goes wrong. A defect log with the same discipline as the experiment record, because most soundness failures found so far pointed in the flattering direction and none was caught by the automated gate.

Capability 2 has two promotion boundaries. Robust rational promotion is built for suitable decimal center-angle poses and may prove a slightly weaker upper bound by making its side relaxation explicit. A generic path that infers contacts and certifies an exact solution at the reported value is built as generic library components but is not exposed as an arbitrary Witness/v2 command; certification may still fail for singular, ambiguous, or ill-conditioned systems. What Is Built states, component by component, what runs, what its output may claim, and what remains engineering or mathematics. Read it before citing any capability here.

Results and their significance

The core exposition begins with T-018’s visual proof of $s(11)\ge 3.81$$s(11)\ge 3.81$, then explains the threshold charges and dilation argument that strengthen it. T-026 established the earlier first-party bound s(11)≥955000⋅518400042893309449​/179696714646249=3.8264474…$s(11)\ge 955000·\sqrt{518400042893309449}/179696714646249=3.8264474\dots$ at V3/C3. T-033 tightens the same retained family to s(11)≥955000⋅2073600042893309449​/359341754646249=3.8269975…$s(11)\ge 955000·\sqrt{2073600042893309449}/359341754646249=3.8269975\dots$ at V3/C3. The exact value is now $s(11)=T=3.877083590022814\dots$$s(11)=T=3.877083590022814\dots$: T-060’s independently replayed global lower bound matches T-011’s exact Trump witness. Kleddamag’s $s(11)>31/8=3.875$$s(11)>31/8=3.875$ remains the earlier verified T-037 bound, and Wang and Li’s scaling of its certificate, $s(11)>3875000000/999999999$$s(11)>3875000000/999999999$ (T-061), a later historical one. Future research follows the payoff policy: prioritize substantial bound improvements and methods or theorems that make them possible.

The September 22 external intake verifies Kleddamag’s stronger $s(11)>3.875$$s(11)>3.875$ bound and Tokoharu’s rectangle-density certificates at $s(26)\ge 5.508$$s(26)\ge 5.508$ and $s(29)\ge 5.71$$s(29)\ge 5.71$, with pinned sources, mathematical reviews and complete replays. These now supply the verified Frontier bounds; the records retain literal source reports and state the verification methods separately. The complete native n11 decision adds a distinct interval coverage method for Kleddamag’s strict $3.875$$3.875$ bound (T-037, V3/C3), with no new bound. Part II of the n = 11 series explains that proof and what it inherits. The R052 review of 25 September verifies Guzhou0806’s strict $s(17)>231001/50000=4.62002$$s(17)>231001/50000=4.62002$, built with AI assistance on Kleddamag’s v1.0.0 mixed point/threshold architecture, at V3/C3. All four of the source’s replay modes pass here, but both full sweeps are one event-cell method and the native interval route refuses the certificate at its engine ceilings, so there is no method-distinct decision. It supplied the verified Frontier bound for $n=17$$n=17$ from 25 to 27 September, about $0.000229$$0.000229$ above Kleddamag’s $461300/99853$$461300/99853$. Kleddamag’s v1.1.0 of 26 September then proved $s(17)>232001/50000=4.64002$$s(17)>232001/50000=4.64002$, exactly $0.02$$0.02$ above R052, on the same author’s architecture extended with weighted thresholds and pairwise-intersecting winning-subset rules. Both of its complete checkers pass here and agree on all 2,048 intervals, with a counting surplus of 5,629 units of 10−9${10}^{-9}$; they share one event-cell method, and the native parent-core route cannot yet represent the new features, so it is V3/C3, and its proof review is a separate record. It supplied the verified Frontier bound for $n=17$$n=17$ on 27 September. The same day $s(17)>466001/100000=4.66001$$s(17)>466001/100000=4.66001$ followed, $0.01999$$0.01999$ above it: Kleddamag, building on Squares Project (Joshua Levy), Mira and Guzhou0806, an exact weighted-certificate proof over 2,168 orientation intervals on the same two checkers. Both pass here and agree on every interval, with a counting surplus of 54,340 units of 10−9${10}^{-9}$, again at V3/C3. It supplied the verified Frontier bound for $n=17$$n=17$ from 27 to 29 September; its proof review is a separate record. Guzhou0806’s R068 of 28 September, continuing that charge with one added four-site point orbit over 4,991 intervals, proves $s(17)>116511/25000=4.66044$$s(17)>116511/25000=4.66044$, exactly $0.00043$$0.00043$ higher; its two checkers’ complete replays pass here and agree with the published ledgers, at V3/C3, and it supplied the verified bound until 5 October (review). R067, $233009/50000$$233009/50000$, was replayed beside it. Guzhou0806’s R071 of 30 September keeps R068’s charge and rebuilds its cores over 5,114 intervals for $s(17)>18641771/4000000=4.66044275$$s(17)>18641771/4000000=4.66044275$, $11/4000000$$11/4000000$ higher; its complete replay passed here on 5 October at V3/C3, and it supplies the verified bound now, $0.0151$$0.0151$ below Bidwell’s packing (review). Each now has an entry in the results register (T-038 to T-043, and T-093), which since 29 September 2026 holds every result by others that this record acts on, with the source’s credit beside this repository’s V and C.

The same intake took in three more sources. Evan Daniel’s evand/square-packing, building on Sam Burns’s and Gustavo Massaccesi’s weighted exact-rational covering method, proves $s(32)=6$$s(32)=6$ by a zero-margin weighted closed cover of [0,6]2$[0,6{]}^2$, at V3/C3 on complete replays here of its exact checker and its binary64-enclosure zmx2, which share their author, point test and symmetry fold and differ in how they close germs, and $s(12)\ge 15680/3951$$s(12)\ge 15680/3951$ at V3/C3; its $s(21)\ge 5000/1001$$s(21)\ge 5000/1001$ was superseded by the same author’s mixed covers of 27 September, weighted points plus mass on interior grid-line segments, which prove $s(21)=5$$s(21)=5$ and $s(45)=7$$s(45)=7$, both V3/C3. Its case-free proof of Bentz’s $s(13)=4$$s(13)=4$ was kernel-checked in Lean here on 30 September and is recorded under T-006. wand125’s rectangle-density certificates, 44 as of 27 September, 50 standing as of 28 September and raised again on 1 October for $n=18$$n=18$ to $95$$95$, built with Tokoharu’s solver and decided by Tokoharu’s reviewed interval verifier, are verified by complete replays here at 37 counts (T-045, T-070, T-074) and reported at the others until their replays run. wand125’s point-only routes to $s(21)=5$$s(21)=5$ and $s(45)=7$$s(45)=7$, both verified here as second certificates, and its $s(50)\ge 37/5$$s(50)\ge 37/5$, verified here by a complete replay, followed on 28 September. Guzhou0806’s continuation of R052, $s(17)>4.62003$$s(17)>4.62003$, superseded by v1.1.0, is retained as a publication record. The results register and the site’s results table give the credit for each. The rungs above are the register’s, under the ladder in force since 2026-09-30. Dated sections further down keep the rungs they were written with; epistemics.md says how the two ladders correspond.

Every result this project has registered, in the reading order its significance scores set. The full claims, the rationale behind each score, and the next evidence-improving action for each are in frontier/RESULTS.md; the V, C and S axes are defined in epistemics.md.

Research Program Status and Roadmap

This is the current repository-wide roll-up. The enforced records own the facts: agenda and commitment state lives in the agenda records, session accounting in the session records, and exploration state in the exploration records. The agenda-map.md and session-close-report.yaml are generated views of those sources, the generated ledger derives hypothesis status and summarizes experiment verdicts, and the frontier register owns promoted results.

The agendas divide into six practical eras. Agendas 001–010 built the campaign record, controls, constructive search, and first exact-promotion machinery. Agendas 011–017 made verification and result disposition routine. Agendas 018–023 tested scaling, restricted covering programs, and the validation loop. Agendas 024–028 built on the $3.81$$3.81$ result with adaptive and structural routes. Agendas 029–033 and 035 developed conditional-owner geometry, T-025/T-026, and the now-paused incremental follow-ups. Agenda 036 is the strategy-reset queue, and Agenda 037 is the relational-certificate queue opened by the overnight review, and Agenda 040 is the current overnight lower-bound queue opened by Session 143’s review. The generated agenda map, not this narrative, summarizes commitment state.

Session 143 is the latest terminal closeout: its four research lanes and three adversarial reviews produced X-040, registered H-222 to H-231, opened agenda-040, corrected the Bentz 2016 transcription (D-505, D-506), and selected BC-361 under think-pogj as the next entry; no bound moved. Session 142 is the preceding terminal closeout: its correctness review replayed all four retained n=18 certificates, repaired the stack in PR 202, and preserved think-qqzs as the next entry. The corrected code passed the full checkpoint; unchanged lower PR heads remain independently unready. Session 141 closed the preceding research pass: T-029 retained $s(18)\ge 1871/400$$s(18)\ge 1871/400$, T-030 retained $s(18)\ge 4679/1000$$s(18)\ge 4679/1000$, H-218 and H-220 stay unconfirmed, and think-qqzs remained the next entry. Session 140 closed the stacked-PR survey of $n\le 100$$n\le 100$ lower bounds; it retained T-028 $s(18)\ge 187/40$$s(18)\ge 187/40$ and does not confirm H-218. Session 139 retained T-027 $s(18)\ge 467/100$$s(18)\ge 467/100$ after encode-only timed out unresolved. Session 138 is the preceding route-selection handoff: PR 193 merged its records as 4ad98e90, think-4woh is closed, and certification debt now sits under think-qqzs. The five X-037 owner decisions are resolved under epistemics.md. stopped is not a scientific failure; it includes time limits, guarded refusals, administrative handoffs, and work deliberately ended after its next evidence was identified. The late-session arc moved from certificate production and exact dilation through owner geometry and bounded negative tests, then through the T-025/T-026 publication stack, research-state reconciliation, the CI-efficiency block, and the overnight n=11 route review. Use the generated close report for individual session clocks and never add child-session resource totals to their parent roll-up.

The exploration namespace has deliberate gaps; an absent identifier is not a missing report. Some explorations link forward through proposes, while others remain uncodified observations or strategy notes. The most consequential recent synthesis is X-027’s ceiling for pure point/density certificates, followed by X-028’s strategy portfolio and the scoped BC303 drafts X-029–X-031, followed by X-032’s no-target Route S compression contract and X-037’s ranked relational-certificate slate. A draft or proposed direction is not a registered hypothesis, and a registered hypothesis is not a frontier result.

The exact value is now $s(11)=T=3.877083590022814\dots$$s(11)=T=3.877083590022814\dots$ by T-060 and T-011. Session 152 fully replayed and mathematically reviewed Kleddamag’s earlier external certificate, which closed 95.89% of the gap from T-026 to the Trump upper bound; Wang and Li’s scaling of it (T-061) then added 3.9×10−9$3.9\times {10}^{-9}$. Session 153 independently certifies every one of the 12,028 parent-angle intervals by directed-rounding box coverage, with no stalled or exhausted boxes. The event-sweep replay remains C3 by itself; the complete native decision and reviewed transfer theorem provide method-distinct C4 confirmation of the strict bound. Research on $s(11)$$s(11)$ lower bounds is now method development only: T-060 settles the value. The pure point/density ceiling $38200/9977\approx 3.8288$$38200/9977\approx 3.8288$ lies only about $0.00236$$0.00236$ above T-026, so additional heavy work for microscopic gains in that language is paused. T-033 remains the controlled first-party net-refinement result: it moved T-026 by $0.00055013825660$$0.00055013825660$, but the unchanged family’s ceiling $955000/249507\approx 3.82755$$955000/249507\approx 3.82755$ is already below $3.875$$3.875$ and cannot improve the current global bound. Changed weights, sites, parent domains, or charge atoms remain separate hypotheses. H-160/exp-158 and H-162/exp-160 are registered but blocked before target invocation. H-163 is registered and unresolved via exp-161; its target-blind instrument merged in PR 182. Encode-only timed out with no JSON. --search did not run. think-ufmk registered that experiment; a scientific target still requires the live --check, --authorize-target exp-161, and a coverage-encoding search that is not an admission-control manifest. The retained source and control work carries no scientific verdict.

BC-339’s W7 pipeline-improvement and W8 reconciliation are complete and certified. BC-347’s source-bound Astra Max mathematical audit and roadmap integration are also complete and certified; they ran no scientific target and changed no frontier claim. BC-346’s W10 route-selection review is certified and selected the due BC-340 efficiency checkpoint. BC-340 is now complete: VE-005 removed repeated whole-corpus parsing from the branch cost rollup behind an exactly-once load guard and unchanged-output checks. Its three alternating local pairs reduced the rollup’s median from 47.72 to 2.31 seconds, and the first candidate hosted checks tier passed in 106.38 seconds against the unchanged 195-second ceiling. This is validation evidence, not new mathematics. BC-355 / think-97we reconciled the later Pages, Packing, budgeting, and validation-lane work into one exact-head topology. Session 136 stopped after the implementation handoff and Session 137 recovered it; PR 188 merged as 042e791c and PR 185 merged as d7f9d94d, and think-97we is closed. What that closure did not carry is the 180-second hosted wall: by owner decision the pull-request walls are advisory under the open think-g4n9 until they hold on hosted runners, so BC-355’s agenda cell still records in_progress. The block ran no scientific target and changed no theorem, hypothesis verdict, n=11 bound, or frontier record. The order as it stood before T-060 settled $s(11)$$s(11)$, kept as a record, was:

1. BC-361 / think-pogj is the active block, opened by Session 143’s review in agenda-040. Session 144 decides H-223, H-224, and H-225 on the stock instruments under exp-213 to exp-215, with the BC-362 Bentz 2016 replay lane beside it. BC-357 / think-qqzs stays the registered n=6 calibration entry in agenda-037: it closes M7’s n=6 point bracket at 299/100 after the G5 site-merge fix and can fill an idle slot.
2. BC-354 / think-0t5y stopped at Route A’s representation boundary. Its source inventories found no complete 80-stratum negative-root producer, matched exact baseline, conditional gate, or method-distinct replay. No target ran and no physical root closed.
3. BC-343 remains the standing Route S commitment; think-ufmk is its sole scientific entry, on a fresh planning branch. X-032 and H-163 freeze T-025 as the sole matched control, its exact 119-orbit support universe, and the at-most-23 positive-orbit criterion. T-026 is only a support-and-rescaling sentinel. Session 134’s source-distinct review refused the first admission checkpoint. Session 135 then discharged all four retained guards: complete source contents bound to a declared Git revision and repository-relative paths, both T-026 sentinels, a canonical selection-manifest boundary, and the complete X-032 mutation matrix. Its source-distinct re-audit returned ADMIT after one symlink-alias boundary repair. PR 182 merged the instrument as 1d9c49c4 from reviewed head 609d7d62 after exact-head validation. Session 139 registered exp-161 and landed the named producer, which emits no candidate. Encode-only timed out unresolved. --search did not run.
4. Treat A, S, global angular resources, and B as the first advisory tier. A is the strongest route to a material $n=11$$n=11$ lower bound; S is the best bounded deliverable; angular resources offer a cheap optimal-face screen; and B is the strongest alternative mechanism after its soundness controls.
5. Retain stronger charge algebra, geometry-dependent budgets, an $n=12$$n=12$ exact-value program, and orientation structure as second-tier candidates whose first blocks must pay for missing premises.
6. Keep constructive search separately budgeted after an oblique proposer control, and treat geometric waste accounting as a speculative candidate requiring both a local lemma and a non-double-counting global rule.

The detailed six-hour execution schedule originally allocated five sequential merge-bounded blocks. BC-354 activated that schedule’s guard-refusal branch, so the Route A discriminator no longer follows it. BC-343’s no-target Route S instrument is admitted and merged. Its remaining Route S path is the think-ufmk planning block, which registered exp-161; the named producer exists and emits no candidate. Encode-only timed out unresolved. A later encode still needs a live --check and --authorize-target exp-161 before --search; agenda-037’s relational-certificate queue now runs ahead of it. Each block starts from the preceding merge on a fresh branch and gets its own session, bead disposition, validation receipt, and pull request.

The audit’s linear advisory order is A, S, angular resources, B, stronger charge algebra, geometry-dependent budgets, $n=12$$n=12$, C, D, then geometric waste. That is a readiness-and-information judgment, not a measured probability of success or an execution decision.

The W8 documentation-pass runbook defines the cutoff, source precedence, counting rules, conflict handling, and validation needed to refresh this section. Together, packing-ledger check and devtools.check_synopsis derive every row in the marked table from its owning artifacts and checked generated views, so a later source change cannot leave a plausible but stale total here.

The roll-up and audit source checkpoint fa6363b6c2b4c7d7449807c04166e9df94bc7b35 passed the complete 63-step fast surface at the declared four-CPU reference shape in 459.37 seconds. The following closeout changes only record that gate, advance lifecycle state, and regenerate derived views; pull-request CI independently validates the resulting tree.

Current research readiness

The program has two promoted mathematical outputs: an exactly verified packing that improves an upper bound, or a proof certificate that improves a lower bound. Search, refinement, local geometry, component statistics, and visualization are instruments for producing those outputs. They do not inherit the status of a bound merely because they run or reveal structure.

The judgments below concern safe research use, not whether code exists. The detailed implementation statuses remain in What Is Built.

Its active confidence ladder has completed the exact and event controls up to the first nontrivial identity question; the next scientific transition is from specialized $n=5$$n=5$ local geometry to a defensible component relation, not to a larger raw census.

Refresh rule

Refresh this block whenever a layer’s admissibility or built state changes, the confidence-ladder head moves, or the numerical launch decision changes. Take counts and verdicts from the generated ledger, cell order from the confidence ladder, blockers from the defect log, and numeric go/no-go from the launch agenda. Do not copy a ready bead, dated throughput, or a candidate mathematical verdict into this table. Reconcile the table with What Is Built and Where This Stands, then run uv run --frozen python -m devtools.check_synopsis; the checker keeps the marked block attached to these canonical owners without freezing its wording.

The strategy that organises lanes 3 and 4 is stated in A Search Philosophy for Square Packing: a validated map of terminal components is the intended deliverable, and records are corollaries. The current endpoint map remains provisional while identity and local certification are unresolved. The argument for it, and the measurement registered to kill it if it is wrong, are in Theoretical Results and The Hypothesis Registry below.

Terminology below fixes both the work units—campaign, session, phase, slice, experiment, round, and run—and the mathematical terms used narrowly here. Those definitions apply in the campaign artifacts and the beads too, not only here.

Document Map

The validated document map distinguishes current rules and synthesis from supporting research, dated records, generated views, and transient plans. Follow the replacement link instead of using a superseded review or handoff for current status. Collection rows cover homogeneous typed artifacts without listing every case or experiment separately.