Synopsis: The s(n) Program

Date: 2026-10-01

Status: Living document, revised whenever a result lands.

Owns: The single technical account of what this project knows, how it knows it, and what it is doing next.

Evidence cutoff: Includes the independently audited T-060 global proof replay of 2026-09-30 and Session 165’s certified \(n = 17\)$n=17$ upper endpoint of 2026-10-01. Earlier record-state and validation revisions are retained in Session 128.

Every number here also appears in a schema-validated artifact in this repository, or is reproducible by a command given in the text, and the artifact is authoritative where the two differ. devtools.check_synopsis enforces that in the gate.

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) \ge 955000 \cdot \sqrt{518400042893309449}/179696714646249 = 3.8264474\ldots\)$s(11)\ge 955000·\sqrt{518400042893309449}/179696714646249=3.8264474\dots$ at V3/C3. T-033 tightens the same retained family to \(s(11) \ge 955000 \cdot \sqrt{2073600042893309449}/359341754646249 = 3.8269975\ldots\)$s(11)\ge 955000·\sqrt{2073600042893309449}/359341754646249=3.8269975\dots$ at V3/C3. The exact value is now \(s(11) = T = 3.877083590022814\ldots\)$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\ldots\)$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 \times 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.

The code that produces the numbers: sqpack.verify decides validity exactly, sqpack.research.quench is the LP-in-cell quench, cases.trump11.independent_lp_cell is a second, independent implementation of the quench’s linear program, and sqsearch/ is the screening annealer.

Workflow Entry Contracts

A workflow is the purpose-and-output contract for one contiguous phase of agent work. It is independent of the operating focus: a focus identifies the phase’s primary quality emphasis, not the only principle that applies. W6 may run under a Correctness focus while an exact certificate is checked, then enter another W6 phase under Insight when the same registered question needs a creative construction. The focus changed; the workflow did not.

Workflow selection should reduce context, not create paperwork. Routine single-purpose work records four facts where the work is already tracked: the workflow, bounded objective or question, intended artifact, and focused check. No session-NNN artifact is required.

Use the fuller session contract only when the work crosses multiple workflow or material-focus phases, continues autonomously beyond an ordinary checkpoint, coordinates independently tracked delegates, supervises an expensive experiment or proof search, or needs durable recovery and handoff state. Each phase in that escalated record begins with its workflow and primary focus; objective and required inputs; expected durable output and validation command; stopping condition and fallback; and start and deadline. Actual outcome and evidence are terminal fields recorded when the phase closes, not placeholders invented when it opens. The generated ledger summarizes those versioned sessions; it is not a census of every routine task.

Result Import and Efficient Confirmation

A result published by others enters the record through the result import process, a standard sequence of phases and not a workflow of its own, from whichever source delivers it: an issue or a comment, an owner’s message, the Kingbird catalogue or another catalogue, or a watched repository. An intake pass, run when the owner asks, sweeps every source at once, and whatever the record defers names the open bead that owns it. That runbook owns the stages and their exits; this section says what W1 and W2 each contribute.

W1 turns an incoming result into a reviewable source packet: maintained repository and license, immutable source identity, precise claim and assumptions, certificate format, and any supplied verifier. Check the current register before assigning claim IDs; record explicit mappings when provisional IDs collide. Separate source assertions from results already independently confirmed. Every imported result within the register’s scope receives a claim ID, explicit verification (V), confirmation (C), significance (S) and novelty assignments under Epistemics. Record the significance rationale, assessment date and scorer, and explain the evidence and limitations supporting the verification and confirmation levels. These assignments are required at import, including when the result remains V0/C0; useful tooling or a promising claim does not earn a higher verification level. Keep each assignment attached to its precise claim, not to an entire repository or provider. Its W2 handoff names the proof obligations, existing evidence, missing checks, and the smallest useful next confirmation.

W2 owns correctness and efficient confirmation. For each obligation, declare the exact acceptance condition and domain, then use the smallest relevant check: premise audit, exact control, bounded diagnostic, or complete replay. Keep independent mathematical review and disjoint tool work in parallel. Reuse evidence only when its input, source, assumptions and checked scope still apply. Report what passed, what failed or remains unresolved, which implementation was independent, and the precise conclusion supported. A sampled replay, diagnostic frontier, or green software test is not complete coverage.

General slow repository testing is batched at integration or release checkpoints; it is not part of every W2 iteration. During confirmation, run checks for the proof, changed verifier, and affected contracts. Record broader integration debt separately without relabeling a proof-specific result as repository certification. Required hosted checks remain in force, but unrelated checks do not block the next independent review.

At each W2 checkpoint, inspect the cost of obtaining the next useful result. Separate observed analysis and coordination intervals from validation setup, exact computation, serialization and worker idle time. Record elapsed time and CPU or runner cost with source, workload and timing boundaries; overlapping agent intervals cannot be added to explain wall time. Missing timings remain unknown. Retained receipts come before new benchmarks, and profiling overhead is distinguished from ordinary execution cost.

Delegate a bounded W5 efficiency slice when a declared wall ceiling is missed, repeated setup or reruns dominate, workers sit idle with queued work, or the cost of a complete check is unknown and prevents choosing the next slice. Keep the regular W5 cadence in OR-12; these triggers need not wait for that cadence. W2 retains ownership of the claim and can continue independent obligations while W5 measures the bottleneck. The handoff names a bead, frozen workload, baseline or missing measurement, cost target, exact correctness guards, wall ceiling, and the owning consumer to return to. W7 can delegate this measurement while retaining ownership of pipeline readiness.

W5 chooses among less orchestration, stronger bounds, compiled exact kernels, caching, and bounded parallelism from measurements. Preserve the exact reference, refusals, provenance and complete-domain acceptance. Benchmark comparable workloads with repeat samples and spread before claiming a speedup; report negative results too. Return a reviewed change or rejection and a reproducible measurement to the owning workflow. Tool improvements and mathematical confirmation have separate dispositions; neither silently closes the other’s bead.

The current W5 validation efficiency and checkpoints plan reviews ordinary PR feedback, full final checkpoints, detailed timing records, and coverage-preserving cost reductions. The development guide owns the current commands, names, and budget semantics; historical benchmark records remain linked from the plan.

Implementation is an action inside the workflow that owns its promised result, not an undefined handoff: W1 and W2 can make bounded research corrections, W3 can implement a bounded exploratory derivation or visualization without spending an undeclared experiment budget, W4 can make a narrow accepted process correction, W5 can implement a measured optimization, and W6 can build a one-round instrument that freezes before measurement. W7 owns reusable packing-pipeline capabilities, targeted refactors, robustness, visualization infrastructure, and cleanup for named consumers. W8 owns the reader-facing tier when research has moved past it, and it is a reconciliation workflow rather than an authoring one — its edits answer to the record, not to taste. Two boundaries make that real. It may not introduce a claim the artifacts do not already carry: a document that wants to say something new is asking for W1 or W6, not for a documentation pass. And it may not resolve a disagreement by choosing the more readable side — where a document and an artifact conflict and the artifact is not obviously right, the output is a defect, because a documentation pass that quietly picks a winner is how a wrong claim becomes the tidy one. Schedule it after a run that closed several commitments rather than continuously; the documents are meant to trail the record slightly, and a pass with nothing to reconcile is a pass that should not have been opened. Registering a result does not open one: the change that moves the record runs New Result Publication itself. W8 also owns a review paper that explains a confirmed result; the paper states nothing the register does not hold, and its exposition gets a W2 review.

W9 owns bounded repair waves over confirmed defects and issues. It does not turn a large backlog into one undifferentiated implementation phase: risk is ordered first, compatible defects are batched only when they share a trust surface, and every selected item exits fixed, contained, rerouted, blocked, or obsolete. W10 owns mathematical portfolio planning at launch and checkpoints, and full closeout after an agenda or remediation wave. Its planning process distills source assessments into H-items, agenda commitments, and beads. At terminal closeout, the documentation review is a mandatory impact check over the root documents; W8 owns substantive reconciliation when that check finds real drift. W10 selects one coordinating entry, which can dispatch independent commitments in parallel after the planning block closes.

general-improvement remains only for repository maintenance outside the packing pipeline whose output fits none of W1–W10. It must not hide core work or a session alternating among research, review, and infrastructure; those are separate phases.

Switching Workflows in One Session

One phase is active at a time per versioned agent session. Start a new phase when its purpose, primary focus, or bounded slice objective changes. A focus-only change repeats the workflow name and is a phase boundary, not a workflow switch. A momentary shift in emphasis is not a phase. A renewed slice may repeat both workflow and focus, but it must close the prior slice, change the objective, and state the new fact that justifies another clock. An orchestrator may switch or renew at a planned checkpoint, after a concrete evidence checkpoint, on a user request, or because the active premise was falsified. It closes the old phase first with status, evidence, stop reason, and next action; then it declares the new workflow, primary focus, objective, expected output, validation, kill condition, fallback, start, and deadline. It does not relabel mixed work after the fact.

Sessions 001–008 predate this workflow vocabulary. Their v2 phase rows are explicit retrospective reconstructions from the durable session record, not evidence that those workflows, focuses, clocks, or transitions were declared contemporaneously. Current and future phases are declared before work begins.

The normal research cadence is not a mandate to traverse every workflow:

W1 research-survey ──> W2 factual-review ──> W3 insight-iteration
                                               │
                         missing reusable tool v
W4 process-review ──> W7 pipeline-improvement ──> W2 ──> W6 research-loop
        │                    │                              │
        └─ accepted repair ──┘        W5 efficiency-loop ──┘
                         promoted/high-risk result ──> W2 ──> W3

launch/checkpoint ────> W10 review/planning/oversight ──> coordinated parallel work
W1–W9 terminal work ──> W10 terminal closeout ──────────> selected coordinator
confirmed defect wave ──> W9 remediation ────────────────┘

result by others ──> W1 import ──> W2 validate ──> publish ──> answer the author

At any checkpoint, the human operator may choose the next phase, narrow the question, or stop. Long autonomous sessions use the same rule; autonomy changes the duration and controller, not permission to blur contracts.

Current Handoff

Session 183 ran the one state of BC-428’s draw that exp-257 never reached, draw 31, under BC-429 and exp-258, with exp-257’s recipe unchanged from the clean run worktree at cebb5d15a. It stopped with its resource rollups withheld (think-h8oz); the hosted fast run of its close commit certifies it.

• Certified residue. Draw 31 closed in 577 s of wall and passed the standing kernel verifier in full in 266 s; s183-bc429-u31 is admitted, and the census is 36,784 states in 4,685 orbits under 58 admitted entries, the endpoint surviving.
• Accepted. exp-258, on its criterion (exp-258). Every one of BC-428’s 31 draws now has a verdict, and 26 of its 29 counted draws closed. H-275 remains an open question.

The session before it:

Session 182 ran BC-418’s n17 overnight lanes from the clean run worktree at cebb5d15a, admitting each closure on the standing kernel verifier’s full pass. It stopped at its deadline, its resource rollups withheld because they carry model identifiers (think-h8oz); a hosted fast gate at b68744cba (PR 379) later certified its handover.

• Certified residue. 126,168 states in 15,953 orbits fell to 36,792 states in 4,686 orbits under 57 admitted entries, the endpoint surviving, counting u29, admitted after exp-257’s verdict.
• Accepted. H-267 is confirmed: the entries of arity at most seven leave 8,191 orbits (exp-251). H-264 and H-274 are accepted (exp-252, exp-253). Each of the three was confirmed with corrections by its W2 review. H-275 is accepted on a round stopped by its clock, and its W2 review confirmed it with corrections: 24 of 27 counted draws closed, 25 of 28 counting u29 (exp-257).
• Unresolved. H-273: all 95 distance-2 orbits were searched and none placed (exp-255). exp-254 is unresolved for H-267; its eight arity-8 closures count in the census.
• Held for the owner. Lane K’s target 2 and BC-426’s two re-runs, closed and verified in full but held on BC-423’s control receipt; the branch-and-bound queue, stopped as miscalibrated; #360’s merge.

Before it, Session 167 merged PR 283 onto current main and ran BC-406’s lanes, plus the follow-ups their results selected. Every verdict rests on an independent review and a clean committed-tree run.

• Accepted. H-258, the common-core stress, is accepted (exp-242). H-265 identifies the certified side with the catalogue’s irreducible degree-18 polynomial (exp-245).
• Rejected. H-262: R068’s charge at the cap excludes nothing, and one symmetric linear per-cell floor vector leaves at least 30,966 orbits whatever the charge (exp-243).
• Unresolved, each with a stated closing item. The local minimum modulo sliders is certified at radius \(1/5000\)$1/5000$ over a declared slider box, worst ratio \(0.926\)$0.926$, but the claim names the whole physical slider domain, and H-268 owes the bound (exp-244). A 24-cell capacity-one cover is certified with 43,593 orbits, against 7.7 million on the H259 grid, but the endpoint family realises a second state through an overlapping cell (exp-246).
• Replanned. n11’s focused radii were of the n17 scale, so capture is priced as logarithmic in the radius (capture review). The global half’s next engine is isolated sub-pattern exclusion on the minimal cover (design review).

No bound, frontier field or open status changed.

Selected next entry: think-tmz6, the BC-418 coordinator, continuing. Its first decisions are the owner’s: whether BC-423’s endpoint7 control re-check (PASS_SAVED_STALL, cells and node matching) releases k2 and BC-426’s two closures; recalibrating the branch-and-bound queue; and publishing the certificate objects (think-jhgi, which needs uploads.github.com). The research step after that is BC-423’s recipe (48 rounds, 2,304 rows, octagon core) on the kept cap-stall nodes of BC-425 and BC-427, once its control is ruled on, followed by lane D’s aimed splits (C2). The capture route (lane R9) waits on the hull-vertex compression-pull repair (think-juy9).

Session 168 ran BC-418’s lanes. Its record is not yet written and will take session-181 (think-wcqs). Hosted certification of Sessions 166 and 167 passed again on this branch at c0941ba4e (Packing validation run 37247106436).

• Accepted. H-266, on the unique-state 24-cell cover (exp-247): 43,593 orbits, with the family in one state. H-268 (exp-248): square 6’s cell bounds every slide inside a widened box \(B_W'\)$B_W^{\prime }$, over which the local theorem passes. The local half is therefore the capture-target theorem of the composition review. H-261 stays unresolved as worded.
• Admitted. Four exclusions, each by an independent or standing verifier’s full pass. W7 was closed by the kernel and A by an interval branch and bound (exp-249), then flag 3 (SW9, arity 9) and the whole residue state N1 (exp-250). Their verifier at 25c1cdef6 carried the closed-cover defect class found the same day; neither defect was reached on them, and the fixed verifier re-passes both (verifier-rewrites review, §6.2 and §6.5). The certified census is 126,168 states in 15,953 orbits. The selector’s finish-stage recheck placed one of its 90 flags (an arity-8 false flag), so 87 flags stand uncertified. If all of them certify, 2,197 orbits remain.
• Measured. The residue survey finds no sampled state feasible at the cap; each needs its own failing sub-pattern of arity 8 to 15. Flag 2 (arity 9) stalled at 1,152 adaptive rows, and its 2,304-row check stopped incomplete at its time ceiling. Its diagnosis reads it as a true pattern held by west-wall row losses. Capture pilot 1 met its falsifier, which the after-pilot review found producer-limited. Pilot 2, with rows allotted by need, met that review’s sharper falsifier at round 17: no position contracted. Lane R9’s reading is not yet written.
• Infrastructure. Standing verifiers gate the census, and the streamed kernel verifier (601bbf110) is admitted. The 92 certificate objects (112,285,110 bytes) are hosted outside Git under OR-18 and listed in packing/hosted/n17-x048-session-168-certificates.yaml. Their release exists and awaits the uploads, which the cloud environment’s egress refused (think-jhgi). Lanes F1 and F2 wrote the two cost-reduction reviews.

No bound or open status changed. The frontier page now records H-265’s identity (think-yjgk).

In flight under think-tmz6:

• R9 and the capture route (think-g2qn);
• flag certification (think-j6qy);
• the census’s flag list after the recheck, and the residue-universe sweep (think-gygy, paused at chunk 61 of 848);
• the H-264 pilot (think-e17c);
• the compiled checker (think-ui2y);
• closing the session (think-wcqs).

This branch’s Session 168 is a working label. Main’s Sessions 168 and 169, below, hold those ids, and the open drafts claim session-170 to session-180, so its record takes session-181.

Session 168: Families, the T-007 Correction and T-087

Session 168 answered the owner’s four questions about the \(n = 1..324\)$n=1.\mathrm{.324}$ atlas in X-049: the families were never classified by \(n - k^2\)$n-k^2$, light green squares are geometry rather than arithmetic, an exact regularized layer darkens them on the homepage toggle, and the pattern set at large \(n\)$n$ is open. Its literature lane found Nagamochi 2005’s Lemma 1 false, so T-007 is V0 and 287 case records were re-grounded with dated corrections and defect D-516: 233 open floors fell to Karakuş’s general bound (T-083), \(s(k^2-1) = k\)$s(k^2-1)=k$ rests on Karakuş (T-084), \(s(k^2-2) = k\)$s(k^2-2)=k$ on chelokot’s Lean proof replayed here with an axiom receipt (T-086), and \(n = 37, 61\)$n=37,61$ on Bašić and Slivková’s piercing bound (T-087). Floors that correct Nagamochi’s work say so on every surface, as “corrects Nagamochi 2005”. Merged on 3 October 2026 with main’s replayed certificates and covers (T-066 to T-079, and T-062 to T-064 raised to V3/C3), 45 of those floors moved higher, \(n = 37\)$n=37$ and \(61\)$61$ among them, so T-087 stays registered and holds neither; the second merge that day, with T-080 and T-081, raised five more at \(n = 101\)$n=101$ to 105, and the third, with T-082 and the replays that raised T-073 and T-076 to V3/C3, one more at \(n = 82\)$n=82$, so 187 open floors rest on Karakuş and 219 carry the tag. Its open item is the owner’s restoring commit for the withheld model labels (think-wqfw); its result identifiers, first T-066 to T-070, then T-080 to T-084 and then T-082 to T-086, were renumbered T-083 to T-087 when main took T-066 to T-082. The selected next entry above is unchanged.

Session 169: One Record per Line for Retained Results

Session 169 answered the owner’s question whether PR 305 should be 275,273 lines. Most of it was generated data in indented JSON, one scalar per line, so a shared writer, sqpack.retained_json, now writes retained results one record per line, and PR 305 adds 102,197 lines with no value changed. PR 323, stacked on it, moves 31 more retained results onto the writer (1,480,449 lines to 155,443) and adds a check that holds every tracked JSON file over 5,000 lines to the layout or names its exemption. Squashing would save 0.5 MB of a 950 MB repository that is 87% PDF, gzip and PNG, so the history stays, and the repository’s growth is left to four owner decisions. The selected next entry above is unchanged.

Previous: Session 166 n17 Route Review

Session 166 ran a W10 checkpoint on the merged PR 265 record with two Fable extra-high lanes. The route review holds the assessment, the evidence status and the reading order for the next agent. Neither lane found a mathematical error. In exploratory checks the stalled H258 stress is valid, and the kernel of its 52 positive rows is exactly the six slider and rattler directions, so the local theorem needs no second-order analysis. Its first-order radius estimate is \(3\times10^{-4}\)$3\times {10}^{-4}$. The global half has a census and no exclusions; settled-case cuts alone leave about 7.7 million of the 20,155,518 orbits. The conditional minimum holds only for sides in \([4.675,4.676]\)$[4.675,4.676]$ and cannot be the terminal theorem; the morning report and projection review carry dated scope notes. No bound, frontier field or verdict changed.

Its selected entry was think-c7kv, the BC-406 coordinator. It dispatches three disjoint lanes in parallel: BC-402 repairs the H258 identity proof (then BC-407 proves H-261, the local minimum modulo the slider cone); BC-408 measures H-262, the survivors under settled-case cuts and conditional charge floors; and BC-409 identifies the endpoint with the catalogue polynomial (H-265). BC-410 and BC-411, which now owns the re-scoped think-11ma, wait for BC-408. Session 166 stops with hosted certification pending under think-od9c.

Previous: Session 165 Post-optimality Overnight

Session 165 completed seven independently reviewed n17 rounds: exp-235 through exp-239, exp-240 and exp-241. The known packing now has a certified exact chart endpoint and an attained minimum under explicit orientation and directed-projection premises. The verified outward upper ceiling is 4.6755300936045509516342148538535054; the lower bound 4.66044 is unchanged. Unrestricted local and global optimality remain open. The mixed-capacity cover has 161,100,756 necessary occupancy states; its closed-assignment D4 quotient has 20,155,518 orbits, with no geometric case excluded. H258 stopped after three preparation failures without a target stress verdict. The morning report records the mathematics, independent-checker boundaries, costs and remaining gaps.

Session 165 selected think-11ma, a small exact geometric-exclusion pilot below the certified endpoint. Session 166 re-scoped it to a cap at or above the endpoint, as BC-411.

Previous n11 Intake and Verification

T-060 is machine-checked at V3/C3/S5 under the current epistemics rubric. Its historical V4/C5 label did not denote human referee confirmation. The Queuingtheorydotcom/11SquaresOptimal proof gives \(s(11) = T\)$s(11)=T$, Trump’s exact side. The retained packet pins the source and independent exact replays; the review audits the full mathematical composition, including all 2,180 exclusions, ten capture nodes, local isolation, and the exact witness. The publisher’s four cached final-state digests are stale; our acceptance rests on fresh source-bound geometry, not those cached results. On 2026-10-06 the Lean 4 formalization of the proof, ElevenSquare.optimality in Queuingtheorydotcom/11SquaresFormalized, announced as formalized with Astra and Claude, entered the record as the source’s reported proof-assistant evidence. The statement audit reads its theorem as exactly T-060’s claim; the source reports that its full verification run, resumed from earlier receipts, passed with Lean’s compiler trusted for 13,308 native_decide axioms; and the statement closure and upper half were built here. It moves no rung until a complete build the record can rest on and a human expert’s review of the formalization are retained. T-037’s verified \(s(11) > 31/8\)$s(11)>31/8$ and T-059’s reported row-minimum equality retain their separate scopes. PR 246 merged with the verified result; the next handoff is a bounded fresh-ensemble replay entry point.

The n = 11 papers form one series, read in order (plan): Part I, the project’s lower bounds T-018, T-025 and T-026; Part II, a review of Kleddamag’s \(s(11) > 31/8\)$s(11)>31/8$ (T-037), its k-of-m charges, shrunken parents with strict cores and exact sweep (source); and Part III, the dedicated optimality paper, which explains that complete argument from first principles. Its simplification review consolidates the proof dependencies and geometric invariant without removing required cases, branches or checks. The rendered paper and PDF include the exact center cover, occupied mask and capture ancestry, with the implementation-sharing and fresh-replay limits stated beside the verification record.

The following paragraphs retain the previous intake handoff as an execution record. It placed tooling and efficiency off the proof’s critical path, then assigned think-uz2x to simplification and think-08pw to the separate n11 explainer. The Session 164 plan records parallel lanes, bounded checks and integration debt.

Session 163 completed the reviewed rectangle-bound, refinement, and T-059 receipt-admission slices on PR 246. The merge with main and hosted fast-tier certification are complete. The dependency map separates these engineering slices from complete certificate replay, global counting, ceiling repair and accelerated-verifier validation. These slices do not promote a packing bound.

Session 162 initially closed the wand125 intake, native rectangle-verifier prototype and documentation slice with explicit certification debt, since discharged by the hosted fast checkpoint. The implementation and review are published in PR 246. Required CI and the certificate-page workflow passed at c621b845f and the documentation follow-up c5490f783. The full deferred checkpoint also passed on the unchanged implementation at c621b845f. No complete retained external rectangle certificate has been independently verified.

Previous n11 follow-up: think-e2ot, build the bounded fresh-ensemble replay entry point while preserving the accepted historical evidence. The later mathematical entry is think-bmf3, W7: design and cost a whole-angle traversal using the measured refinement result, before a complete external rectangle replay. The two-level diagnostic evaluated all 268 children and closed 15 of 67 depth-capped parents in 8.994 seconds. The other 52 parents and 11 originally queued boxes remain outside a complete proof. The earlier corner comparison’s zero new threshold crossings remains a negative result. Complete external-certificate coverage remains required before assigning independent confirmation to that rectangle certificate. T-059’s complete source-row equality remains open; the identical point certificate’s global packing proof is already established as T-037 V4/C4. No frontier bound was promoted.

Session 151 asked again what improvement is left at low \(n\)$n$ and moved one bound. The frozen T-025 threshold atoms re-certify at the 2880-step net, where the crossing shrink does not rise, so the dilation-limit supremum rises to \(955000 \cdot \sqrt{2073600042893309449}/359341754646249 = 3.826997548829544\)$955000·\sqrt{2073600042893309449}/359341754646249=3.826997548829544$, \(+0.00055\)$+0.00055$ over T-026. Both retention routes accept the frozen bytes and agree at exactly 1, and the limit record is replayed and written. Session 151 deliberately left the register entry unwritten, which is why that session remains stopped with certification debt rather than being rewritten after the fact. PR 221 later registered the result as T-033; Session 154 reconciles it with the stronger external \(s(11) > 31/8\)$s(11)>31/8$ bound. Four cells returned measured negatives with witnesses — the \(n = 17\)$n=17$ triples and the parent-centre restriction are both load-bearing, re-pricing that support is capped at about \(+0.0034\)$+0.0034$, and the first grid-capable search at \(n = 12\)$n=12$, \(20\)$20$ and \(21\)$21$ returned the grid exactly on every run. Its X-042 contradicts X-041 in nine places, and the block corrected itself three times, including reverting an H-228 refutation that an adversarial lane caught after it had been pushed.

Session 150 landed the agenda-040 overnight stack and the n = 17 intake on main, repairing four confirmed review findings at the integration point rather than after it, and left the session’s own analysis as records: X-041’s ranked slate and the 2026-09-21 derived-artifact currency review. It also replayed and reviewed a fifth external n = 17 value, Kleddamag’s \(461300/99853\)$461300/99853$, which reproduced byte-identically through both of its own checkers and drew no Blocker and no High from an adversarial proof review. That artifact is retained at V4/C3 with C4 blocked, and no bound moved for it: the registered n = 17 lower bound is T-032 at \(461300/99999\)$461300/99999$.

Three process defects came out of the block and are tracked rather than worked around: think-fqut, where GitHub’s stacked-PR merge orphans declared gate commits; think-qsn2, where check_session_gate’s verdict depends on the clone’s fetch depth; and think-3umt, where a record authored terminal can never earn its first receipt.

Session 152 retained and reviewed the complete external n11 threshold, rectangle-density and point certificate packet. Complete source replays and mathematical audits support 19 newly audited verified-field improvements, and the session corrects n17 to the stronger Kleddamag bound already replayed and reviewed in Session 150, for 20 promotions in all. The n11 and n17 paired source checkers each share one event-cell method, and the density global decision remains the source C++ method, so the adopted evidence is stated at C3 rather than C4. The density continuation driver’s wrong-count and stale-side imports are a High defect in that admission path; the separately checked fixed certificate files remain valid. The scoped pre-push at clean commit 819ade7 timed out in reachable behavioral tests with no emitted assertion failure; its retained receipt is diagnostic, not certification. The closure is certified at reachable branch commit 819ade7ca8afbe634a6ee54f215f0878f5674031 solely by the hosted five-job full gate.

Session 153 completed the independent adaptive parent-core audit. All 12,028 rows certify with the admissible parent-centre domain, strict core containment, and bounded site and feature tables. The full proof remains pinned to clean c183cc9ab; PR 223’s final records at 22671c5e6 merged into main without changing the 19 frozen proof inputs. This supplies C4 confirmation by a method independent of the source implementation.

Session 154 reconciled PR 221 with the final PR 222 head. T-033 and its three evidence records remain the retained first-party 2880-step rung, while the external strict \(s(11) > 31/8\)$s(11)>31/8$ result remains the current case bound and all twenty promoted fields remain current. BC-373 is complete on the retained T-033 receipt and full-gate evidence; Session 151 stays stopped as the historical record of its cutoff.

PR 224 is merged. Session 155 publishes the owner’s W3 frontier review as PR 230: three reviewed explorations, three diagnostic tools, seven original receipts and 31 shaped idea rows. It changes no bound or registered hypothesis. Ordinary PR checks and the exact-head five-job full checkpoint passed. Session 154’s earlier think-vx26 selection remains a bounded publication gap: render T-033’s missing standalone claim document from the retained result and evidence records. think-tzg7 owns the frozen producer-provenance limitation, think-380b owns the broader significance rubric, think-ck07 owns a second complete density-verification method, and think-c0xc owns the continuation-driver admission guard.

Session 156 answered that prioritization overnight, stacked on PR 230 as PR 231. Four reviews of X-043 to X-045 found no fatal error and changed what counts as progress at n11: with \(s(11) > 31/8\)$s(11)>31/8$ known, closing the gap to Trump’s \(U\)$U$ is the whole problem, and no counting certificate can prove equality there. X-046 therefore lays out a ladder of restricted-family theorems, and X-047 maps where the additive route dies at each low \(n\)$n$; agenda-042 registered H-236 to H-241. One bound moved: T-034, \(s(21) \ge 122/25\)$s(21)\ge 122/25$, from a window-free point certificate that a Fable max review accepted on three routes. At n11, rung 0 of the ladder (Trump globally optimal at its own angle) closed 198 of 256 subtrees on \(1.19 \times 10^8\)$1.19\times {10}^8$ nodes with every checked certificate accepted and no leaf below \(U\)$U$; the tree is about a thousand times X-046’s estimate, so rung 1 needs a stronger relaxation. The capture-radius route is exhausted at the BC-199 modulus, and a descent-filtered census found no third-orientation minimum below Stromquist’s value but two new minima within \(U + 0.02\)$U+0.02$. The n12 ceiling run ended unsettled, and the ParentClip build never opened: the harness session quota stopped every agent from about 03:15 to 08:45 PT. Session 156 is closed and certified by hosted full run 35960673750 at a08ce5289.

Session 157 spent one night of CPU on registered work, stacked on PR 231 as PR 233. Rung 0 closed. The last 58 subtrees ran with the unchanged frozen instrument and the independent reader accepted the complete tree: 119,556,859 leaf certificates, three Trump-degenerate leaves, no unresolved leaf (exp-232). H-236 is confirmed: at Trump’s own angle, no packing of eleven unit squares beats \(U\)$U$, the first optimality statement with an equality case for a family containing Trump’s packing (Stromquist 2003’s \(0^{\circ}\)$0^{\circ }$/45° bound is an earlier restricted-orientation statement), pending BC-241 for the local theorem its terminal leaves use. The n12 cutting loop converged at \(11.980175 < 12\)$11.980175<12$, rejecting H-241 (exp-233). D-508 corrects exp-231’s certificate count, which had included branch nodes. Hosted full run 36003435328 certified the closed session.

Session 158 locked in rung 0 and priced rung 1, stacked on PR 233 as PR 234. A Fable max review accepted the closed tree, and it is registered in two parts: T-035, the machine-verified reduction of every packing in the family to Trump’s ball (V4/C5), and T-036, the composed theorem that Trump is optimal at its own angle, with equality only at Trump (V3/C2, the minimum of its parts). BC-382 closed BC-241 with a full radius-generator replay and a method-distinct control, so BC-240’s first clause is verified and exact. The 8 GB certificate tree is archived off-repo with its SHA-256 manifest in the record. The rung-1 pilot (exp-234) ran eighteen boxes away from Trump’s tilt: none closed at 150,000 nodes per subtree, and every one closed about two-thirds of its measure for about four million nodes whatever its width or tilt. Rung 1’s cost is in the fixed-angle centre enumeration, so a stronger per-node bound comes before H-112. Hosted full run 36075268969 certified the closed session.

Session 159 took in Guzhou0806’s R052, \(s(17) > 231001/50000 = 4.62002\)$s(17)>231001/50000=4.62002$, built on Kleddamag’s architecture. All four of the source’s replay modes pass here, both full sweeps reproducing its row ledgers exactly, and a Fable max review found no mathematical defect (review). It became the verified n = 17 lower bound at V4/C3, until Kleddamag’s v1.1.0 \(232001/50000\)$232001/50000$ superseded it on 27 September; the native interval route refuses it at its engine ceilings, so there is no method-distinct decision yet. A planning block then asked what R052 and the closed rung 0 make possible (plan). At n = 17, R052’s certificate is nearly saturated, so a first-party increment of \(10^{-4}\)${10}^{-4}$ is not worth building; an unreviewed lemma says a triangle-free overlap family of 34 squares at side \(S\)$S$ caps every capacity-one certificate at \(S\)$S$, which a cheap search can price. At n = 11 the retained trees show the separating-axis LP reaches any target until about twenty pairs are fixed, so BC-384 waits on a tilt-profile census and a two-class counting certificate. Agenda-042 gains BC-386 to BC-391 and H-243 to H-247. Hosted full run 36121001128 certified the closed session.

The 27 September planning block (BC-392, plan) followed Kleddamag v1.1.0’s \(s(17) > 232001/50000 = 4.640020\)$s(17)>232001/50000=4.640020$ and wand125’s rectangle certificates for n = 18 to 78. Every atom of v1.1.0 has capacity one, so the certificate itself refutes H-243’s \(4.63\)$4.63$ family and the ceiling search moves to \(4.65\)$4.65$ in clique-weighted form (H-248); a reweighting of its dictionary is worth of order \(10^{-3}\)${10}^{-3}$ in charge, an unmeasured amount of side (the lemma check withdrew the plan’s \(+0.006\)$+0.006$ cap). BC-386 is superseded by BC-393, the same cap lift aimed at v1.1.0 through a winning-subset atom; BC-391 is superseded by wand125’s \(4.985\)$4.985$. The overnight queue is BC-390 on eight workers beside rectangle-density ladders at n = 82 and n = 50 (BC-394, H-250 and H-251) and n = 12 (BC-395, H-249), the rows the external certificates left weakest; BC-393, BC-388 and BC-387 follow their day builds. evand/square-packing’s claims (\(s(32) = 6\)$s(32)=6$ by a zero-margin closed cover, \(s(12) \ge 3.968616\)$s(12)\ge 3.968616$, \(s(21) \ge 4.995\)$s(21)\ge 4.995$), reviewed and registered by other lanes, retarget H-249 to \(3.99\)$3.99$ and add BC-396 (H-252): the same cover carried upward to \(n = 45\)$n=45$, side \(7\)$7$.

Session 160 took in Kleddamag’s \(s(17) > 232001/50000\)$s(17)>232001/50000$ at V4/C3, Evan Daniel’s \(s(32) = 6\)$s(32)=6$ at V4/C1 with \(s(12) \ge 15680/3951\)$s(12)\ge 15680/3951$ and \(s(21) \ge 5000/1001\)$s(21)\ge 5000/1001$ at V4/C3, and wand125’s rectangle bounds for n = 18 to 78, each after a Fable max review, and contained D-509’s explainer PDF wobble on PR 235.

Session 161 took in wand125’s 28 September update and what it pointed to: Guzhou0806’s \(s(17) > 116511/25000\)$s(17)>116511/25000$ (T-043), Evan Daniel’s mixed covers for \(s(21) = 5\)$s(21)=5$ and \(s(45) = 7\)$s(45)=7$ (T-052, T-053), wand125’s point-only routes to both (T-054, T-055) and its reported \(s(50) \ge 37/5\)$s(50)\ge 37/5$ (T-048), each after a Fable max review, and recorded the retained zmx2 run as a second method for \(s(32) = 6\)$s(32)=6$ (jlevy/squares#245). It stopped at 07:12Z with the complete zm_mixed.py re-sweeps unfinished, so its handover is uncertified and named under think-l6la.

Selected next entry at the Session 161 cutoff: think-l6la: the complete zm_mixed.py --d4 --cert-mode re-sweeps for \(s(21)\)$s(21)$ and \(s(45)\)$s(45)$, recorded, raising T-052 and T-053 to C4.

Selected next entry at the Session 160 cutoff: think-7c17, BC-390: the widened n = 11 rung 0 box on eight workers overnight, with BC-394’s rectangle ladders (think-pr2b), the 41 queued wand125 replays and Evan Daniel’s \(s(32)\)$s(32)$ full sweep on the remaining workers; BC-393 (think-0rbj), BC-388 and BC-387 follow their day builds.

Selected next entry at the Session 159 cutoff: think-amx8, BC-386, since stopped in favour of BC-393.

Selected next entry at the Session 158 cutoff: think-ggk5, BC-384, now blocked on BC-388 and BC-389.

Selected next entry at the Session 157 cutoff: think-6w2y, BC-381, the closed-tree review, fulfilled by Session 158.

Selected next entry at the Session 156 cutoff: think-ie35, BC-375, finishing rung 0. Run the 58 wall-cap subtrees with the unchanged Amendment 1 bytes and then the reader over the whole tree; the index list is in exp-231’s retained summary and the 5.5 GB tree sits in the Session 156 worktree’s attic/rung0/, outside the record. Deferred behind it: a stronger per-node relaxation for rung 1, a second-order-exact isolation theorem (idea 246), think-m9iz (ParentClip, for n21 at 4.9 and n18 at 4.70) and think-xmm4 (the n12 ceiling with a converged row loop). The owner’s decision on retiring H-121 as a route, which X-046 recommends, is open.

Selected next entry at the Session 155 cutoff: think-5zjd, user prioritization of the shaped W3 candidates from X-043 through X-045, fulfilled by Session 156. Session 153’s earlier think-d010 publication handoff is fulfilled by PR 223’s merge.

Selected next entry at the Session 151 cutoff: think-gvlg, registering the \(n = 11\)$n=11$ rung Session 151 left accepted and unregistered. Its threshold certificate at the 2880-step net is RETAINABLE by both retention routes, which agree at exactly 1, and its dilation-limit record is replayed and written. That cutoff debt is now discharged by T-033 in PR 221; this paragraph preserves the selection Session 151 actually made. think-zmos, the W5 efficiency block that was the previous entry, is discharged: OR-17’s 1.38x turned out to be the hosted runner pool rather than drift, the four CI jobs are clocked, and the rule’s text is corrected. The agenda-040 closeout under OR-11 remains outstanding and is not this entry.

Session 149 adopted \(s(17) \ge 461300/99999\)$s(17)\ge 461300/99999$ as T-032 from Guzhou0806’s R012 certificate, with Mira’s \(4613/1000\)$4613/1000$ beneath it, after four passing replays and a proof review that found no error. It is the first verified bound at this size that came from outside, and both certificates descend from this repository’s own T-019. The identifier was contended: pull request 208 claimed T-031 from the open overnight stack for the \(n = 11\)$n=11$ octagon corner class, the stack merged into main first and kept it, and this result took T-032 when main was merged into the intake branch.

Selected next entry at that cutoff: think-pcd0, the n = 17 intake: land the adoption of \(s(17) \ge 461300/99999\)$s(17)\ge 461300/99999$ as T-032. The research entry behind it is BC-357, closing M7’s n=6 bracket at 299/100 under H-216.

Session 148, chunk 5 on PR 209, stopped at the owner’s request at 17:02Z with its work captured. It registered H-232 after an adversarial review: the all-deep corner class at 96/25 is pinned (occupant cores contain X', at least three non-occupants at depth at least sqrt 2 - 1 from every wall, at most one in the central 1.84-box), the ring-centre 2-of-3 atom collects exactly 5/4 against a budget of 1 from the transported 88-family, the maximum, and the fixed-support screen is the full kill at value 7. The gap-g wedge lemma (BC-364, H-230) is derived and reaches the 7.11 degree orbit but cuts no weighted pair of the 64-family (CANNOT REACH, unreviewed). Two partial ports (the corner clip on the threshold routes, the gap_wedge tool) are retained as patches under results/agenda-040. No bound moved.

Selected next entry at that cutoff: think-n1v2: resume chunk 5 from the retained patches and the wedge derivation (its review, exp-221 for H-230 and BC-364’s disposition, the threshold clip and the gap_wedge port), then H-232’s fixed-support screen, in Session 149 on the next stacked branch. BC-357 / H-216 stays the registered n=6 calibration entry in agenda-037.

Session 147 completed overnight chunk 4 of agenda-040 in PR 208, stacked on PR 207: T-031 registers the exp-220 exclusion of the octagon corner class at 96/25 at the scope Session 146’s review accepted, V4/C3 on the two gate routes — the exact sweep and the interval branch and bound are the two internal routes of one gate invocation, so the review counts them as one confirmation — significance 2, with a case package and a control test that replays the gate. The overnight loop closed on its clock after four chunks; no bound moved.

The selected entry at that cutoff was think-b7pr, BC-367: the four mixed corner classes at 96/25 and a second n=26 site set.

Session 146 completed overnight chunk 3 of agenda-040 in PR 207, stacked on PR 206. A Fable registration review of the exp-219 exclusion returned REGISTER WITH CORRECTIONS with no soundness defect: the gate replays byte-for-byte, the statement is a theorem about every packing of eleven unit squares in a square of side 96/25 (some square meets the open corner triangle x + y < 1/2), and the all-deep class is already outside the point language (BC-366), so the corner tree cannot close at 96/25 by clipping alone. The bytes’ unconditional claim string was fixed in the driver, the gate and the readers, and exp-220 re-froze the same 680-atom covering under the class claim with both routes accepting. The ceiling-family fold is retained as devtools.fold_ceiling_family. No bound moved.

The selected entry at that cutoff was think-b7pr, BC-367: write the registration entry at the reviewed scope, then the four mixed corner classes and a second n=26 site set.

Session 145 completed overnight chunk 2 of agenda-040 in PR 206, stacked on PR 205. The convex corner-clip instrument was admitted after an adversarial review, and exp-219 confirmed H-222 at its scope: every packing of 11 unit squares in a square of side 96/25 has a square meeting the open corner triangle x + y < 1/2 at some corner, RETAINABLE under the corner class hypothesis from both routes at mass 10.868617. That excludes the octagon class at 3.84; it is not a bound, and the all-deep class is already outside the point language (BC-366), so the corner tree cannot close at 96/25 by clipping alone. The three retained replay readers are re-bound to the instrument’s revision with their determinations reproduced. The overnight loop closed on its clock after two of four chunks; BC-361, BC-362 and BC-363 are dispositioned on agenda-040.

The selected entry at that cutoff was think-b7pr, BC-367: register the exp-219 conditional exclusion after review, clip the remaining corner-bin classes at 96/25, and give n=26 a second site set.

Session 144 completed overnight chunk 1 of agenda-040 in PR 205, stacked on PR 204. None of the three stock-instrument determinations reached its target: H-223 and H-224 are unresolved with their site sets refuted at 15.566 and 17.042 (exp-214, exp-218), and H-225 stopped on the clock at the 25.000000 plateau (exp-215). The BC-362 lane replayed Bentz 2016 Theorem 11 at the printed constants, retained the one-spare inventory under devtools/bentz2016, and rejected H-226 and H-227 as stated (exp-216, exp-217); D-507 corrects the Theorem 9 budget. No bound moved.

The selected entry at that cutoff was think-ni3v, BC-363: the corner-clip instrument and H-222 at 96/25 in Session 145 under exp-219.

Session 143 completed the owner-directed deeper mathematical review of the lower-bound routes in PR 204. X-040 reads the retained ceiling family as a fractional 8 + 3 packing, shows the corner deep branches neutral at the target sides, retires the theta screen and the four-wall stress theorem, identifies the one-spare integer cases 21 and 32, and corrects the Bentz 2016 transcription (D-505, D-506). Ten hypotheses H-222 to H-231 are registered and agenda-040 carries the overnight loop; no bound moved.

The selected entry at that cutoff was think-pogj, BC-361: decide H-223, H-224, and H-225 on the stock instruments in Session 144 under exp-213 to exp-215, with the BC-362 Bentz 2016 replay lane beside it.

Session 142 completed the correctness review and bounded pipeline repairs in PR 202. All four retained n=18 certificates passed both routes, and the corrected code passed the matching fast and deferred checkpoints. The original PRs 199–201 remain unchanged and are not independently ready to merge; landing must retain the corrections at the cumulative tip. The n=29 candidate remains interval-unresolved and unpromoted. The owner’s follow-up on 2026-09-19 requires the PR-by-PR landing-readiness block think-n3fl, then the small W7 correctness and efficiency block think-177v, before resuming H-216. The pipeline block includes think-1i1x and the publication update sequence in the documentation runbook. The current publication audit is tracked by think-kq00.

Session 141 closed the stacked n<100 research loop. It retained T-029 \(s(18) \ge 1871/400\)$s(18)\ge 1871/400$ and T-030 \(s(18) \ge 4679/1000\)$s(18)\ge 4679/1000$, confirmed H-219 and H-221, and left H-218 and H-220 unconfirmed. think-qqzs was the selected scientific continuation behind those prerequisites until Session 143; H-216 stays the registered n=6 calibration entry, and the owner’s 2026-09-20 direction runs the overnight lower-bound loop of agenda-040 beside the landing-readiness and pipeline blocks. Session 140 closed the preceding stacked-PR n<=100 survey and retained T-028 \(s(18) \ge 187/40\)$s(18)\ge 187/40$.

Session 139 is the preceding overnight scientific closeout. It retained T-027 \(s(18) \ge 467/100\)$s(18)\ge 467/100$, stopped after Route S encode-only timed out unresolved, and left H-216 open. Session 138 is the preceding route-selection handoff. It reviewed the n=11 record, ranked eight mechanisms that price relations between squares, subjected them to an independent adversarial review, and measured two. X-037 records the findings at their scope, and agenda-037 owns the resulting queue. No bound moved, no covering value was measured above 191/50, and no hypothesis was registered that night. The measurements come from scratch lanes and need guarded tools before any of them is retained.

• M1 (clique and majority atoms at 153/40). All 44 heavy cliques of the A6 64-family are budget-one threshold atoms. Fixed supports fell below 11, but column generation rebuilt a mass-11 family after every cut, and the decisive rows-complete LP was blocked by the unretained sites-1 checkpoint.
• M7 (helper-free point certificates). n=10 at 37/10 is foreclosed exactly by an integer ceiling family. The n=6 covering value at 299/100 lies between 83/14 (exact) and 6.006571 (float). The two-route gate accepts only crossings weaker than the proved values.

Session 138’s records landed when PR 193 merged 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: weighted-majority, k-of-S, and floor atoms are an admitted language (think-g3j7 still lands a new reader, and does not mutate T-025/T-026 verify_claim.py); H-216 is the n=6 existence determination; H-217 is Route F1, blocked on tools; M6 stays retired with no Route D search hypothesis; SDP is not admitted and M2 stays retired.

Selected next entry at that cutoff: think-qqzs, BC-357: close M7’s n=6 bracket at 299/100 under H-216. G1, G2, G3, and G5 are on main. G4 remains on this bead and is not H-216’s instrument. Session 139 stopped after encode-only timed out unresolved and T-027 retained \(s(18) \ge 467/100\)$s(18)\ge 467/100$. H-216 stays open. think-qqzs was the next entry until Session 143 selected BC-361.

BC-358, Route F1 / H-217, is blocked on the think-g3j7 reader, think-3xbr, and think-gyzw. BC-359, the M3 kill test under think-k4vb, is tentative. BC-360 retires M2, M4, M5, M6, and M8 with reasons. exp-161 remains Route S in agenda-036.

Session 137 is the preceding terminal handoff and the last pipeline one. It records the continuation of Session 136 by two concurrent Codex threads, their interruption, and the recovery that restored the 160 MiB snapshot cap and committed a repair for the Pages deploy that had not run since PR 183, pending the first main deploy. It then took PR 188 to green hosted CI at be28ad5a: the suite shards were rebalanced, and by owner decision the pull-request walls are advisory under think-g4n9 until they hold 180 s on hosted runners. PR 188 merged as 042e791c and the stacked PR 185 as d7f9d94d, and think-97we is closed; BC-355’s cell stays in_progress for those advisory walls alone. Neither stopped CI session changes a mathematical result.

Session 135 remains the latest Route S handoff. It discharged the four guards retained by Session 134: complete T-025/T-026 contents bound to a declared Git revision and repository-relative paths, both T-026 sentinels, a canonical source-bound nonempty selection manifest, and every declared mutation refusal. A fresh source-distinct audit found one path-alias hole; the repaired symlink refusal and its regression passed re-audit, so the retained receipt admits the instrument, and PR 182 merged it as 1d9c49c4 from reviewed head 609d7d62. No optimizer, candidate, coverage target, experiment, or scientific verdict was produced. X-032 owns the source and verdict boundary, H-163 owns the prospective scientific claim, and T-026 is only a support-and-rescaling provenance sentinel. BC-343 stays open in agenda-036 under think-ufmk. Session 139 registered exp-161 and ran encode-only; that process timed out unresolved. --search did not run.

BC-340, BC-353, and BC-354 are terminal. BC-341 remains tentative behind a future W10 reselection and the named Route A representation gaps, which Session 133 found when it stopped BC-354 at the frozen Route A representation boundary: three source inventories turned up no complete 80-stratum negative-root producer, seam-safe shared-parent domain, rows-complete matched baseline, conditional-domain gate, or independent exact replay. No target ran, zero of the 16 physical roots closed, and that is not evidence against a future complete Route A representation.

For the n = 11 Route A/Route S decision, the scientific evidence cutoff remains main revision 80bcdbb0819504354e1278c37f211dd8cc2158fb. Later merged campaign, CI and workbench records are included in the repository-wide roll-up above; none of them promoted a frontier result at n = 11, so T-026 was then the n = 11 lower-bound frontier. T-037 and then T-060 have since superseded it.

The older BC329, weighted-atom stages 3–4, and BC303 H-160/H-162 target lanes are paused. Their admitted implementations, registrations, and controls remain evidence; no exp-158 or exp-160 target receipt exists, so none carries a scientific verdict. The current inventory and candidate roadmap are in Research Program Status and Roadmap.

Handoff Record

September 10–13

New analytical exploration: X-027 connects the Stromquist correspondence with the recent certificate and owner results. Three cross-reviewed reports derive the full-unit fractional obstruction at \(38200/9977\)$38200/9977$, a precise interior-duality argument, seven-of-eight corner-mark ownership, and at most three normalized physical contact components. A floor-charge example adds an exact abstract expressiveness separation. These are analytical deductions with explicit scope, not newly registered frontier results or target measurements. BC329 remains the direct-bound continuation; small geometric charge and joint-owner tests are the next new mechanism comparisons. X-027’s ranked table states their prerequisites and what each outcome would establish. The exploration and all three reports now define their terminology locally, use KaTeX notation, and identify their imported premises and supplied results. Session126 retains the analytical work, independent reviews, and validation.

Weighted atoms now exist in production: Session127 implemented the representation and source replay from the first two stages of the weighted-atom admission. Its review addendum records the consumer corrections and the remaining validation boundary. ThresholdAtom carries an explicit positive integer token count per distinct site. Geometry uses one membership rectangle per site; the threshold and resource budget count tokens. For total token count \(A\)$A$, threshold \(k\)$k$, and nonnegative atom weight \(w\)$w$, the budget is \(w\lfloor A/k\rfloor\)$w\lfloor A/k\rfloor$. The D4 orbit key preserves each site’s count, and the inclusion–exclusion expansion runs over labelled tokens. The retained seven-token, threshold-four motif \((2,2,1,1,1)\)$(2,2,1,1,1)$ expands over 64 token subsets with absolute coefficient mass 209, where the same atom read as five sites reports 9, so the int64 headroom bound now reads the token count. All four retained receipts reproduce their declared token total, budget, charge \(3/2\)$3/2$ and exact charged-placement lists from family geometry, on rational coordinates up to 965 characters wide. Replay digests bind the supplied inputs; no retained historical digest authenticates their pairing. Unweighted admission and publication readers refuse declared weighted records. The internal interval route supports weighted member counts within its size limits; that support does not admit certificate coverage. No hypothesis, experiment or scientific target was registered or run, and the frontier is unchanged.

Selected next entry at that cutoff: think-8c9e, the weighted-atom coverage mechanics. The agreeing direct, event and interval controls on weighted atoms remain, including the closed-boundary and undercharged-core cases and the interval route’s stall handling, which is unresolved rather than a refuted atom or a failed budget proof. Certificate coverage admission stays blocked until they pass, and the paired instrument with its exact common row and point manifests is tracked separately behind it. The parallel BC329 lane has completed its bounded fixed-core runner implementation review in PR156. Its separate calibration instrument, three fresh full-shape host runs and source-distinct readbacks remain unadmitted and unrun, so BC329 execution remains blocked. The preflight addendum records the implemented controls and the remaining admission requirements.

Current combined reader entry: the consolidated PR-series takeaways, with definitions, proof results, scoped negatives and open comparisons in one place. PR137, PR142, PR145 and PR147 landed together at 1c1db463 on September 10, 2026. PR139 then merged as 3a18a05a, incorporating that owner strand and contributing T-024–T-026. At that cutoff the global lower bound was \(3.8264474\ldots\)$3.8264474\dots$; the upper construction is unchanged at \(3.8770835\ldots\)$3.8770835\dots$. The review corrections preserve the fixed-family scope of conditional obstructions and the existential owner-selection requirement. Finite support, net and grid results do not close entire research directions. The review addendum and PR139 carry finalization evidence. The post-merge daytime checkpoint adds no new global bound or target measurement. It proves that the translated 88-core obstruction has exact, zero-mismatch individual unit parents from \(3.82345\)$3.82345$, and independently verifies the analogous A6 statement from \(3.82845\)$3.82845$; contact, ownership and joint feasibility remain separate conditions. It also retains the fixed-angle adjacent-wall contact normal form, the correction that an arbitrary tight SAT row need not be physical contact, and the abstract \(4/3\)$4/3$ weighted-atom separation. The parent-domain adapter and production runner passed target-free independent admission, including deadline, timeout, failed-readback and source-closure adversaries. Exp156 then completed its sole source-bound run. The fixed exp151 residual lies inside its necessary parent box, while the first selected owner, TR / bottom-left:m1:j7, is already incompatible under the B-only model after all 181 frames and literal replay. The parent-restricted TR set is contained in that B-only set, so parent-domain gain is impossible there without running the redundant restricted arm. The frozen protocol did not evaluate BL, BR or TL; a new prospective protocol would need to skip TR and test those three owners. This complete old-model finding leaves H-158 unresolved and changes no global bound. BC329 remains the next direct global-bound target. BC337 is a secondary parallel lane, blocked on admission of a source-bound half-plane constructor, exact clipping, bounded runner and independent reader. It keeps exp151 direction 6 and open residual-centre domain \(C^{\circ}\)$C^{\circ }$. The control uses the existing TR centre-space obstacle \(P_{TR} + (-R)\)$P_{TR}+(-R)$ with the same nine other closed obstacles; the candidate substitutes the exact all-owner-incompatible obstacle \(K_{TR}\)$K_{TR}$ directly, with no second Minkowski expansion. Thus U0 and U1 remove the respective TR obstacles and the same other nine obstacles from open \(C^{\circ}\)$C^{\circ }$. The target would accept only exact area(U1) = 0 with independent union confirmation; because U1 remains open, that establishes emptiness. The strategy review puts the conditional parent comparison first and one frozen 2880-step core/net packet next, while multiplicity admission, contact-conditioned domains and mixed angle-profile charges proceed as separate blocks. The packet’s target-free preflight verifies its exact geometric headroom but identifies two prerequisites: test the raw least charge against \(M/11 = 685457679/687500000\)$M/11=685457679/687500000$, then normalize by the frozen rule \(\alpha = 1/m\)$\alpha =1/m$; and admit a bounded fixed-core runner because the existing refinement CLI runs a different adaptive experiment. Coverage remains unmeasured, so this is a readiness result rather than a new bound. The two-attainer target remains preparation. Historical handoffs below retain their original context.

Session113 closed Agenda032 with T-023, the five-dot exclusion of one specified four-owner branch at side \(96/25 = 3.84\)$96/25=3.84$. The composed result is V3/C3, significance S3: exact full-net coverage plus audited geometric transfer, with no change to the global bound. The sprint report explains the full result and next think-yhw2 selection. The gaps and routes analysis separates certificate assurance, exhaustive case coverage and stronger geometric restrictions, including what could improve the bound at a different target side.

Agenda033 governs the continuation after T-023. Exp145 independently confirmed all 361 exact zero deficits in 39.06 seconds. Exp146 then completed all 16 wall-aware owner classes in 25.69 seconds: 12 common footprints strictly enlarged, four were equal and none was impossible. H-144 is accepted, but that geometric gain adds no owner selection or global lower bound by itself.

Exp147 completed its bounded component-containment transfer: eight of 128 relations held, it preserved the two baseline tuple labels, and it certified no additional selection. This is a negative result for that sufficient transfer, not a physical tuple census. PR142 retains the independently tallied audit and wall-aware continuation. The owner-case design shows why proper containment cannot extend the equal-area coarse patch family; simultaneous square symmetries give only two geometric owner tuples. No shared arrangement census has been promoted from this result. Usage after Session113 is retained in separate, nonoverlapping receipts.

Math startup release checkpoint. Session 111 records the prepared geometry, parameter-first hydration, reload restoration, and the local browser and PDF evidence for PR 135. PR 135 subsequently landed on main at 171bba33; its post-merge CI, Pages deployment, live publication checks, and delayed-font smoke test passed, closing the release work under think-qcmi. The research priorities below are unchanged.

Parallel structural lanes at \(n = 11\)$n=11$, first wave terminal. X-021 pursued X-019’s exploration with four Fable lanes in parallel and reports what can be proved about eleven-square packings today: seven corner and wall lemmas, exact-verified angle counts at \(96/25\)$96/25$ on the rational cell unions specified in H-131 (rounded degree labels are approximations, not theorem endpoints), Stromquist’s Theorem 3 transported to \(0.68^{\circ}\)${0.68}^{\circ }$ bands at \(96/25\)$96/25$, the spanning and chain lemmas, a weighted ownership lemma that would make four-corner containment a theorem from one LP, and a duality lemma that prices every conditional and capture certificate — including a retained-net cap below \(U\)$U$ with the strict endpoint corrected in the handoff review. It also records what cannot be forced (corner penetration, blocker angles, positive-length contacts, a bound on orientation classes) and prices the three closing architectures. Agenda 030, epic think-kbci, maps eleven research lanes with disjoint deliverables under BC-292–BC-302. BC-303 selected the continuation and BC-304 has dispositioned every lane, including the unmet scopes inherited from Agenda 029. H-127–H-134 register the lanes’ claims. The lane reports and every script they ran are retained under results/agenda-030/. No bound has changed. The owner started the wave on 2026-09-08: sessions 100 to 104 run BC-294 (the \(B = 1\)$B=1$ value and the kill tests), BC-293 (the corner-skeleton measure), BC-295 (the band replay and widening), BC-297 (the \(3.82\)$3.82$ plateau) and BC-302 (the eleven-mark ownership set), each in its own worktree on claude/squares-n11-constraints-wl9atd; exp-130 was the next experiment id at launch. Session-103 is the first terminal lane: the exactly-eleven plateau at \(191/50\)$191/50$ is not a Trump-strip artefact (45 grid-seed sites and 822 of BC-200’s retained sites lie in two or more of the scaled cores), the general site-invisible-overlap mechanism holds, adding strip sites left the value at \(11.07\)$11.07$ with the generator stopping on its 32-row pricing cap, and an exact census at the different mass \(11.118805\)$11.118805$ exceeds one million near-tight cells with no clustering on Trump’s cores. This rejects the proposed strip explanation; it does not prove an obstruction at mass eleven or decide full-dual pricing. Session-102 replayed every count in H-131 exactly and widened the robust end band far past H-130’s \(3^{\circ}\)$3^{\circ }$: no packing at \(96/25\)$96/25$ has every folded angle in Theorem C’s exact end-cell union (degree boundaries approximately \(10.387466^{\circ}\)${10.387466}^{\circ }$ and \(43.0737^{\circ}\)${43.0737}^{\circ }$) (Theorem C, grid 119, mass \(11083/1024\)$11083/1024$), with \([0^{\circ}, 1.7139^{\circ}] \cup [43.5293^{\circ}, 45^{\circ}]\)$[0^{\circ },{1.7139}^{\circ }]\cup [{43.5293}^{\circ },{45}^{\circ }]$ the first rung on grid 79; the dual of the band toward \(40.19^{\circ}\)${40.19}^{\circ }$ puts its weight near the axis, not at Trump’s angle, and ceiling.py decides that none of those duals is a continuum obstruction, so the band’s true value stays open from below. Session-104 met H-134 in segment form: ten horizontal segments of length \(1/10\)$1/10$ centred on Stromquist’s ten Figure-13 points at \(96/25\)$96/25$ are a robust unavoidable set at tolerance \(3/500\)$3/500$, certified by an interval reader over pose space with every one of its 184,756 leaves re-decided in exact arithmetic, while every point-mark set built from the atom skeleton has an exact escape; every contained unit square is therefore localised near one of ten known segments, which is the premise route (a) needed, though not exactly-one ownership. Session-101 found H-128 unsuccessful on its tested finite support at \(96/25\)$96/25$: the corner-bounded measure sweeps exactly at mass \(11.798\)$11.798$ against \(11.262\)$11.262$ free, and the corner atom’s position, not the bound, is the obstacle on that support. H-128 remains open over the retained net; it proved the corner-pair form instead, that every packing at \(96/25\)$96/25$ has four distinct squares each containing one of its corner’s two marks, so the anchor for BC-299 is a corner pair. Session-100 left H-129 undecided: the \(B = 1\)$B=1$ family at \(96/25\)$96/25$ verifies exactly at \(8.918\)$8.918$ on a 203-direction net, with its weight diffuse in angle and mostly outside Trump’s neighbourhood. The handoff review found a stronger retained control: exp-070’s family transports by \(10000/9977\)$10000/9977$ to unit squares at side \(38200/9977 < 96/25\)$38200/9977<96/25$, preserving depth one and mass \(21342289572/2055263195 \approx 10.3842\)$21342289572/2055263195\approx 10.3842$. A smaller feasible family does not certify an upper bound. The depth polisher will start from that retained control; its missing scratch state is not a runnable handoff.

Session117 completed exp147’s bounded containment screen under H-145. All 128 relations completed; the screen preserved only the two baseline labels and added none.

BC-319 then ran under think-ykd6, with exp-148 registered under H-146. It keeps the five dots fixed, builds a reusable exact witness bank, and permits one surviving tuple check. Exp148 retained two exact witnesses before its seed deadline: 49,152 labels rejected, 16,382 nonbaseline labels remaining, no candidate attempted. H-146 remains unresolved.

Session120 continues the published work from Session119. Exp-148 was partial. The separate analytic transport rejects 61,440 labels for fixed D, leaving 4,094 nonbaseline labels. Exp-149 refutes H-147 at its first required direction: owner-000 has a positive exact uncovered area and a retained rational strict escape for the selected four-patch relaxation labelled by tuple \((0,0,0,7)\)$(0,0,0,7)$. This refutes fixed D as a cover of that relaxation, not the physical tuple. H-146 remains unresolved over other labels.

BC-320 then tested the saved escape and every one-site extension of fixed D on that same relaxation. Current evidence: exp-150 refuted individual-owner exclusion in the unchanged B-core model, with one frame-0 witness in each of four classes; exp-151 refuted the fixed sixth site; exp-152 accepted the necessary two-core screen; exp-153 is the completed refutation of every one-site extension of fixed D on the selected four-patch relaxation. exp-154 refuted H-157: six of its eight refined subclasses retain survivor weight ten, while two improve to \(19/2\)$19/2$. The two improved patches intersect their fixed target cores, so their old positive distance explanation was invalid; the six neutral children retain the reported positive distance. The corrected T1 and T2 statements concern the retained finite ray universe and the fixed patch-only residual domain. They do not rule out other angular restrictions, stronger domains, changed charges, or owner-selection routing, and they do not establish that the conditional strategy fails. Separately, the retrospective BC303 T1 literal replay rejects the named bottom-left role-C universal local surplus inequality: one admissible parent has closed labels \(\lbrace 3,4,11,12\rbrace\)$\{3,4,11,12\}$ and surplus \(3/800000 < \epsilon\)$3/800000<ϵ$. It decides no continuous-domain minimum, T2 forced-type case, global routing, or new \(s(11)\)$s(11)$ bound. Exp150’s compatibility result does not establish continuous unit parents or simultaneous owners, and exp153 does not exclude the physical tuple.

Session121 and Session122 are terminal. Session123 is terminal. Session124 resumed at 2026-09-10 01:52:40 UTC after the elapsed interruption. Its interpretation work and the BC-324 audit were subsequently completed and merged through PR139.

Historical interpretation selection: think-rm3k, BC-324, is complete. That factual block defined the terms used in the argument, separated exact computations from analytic implications, and audited the premises still required for a global result. The key routing obligation is

The record does not prove this statement. A reviewed two-attainer instrument is source ready but unrun; any future target needs a separate prospective registration and allocation. PR145 is ready after matching fast, page and full checkpoint validation. Historical status at that checkpoint: PR142 and PR137 were ready and unmerged. Both later landed with PR145/147 at 1c1db463.

The two-hour sprint in Agenda032 is complete. Exp141 independently confirmed the retained-family negative screens; exp142 completed the one-owner numerical comparison; exp143 found the four-owner five-dot candidate; exp144 checked those unchanged dots on all 361 canonical orientations. The footprint-containment and strict-core arguments supply the physical implication recorded as T-023. BC-316 subsequently completed the independent polygon-union audit in exp-145: all 361 exact deficits were zero. The saved-escape decision tree is now a historical decision record: exp150 took its compatible-owner branch, exp151 tested the selected sixth site, and exp153 closed the broader fixed-D-plus-one-site family on the relaxation. A global exclusion does not require every raw tuple label to be excluded. It requires the existential owner-selection routing statement above for every hypothetical physical packing. Any next experiment requires a fresh hypothesis or explicitly scoped successor, prospective criteria, published source, and a separate session usage interval. The figure and T-023 registration are post-sprint documentation amendments and are not charged into the frozen session113 receipt through 2026-09-09T05:16:31Z. The separate post-sprint usage delta was initially refused for non-monotone wait timing. The repaired meter retains that tail separately through 07:05:32 UTC, followed by Session114’s separate receipt through 07:53:52 UTC. The original Session113 receipt is unchanged.

PR137, on codex/n11-ownership-continuation, is ready for review and targets main. PR142 stacks the independent audit and overnight continuation on that milestone. PRs 116, 121 and 127 have merged; PR127 merged as 6aa9e72c. Session112 retains the earlier research continuation through 03:18:37Z; main’s independent font session111 retains its own identifier and receipt. Session110 and the handoff review preserve the original stack review and its separately tallied cost.

Full-support pricing H-135 remains an unrun reserve under think-7lp3. Exp134’s exact transport control passed with depth one and unchanged mass \(21342289572/2055263195\)$21342289572/2055263195$ in 135.91 seconds, but the pricing target was never invoked. Neither that administrative stop nor the deferred H-125 kernel is a negative scientific result. The owner-case continuation above takes priority.

Agenda 028’s restricted-family results. Session 092 and session 098 retain the independently reviewed work published on PR 110. The accepted results include the guarded central-parent exclusion, the signed short-slide exclusions, partial full-angle exclusions, exact counterexamples to the proposed disk and octagon capacity-six shortcuts, and the ten-square residual skeleton’s exact translation-fiber reduction. They apply only under their declared wall, contact, angle, or skeleton conditions and do not change the global \(n = 11\)$n=11$ bracket. The matched H-118 coupled-LP comparison and H-120 residual-family determination remain open, and Agenda 028 stays paused. Its dated strategy review records the evidence available before Agenda 030; the current selection above governs new work.

Agenda 030’s selection, made. Session-107 replayed the first wave’s three strongest claims with readers written from their statements, and all three agree: the segment cover at \(96/25\)$96/25$, the corner-pair containment theorem, and the band exclusion at grid 119. Two corrections came with it: the segment length threshold is in \((7/100, 8/100]\)$(7/100,8/100]$, and the cover’s certified domain now closes a far-wall sliver. BC-303 funds the segment cover toward an ownership argument as the next sustained block, with the \(B = 1\)$B=1$ depth polisher as the efficiency block and the plateau’s full-dual pricing as its first task; it retains the band ladder as filler and defers the corner-pair anchored certificate until the restricted fractional packing value is measured, since X-021’s duality lemma bounds any conditional certificate by it. Two more lanes ran and were halted by an external usage limit with their mathematics written and their validation unreached at that handoff: session-108 proves the grazing localisation of the escape class and records where exactly-one ownership fails (a segment can be shared, even by separated squares), and session-109 bounds the corner class’s surplus exactly at 1.6 to 1.8 per cent of the gap to the certificate line on its tested support. Its ratio optimum equals one on site set A; mark banking only proves an upper bound of one on other supports. Ratio and slice forms have the same exclusion power. Run 4 remained partial and run 5 never ran. The review also retracts lane E’s rounded-cover and enlargement helper claims while independently confirming E.4. BC-304 now closes the handoff before the funded continuation, as the owner requested. The same block repaired the deferred checkpoint (a third label-gated job for the slow behavioural lane and a declared budget for the escape screen) and amended OR-2, OR-3 and OR-6.

Atlas expansion to \(n = 324\)$n=324$, owner-directed, beside the research line. The plan under epic think-0juv and session-099 widened the frontier register and the known-best atlas from \(n = 1\ldots 100\)$n=1\dots 100$ to \(1\ldots 324\)$1\dots 324$, the end of the catalogue’s audited range, on PR 111. The unseen-corpus baseline is commit 6e21c4ca; the calibration-only layers stay pinned to the first hundred. The known-best-1-324 poster ships beside the untouched 1-100 figure, the prospective seed is retired to a pointer, and the sweeps tier is re-priced from measurement with two deferred steps. PR 111 landed on main at 28696526. The exact grid replay is also priced and deferred, with sampled replay retained on every pull request. The plan still records owner questions about the derived-facts retention route (D2) for the 123 catalogue cases, a caveated \(325\ldots 400\)$325\dots 400$ extension, and a 2x poster raster; merging this research line does not answer those questions or authorize an extension. PR 116 must obtain its own matching fast and deferred coverage after integration. This line does not preempt the research selection below.

Focused parallel strategy prepared. X-018 reviews PR108 and ranks the overnight opportunities: direct compatibility and complete restricted-family domains first, a bounded contact-release investigation alongside them, and shared-anchor correlation only on a diagnosed residual. Agenda 028 owns H-118–121 and BC-269–275 under epic think-pxv5; it preserves the X-017 allocation below and consumes its single BC-261 geometry interface. Both proposed agendas are paused, with no new target run launched by this planning. The live task Squares plan X-016 continues the source H-110 and conditional compatibility allocation independently; session-091 is already occupied there.

Independent alternative prepared. X-017 reconciles the contributed research packet with PR105’s committed state at 46f38ab4. Agenda 027 proposes resource-and-anchor and six-plus-five restricted-family pilots, with a separate pair-kernel discriminator. It is paused, with no target experiments launched. Its X-017, H-111–117 and BC-258–268 records and epic think-sz5t keep its ownership and numbering separate from the continuing agenda below. None of its dependencies requires that run to finish; the original handoff remains the entry for that run.

The next research phases run in PR101 on codex/post-381-next-phases, with the landed PR100 depth fixes and PR98 validation improvements integrated. Session 089 records live assignments and checkpoints; it was renamed from the branch-local session-088 to preserve the separate landed efficiency session below. Coordinator think-jgnv owns the integrated research line and its first two-hour checkpoint. Source controls have passed; independent review and bounded end-to-end target work remain distinct. Supporting fixes stay on this PR.

Efficiency implementation checkpoint. Session 088 records the bounded W5 slice: detailed timing artifacts, two independently guarded component optimizations, configuration-selection repairs, and integrated fast validation on main edccf294 plus the reviewed changes. Its 62 selected steps passed in 232.89 seconds on the recorded ten-CPU local host with two outer/two inner workers; this is a dated local measurement. PR98 retains the later hosted results and the checkpoint status as upstream work is integrated. The W5 plan links the measured results, retained profile, complete project documentation matrix, and upstream tbd proposal. Automatic exhaustive selection and evidence reuse remain planned.

Research continuation. The T+2-to-T+10 continuation addendum is the cold-review entry point for the partially completed post-T+2 continuation. The Agenda 024 allocation owns prospective priorities. Its planning block BC-250 links the tbd assessment of both prior reviews, and distills their directions into H-093–103 and the existing agendas. Coordinator think-jgnv next dispatches scalar BC-251, adaptive controls BC-231, density support BC-254, and restricted assessment BC-255 as capacity and their readiness conditions permit. The addendum owns command custody and recovery; no successor experiment started during the planning block. The user’s credit-interruption amendment excludes unavailable time from the wall allowance. The addendum records the accounting boundaries, revised deadlines, and conservative active-minute position 124:14, the inherited reference position for this continuation. Session089 is closed; no current active-time total is inferred from elapsed wall time. BC-232’s completed recovery produced no row-converged covering; BC-241’s independent local-scope review was published in ad600896. H-092’s fixed-weight refined-core negative passed independent review and awaits integration under think-xsma. The eventual handoff records the active minute actually reached. The addendum preserves the first block’s frozen packets and binds the active-time, role, safety, BC-241, BC-232, BC-243, and gate contracts. Agenda 024 remains its control plane. It coordinates two disjoint programs: the exact fractional frontier in agenda 025 and density, typed stationarity, and Trump capture in agenda 026.

Research and tooling have separate continuation work. Session 087 completed Session 086’s BC-213 rung and accepted H-062 at bracket width \(0.015\)$0.015$. Session 089 retains the finite-row density candidate, its complete pair exclusion, the exact-angle auxiliary result, and the next complete-method assessments.

BC-264’s entry: think-mq0d retains BC-264’s disposition after the completed H114 feature and kernel-contract pricing. Its immediate prerequisite is the stopped Session097 checkpoint’s operational certification and draft publication. Exp129 missed its launch cutoff; its expired allocation cannot authorize a scientific invocation.

Session097 completed that pricing on codex/n11-kernel-pricing, following the user’s request to continue. Independent reviews accept an exact obstruction to cubic center features and the design of a finite test for one richer family. Independent source-free code reviews admit its LP proposer and exact reader; all 75 controls passed. Exp129 closed as blocked when protocol admission was incomplete at the September 7, 22:20 UTC launch cutoff. The engine push passed, but the protocol records and push checks failed on a stale round-count control anchor. No scientific source or packet was constructed, no target solver ran, and no result directory was created; scientific execution time is zero. The dependency guard gives no mathematical verdict on H125 or continuum certificate. Its new checkpoint is separate from the completed eight-active-hour block.

Session096 reviewed Stromquist’s three memos, corrected the paper’s chronology and five case-proof descriptions, and independently checked a five-dot obstruction and the local segment helper. Its source brief retains the remaining geometric replay under think-0krc; the selected target-research entry remains BC-264. All 66 full-checkpoint steps passed at dd92b2a0.

Session105 follows the author’s clarification about \(n=26\)$n=26$. Its verification report checks Stromquist’s historical packing exactly and confirms that Friedman’s current upper bound is smaller. A scoped support argument closes rigid central-block rotation with two fixed corner separations. Green’s stronger source-reported lower bound is now recorded separately from the verified one at \(n=26\text{–}27\)$n=26\text{–}27$; proof recovery is think-0x08, the remaining source-table audit is think-4g6w, and think-z0fi implements and controls the specified contact-release family. The MacIver review adds three previously unindexed manuscripts. His reported lower bound at \(4.450208382\ldots\)$4.450208382\dots$ is below the verified bound at both n17 and n18. The missing computational artifacts remain a source gap; think-sske owns local replay of the center-area and capacity lemmas before adoption. Exact design controls show potential local cuts, not a new global bound. This source review does not authorize further kernel research.

Session106 extends the source-table audit through n324 and corrects 56 additional reported lower bounds, preserving every verified bound and every upper bound. The dated n26 search finds no smaller packing among the checked public sources; exact normalization shows that two recent numerical submissions are slightly worse than Friedman. This is a best-known conclusion with recorded search limits, not a proof of optimality.

The Session094 handoff was updated after the first result in Session095. Exp125 independently certified the entire diagonal compatibility branch, but its axis representation returned no_chain. Exp127’s fixed collision-augmented axis cover also returned no_chain, in 0.25 seconds, without an independent reader. H124 and restricted H036 remain unresolved; that representation receives no retry or parameter sweep. BC-259 is complete: exp128 independently bound all 88 source images, 60 placements and eight orbits, verified 41 strict inclusions on seven fixed boxes, and established the attained support optimum eleven in 1.12 seconds. H099 is refuted only on that support. BC-265’s independent designs derive an explicit mass-eleven calibration on the old support, but a new undercovered pose would reject only that density. Session097 completed the selected BC-264 pricing and kernel-specific BC-260 review. Its reviewed source-free instrument targets the fixed family in H125: an exact finite obstruction would reject that family, while feasibility of the outer LP proves nothing about a complete kernel. Exact PSD evidence and complete pair-domain verification remain prerequisites for a positive continuum certificate at side \(96/25\)$96/25$. H101’s stronger common-support obstruction is a conditional fallback, with no candidate asserted. Exp129’s blocked, never-invoked outcome is retained in Session097. Any future scientific attempt needs a fresh bounded allocation and admission; repairing the publication control does not reopen exp129. Session 090, under think-9qrx, completed the user-approved research block after PR 101 merged. BC-251/exp-116 finished unresolved: no row convergence, and an independently replayed dual mass of about 10.080180 at depth one, below the obstruction threshold. No bridge or unchanged retry is selected. At that earlier checkpoint, BC-243’s uniform control had timed out on three separately reviewed algorithms. Session094 later completed all five repaired graph controls and ran exp126 once. Its graph-only obstruction left H099 unresolved; no retry is open. BC-255 accepted H-106’s full continuous near-axis ten-point clause through an independent exact rectangle reader. H-108 and H-109 also accepted canonical near-45 A3 and A1/A2 forcing through independent exact replay and a reviewed reflection. These are restricted-theorem auxiliaries, not a packing bound. H-110 is accepted through exp-121: the fixed unit square is independently verified to fit in the actual domain and strictly avoid all twelve marks. This refutes the unchanged unconditional P12 auxiliary, not H-036. Exp-122 refutes H-122’s small-diamond conditional cover through an independently checked square. Exp-123 accepts complete near45 localization through four exact continuous guards and the reviewed geometric reduction. The fixed-S H-124 screen found no witness without certifying continuous coverage; the broader bound is unchanged. At Session090’s earlier allocation, H-107’s reviewed fixed-site scalar protocol was held out of that two-hour block under paused think-7fec; later-session reconsideration preserves its unlaunched history. The freed attention went to a bounded conditional-compatibility assessment from the accepted A-point lemmas, not an automatic P12 repair. Full validation of research checkpoint 99a3ad42 passed; Session 089 retains that verdict and the completed experiments, which must not be repeated. Agenda 024’s Current Allocation owns the scalar, complete-density and continuous-angle packages, including independent-review assignments. Keep these on one integrated successor PR from codex/structural-compatibility-continuation, based on merged PRs 105 and 106. The earlier BC-215 efficiency work remains available in Agenda 023; this handoff does not mark it complete or erase its evidence. BC-219 was the preflight for Agenda 024’s original launch inputs. Its completion does not replace the continuation addendum’s current gate contract.

The completed commissioning slice consumed the first two active portfolio hours of the same roughly 24-active-hour agenda. It exercised the coordinator, both managers, one floating worker, retained-state resume and checkpoint seams, the local Trump theorem packet, central integration, and interruption recovery. The T+2 integration checkpoint left 22 active portfolio hours; the continuation resumes those cells without resetting their clocks or budgets.

At the historical T+0 launch, the only takeable research cells were BC-230, BC-232, BC-233, BC-240, BC-242, and BC-245. Agenda 024’s current allocation now governs which cells may run. The coordinator alone allocates experiment IDs, edits shared or generated records, integrates manager packets, and moves a gate. Codex uses max reasoning for theorem scope, proof boundaries, mathematical disposition, and strategic routing; bounded implementation and independent reviews use xhigh, while replay, manifest, formatting, and value checks may use high when they require no mathematical choice.

Agenda 021 supplied the retained T-021 result and the 3.82 fractional state used here. Agenda 022’s Session 087 closed after PR 83 merged and the full gate passed on main. Agenda 024 is a separate portfolio; its active-hour clocks and T+2 disposition do not resume the completed efficiency block.

PR 93 subsequently landed two operational guards on main without changing this research entry point. The on-demand deep-gate.yml runs the 11 deferred steps in four jobs against a pull request before merge; because it is advisory, the post-merge full gate remains the backstop for a pull request that does not request it. The push-triggered branch-mergeability.yml now reports a branch that cannot be merge-built even when GitHub cannot create its pull-request merge ref. Its remaining blind spot is an idle branch after main moves and before the next push. Session 087 retains the full-gate evidence from run 34010683180 at c743d7bb.

The later upstream efficiency corrections preserve that historical accounting. Session 087 reduced the then-required CI surface from 1369.60 s to about 221.70 s without removing checks. Exact-tree reuse is now fail-closed. A matching successful packing-required proof lets the post-merge integration job omit only explicitly allowlisted tree-pure fast steps; deferred and unclassified steps still run, and any lookup or proof failure repeats the complete surface. The work was motivated by the earlier measurement that 20.2 percent of deep-run work repeated and 92 percent of that repetition came from unchanged trees. Per-test CPU readings are diagnostic because child costs cannot yet be attributed reliably; the 12 s call-wall backstop remains enforced. D-472 records why one hosted timing sample cannot establish a speedup. Development’s validation tiers own the current configuration and measurements; none of these historical selections supersedes Agenda 024’s allocation.

Earlier Handoffs

Open the house rendering of the retained 100-square witness.

The renderer’s standing exact-motion control remains independently replayable:

As of 2026-08-30. agenda-008 is closed with all four commitments terminal; session-045 then ran nine unplanned phases on BC-049 at \(n = 40\)$n=40$ and carries a handoff at its end that is the authoritative summary, and session-046 took the cheapest thing that handoff named. session-047 then left the mathematics alone and worked on the record itself: it promoted the three sizes whose exact certificates were already running in this gate while their records denied one existed, and filled in the two facts the register could not previously state — whether anyone here has read an external argument, and what a novelty claim was searched against. session-048 closed the same gap one level up, joining every session to what it cost and finding that both obvious ways of totalling that were wrong in the flattering direction — see Sessions Conducted. session-049 then did three things in one morning: reconciled the queue against the tree (BC-085 and BC-087 had landed while the agenda still advertised both as ready), built the pre-push floor BC-086 asked for (packing-validate --push, 58s against --fast’s 646s), and ran the BC-088 reassessment whose sequenced plan is X-009 — then executed that plan’s first block: twelve verified ceilings moved off the integer grid onto exact sides at \(n = 18, 19, 26, 27, 38, 52, 66, 67, 82, 84, 85, 86\)$n=18,19,26,27,38,52,66,67,82,84,85,86$, every one decided by exact sign — ten over \(Q(\sqrt{2})\)$Q(\sqrt{2})$ and the last two over \(Q(\sqrt{7})\)$Q(\sqrt{7})$, the first exact verification outside \(Q(\sqrt{2})\)$Q(\sqrt{2})$ — from a published rule or a coordinate lift, about \(3.2\)$3.2$ of aggregate gap. The widest trailing ceiling is now \(n = 50\)$n=50$’s \(3/7\)$3/7$.

session-050 then performed the independent audit exp-045 had waited on since registration, built the -W bridge that makes the accepted helpers corroborate the certificate, and recorded the owner’s acceptance — clearing the gate that held BC-010 and BC-029.

Queued for the next run: agenda-010 — the two-lane overnight program from X-010: nine hours in blocks of two to three hours, instruments before research in both lanes, a checkpoint (BC-098) resequencing the tentative half mid-run, and the standard unattended rules stated in the agenda’s own objective. The run is live: blocks 1 and 2 are complete — session-054 landed the certifier core and the falsifier (BC-093, BC-094; the session ran as 050 and was renumbered at the merge — the audit session above holds that number), and session-051 landed the stage-1 price and the exact-LP measurement (BC-095, BC-096) — and the checkpoint (session-052) has resequenced the tentative half; session-053 closed block 3 on BC-099 under think-1o1f with the run’s first research result: Bentz 2010, Theorem 8 (\(s(46) = 7\)$s(46)=7$) machine-certifies as printed — 92 exact cells over \(Q(\sqrt{2}, \sqrt{3})\)$Q(\sqrt{2},\sqrt{3})$, the Lemma 5 threshold by a rigorous rational subdivision bound of \(0.955390\)$0.955390$, all 45 points charged — held unresolved with needs_review under the unattended rules that night (resolved by the review below), with the \(m = 4\)$m=4$ remainder typed on think-1o1f and one candidate printed gap flagged for replay. The same session absorbed a mid-run merge from main (the parallel audit session had taken session-050 and D-404, so block 1’s record is session-054 and the reassessment defects are D-405/D-406) and root-caused the base branch’s red full surface to two stacked control defects, D-407 and D-408, both fixed on this branch. Block 4 is complete too (session-055, BC-100): the H-044 chunk-expressibility verdict exists as exp-046, exploratory by the hypothesis’s own calibration-only amendment, held unresolved with needs_review that night (resolved below) — the criterion is missed under both denominator readings the registered text supports (23/30 = 0.7667 over all records at \(n \le 30\)$n\le 30$; 3/10 = 0.30 over the non-grid sweep records), identically in both bands, every miss typed and determinate. The measured mechanism: the lattice grammar expresses the grid stratum completely and the tilted stratum not at all (flush groups are tangentially slid off the integer lattice step), so stage-1 over this grammar is a restricted-class instrument — converging with BC-095’s repricing from the price side. Block 5 closed (session-056): BC-099’s own question continued under think-1o1f — the m = 4 foundation layer. Two results landed on first complete runs, both held that night for review (resolved below): Figure 2’s sixteen-point base configuration is machine-certified (30 exact rational cells: 4 Lemma 1 corner pentagons, 8 Lemma 4 wall rectangles, 18 Lemma 2 triangles; 16/16 charged), and Lemma 10 is machine-settled both ways — the printed replacement point \((1, 1.74)\)$(1,1.74)$ is refuted by an exact escape certificate, and all three corrected replacement sets (\((1.12, 1)\)$(1.12,1)$, \((1.74, 1)\)$(1.74,1)$, (1.87, 0.76)) certify exactly, their Lemma 5 quadrilaterals landing inside the very parameter families the paper’s Section 1 lists. The certifier gained subset semantics, margin and near cells, and the rational-a threshold bound along the way. Block 6 (session-057, BC-101) then moved the verified lower lane for the first time since 2005: \(s(17) \ge 17/4 = 4.25\)$s(17)\ge 17/4=4.25$ and \(s(18) \ge 17/4\)$s(18)\ge 17/4$, certified exactly by a sixteen-point unavoidable set in \([0, 17/4]^2\)$[0,17/4{]}^2$ (cases/green17) — above Nagamochi’s \(\approx 4.1623\)$\approx 4.1623$, below Green’s unadoptable \(\approx 4.4452\)$\approx 4.4452$ — the cell plan pinned to \(17/4\)$17/4$ by an \(11/1000000\)$11/1000000$ slack, the falsifier corroborating by saturation, and the verdict held that night for review; the review’s independent audit then showed \(17/4\)$17/4$ was the plan’s ceiling rather than the set’s, and the upgrade below carries the adopted bound. The run then discharged the checkpoint’s two authorized fillers and closed early. Session-058 (BC-103) sized the \(m = 8\)$m=8$ attempt exactly and parked it: the m = 7 pattern’s ceiling \(7\sqrt{3}/2 + 2\sqrt{2} - 1 \approx 7.8906\)$7\sqrt{3}/2+2\sqrt{2}-1\approx 7.8906$ sits below both side 8 and the standing \(7.9282\)$7.9282$ at \(n = 61\)$n=61$, with the lattice dilemma exact (8 rows overrun the Lemma 2 pitch cap by \(0.0157\)$0.0157$; 9 rows overrun the 60-point budget by 7). Session-059 (BC-102) built the τ* pilot and read the method diagnostic: the eleven-crossing sits near side \(3.83\)$3.83$ (uncertified, typed), so a pure eleven-point set has at most a \(\sim 0.04\)$~0.04$-wide window above \(2 + 4/\sqrt{5}\)$2+4/\sqrt{5}$ and any ambitious bespoke \(s(12)\)$s(12)$ bound forces the threshold/segment/moving-resource machinery. Everything mathematical from the run was held unresolved with needs_review overnight per the unattended rules; the verification review below resolved every hold the same day.

As of 2026-08-31, evening. The owner moved the review from their queue to the repository’s own rubric — determinations, not deferrals — and session-060 is running it as BC-106 under think-ngf0 in agenda-011. The determinations, each grounded in conventions.md §4 and the frontier evidence contract: Theorem 8’s audit is verified and fully machine-checked (E-bentz46-theorem8-audit); the Lemma 10 settlement is verified and now source-settled — the published page image itself prints the transposed \((1, 1.74)\)$(1,1.74)$, so the defect is the journal’s, recorded as defect-found on E-bentz-2010-proof with the partial Theorem 9 audit in E-bentz13-figure2-audit; exp-046’s hold is cleared with H-044 undisposed by its own registered amendment (the miss is determinate under both readings); the m = 8 parking statement stands as exact arithmetic; the τ diagnostic stays uncertified by construction* — final typed status, nothing pending. The green17 determination became an upgrade: the independent interval certifier built for the review (cases/green17/interval_audit.py — exhaustive exact integer branch-and-bound over the full pose space, pair-handoff and wall-tightened discharge rules, negative controls refuting tampered sets and oversized sides with exact witnesses) proved the run’s \(17/4\)$17/4$ was the cell plan’s ceiling, not the set’s: the same sixteen points certify at \(4426213/1000000 = 4.426213\)$4426213/1000000=4.426213$, the cell certificate was rebuilt there (right-wall Lemma 4 rectangles replacing the near-slabs), and verified_lower_bound at \(n = 17\)$n=17$ and \(n = 18\)$n=18$ moved to \(4.426213\)$4.426213$ on two independent formal methods (E-green17-sixteen-point-lower, E-green17-interval-audit), the set’s exact ceiling \(753/250 + \sqrt{2} \approx 4.42621356\)$753/250+\sqrt{2}\approx 4.42621356$ bracketed by certification at \(4.426213\)$4.426213$ and refutation at \(4.427\)$4.427$ and typed as follow-on. The assembled case is the 2026-08-31 verification review under docs/project/reviews/; the owner reviews the PR as a whole. Follow-ons stay on their beads (think-1o1f, think-q6vy, think-07t7 paused, think-0z9b); BC-097 and BC-089’s remainder remain the sanctioned gate filler.

Session 061 summary. The review’s epistemics became infrastructure: verification is the highest rung supported by the evidence a result cites, regardless of who performed it; confirmation records what this repository has read, replayed, or established. Session 061 codified that distinction as BC-107 under think-n8vl in agenda-011, a pipeline-improvement slice. epistemics.md at the repository root now owns the four axes — V0–V5, C0–C5 with structural promotion checks, anchored significance that never gates, and a scoped novelty classification — and the results register (packing/frontier/results.yaml, rendered as RESULTS.md) declares the whole results T-001–T-016, whose declared rungs devtools/check_results.py checks against cited evidence, required notes, and review metadata on every validation run. Unsupported promotion and unexplained understatement fail the build. The register subsumes the review’s determinations (the \(s(17)\)$s(17)$/s(18) upgrade is T-001/T-002 at V4/C4) and the legacy first-party theorems (the Stromquist repair is T-010; this document’s own T-1–T-4 below remain declared shorthand). softschema is upgraded to 0.8.0 across the schema toolchain in the same slice. The one-shot post-merge check found main’s full surface still red on one negative control, behind the same mask D-407 named: the worker-snapshot link copy covered the pruned archive but not the pruned renderings, and the control’s expected message lagged the ledger’s round count — fixed as D-409 and D-410 on this branch, with epistemics.md added to the snapshot’s root documents before the same gap could ship again. Research follow-ons are unchanged on their beads.

As of 2026-08-31, late evening — historical agenda-012/013 launch record. X-011 reconciles the new \(n = 17\)$n=17$ weighted certificates, the \(n = 68/69\)$n=68/69$ precision gap, the medium-case construction ladder, and the opportunity cost of a thirteenth open-ended \(n = 5\)$n=5$ round. Agenda-012 turns that synthesis into three disjoint first-wave blocks with real beads and 15--30 minute check-in cells: BC-108 runs an independent-implementation agreement check on the proposed \(4.5058\)$4.5058$ certificate while naming shared assumptions; BC-109 builds the hash-verified parent-child serialization bridge at \(n = 68/69\)$n=68/69$; and BC-110 decides whether \(n = 50\)$n=50$ can become the rational exact-promotion control. They were scheduled to run in parallel, followed by BC-111’s bounded checkpoint. The dependency-linked successors are already filed. Agenda-013 is the owner-authorized nine-hour execution graph on one pull request: 150 minutes for those three first-wave blocks, a 15-minute W5 efficiency checkpoint, 30 minutes for BC-111, 180 minutes for one positive or refusal-path continuation per lane, 30 minutes to measure throughput again and freeze review packets, 90 minutes for three independent reviewers, and 45 minutes for synthesis and final validation. Every wave boundary requires a commit, tbd and generated-view reconciliation, validation receipt, push, and PR update. Existing BC-010 gets one final 90-minute discriminator with a matched \(n = 10\)$n=10$ transfer under dedicated bead think-iivb. Its first cell freezes both fixtures, the observable, threshold, and refusal conditions before measurement. Only a passing transfer may remove BC-011’s blocked hold; a refusal stops the dedicated BC-011 through BC-014 chain and parks H-023. Legacy owner think-1s0h is not the queue gate. Those launch instructions are retained as chronology; use the Current Handoff for the live entry point.

The parallel recognition slice remains BC-089 on think-d0j1 in agenda-009: agenda-012 transfers \(n = 50\)$n=50$ to BC-110, leaving thirteen disjoint cases on BC-089; \(n = 54\)$n=54$ follows only if that result shows nested-radical representation is the next missing seam. The robust-rational sweep and typed \(n = 53\)$n=53$ refusal remain on the parent bead. BC-049 on think-xdly is the research cell all of the mathematics below sits under, and it stays open.

\(n = 40\)$n=40$ is infinitesimally flexible, exactly, over \(Q(\sqrt{2})\)$Q(\sqrt{2})$: seven retained directions turn the sixteen squares of its tilted block and leave the frame fixed, and every one is refused at second order by a verified self-stress. The property stays undetermined because an infinitesimal flex is not a motion — the gaps curve shut at order \(t^2\)$t^2$ — so what is settled is that no first-order argument can establish rigidity there. Getting further needs an instrument this repository does not have: the cone is bounded to dimension 45 against six dimensions of anything found admissible, and closing that gap means reasoning about \(2^{42}\)$2^{42}$ corner disjunctions without enumerating them.

The correction underneath it generalized. Göbel’s published family is exactly the best known at \(n = 5\)$n=5$, \(40\)$40$, \(65\)$65$ and \(89\)$89$; all four now have exact constructions here, and the last two turn out to be what their retained decimal witnesses were all along — agreement to \(5 \times 10^{-33}\)$5\times {10}^{-33}$ identifies rather than merely permits. \(n = 28\)$n=28$ is the near miss that stops the obvious guess: the family gives it a valid packing \(0.004\)$0.004$ worse than the best known, whose optimum is at algebraic degree 6 and is not in the family at all. Take the next slice from agenda-map.md.

BC-017 delivered its readiness input and stopped there. The \(n = 3\)$n=3$ full-cell control already retained the target-free execution-plan receipt the commitment asked for, so the slice produced what that receipt authorizes instead: on the same three-square subject the structural plan reports 4 seated-wall equalities and 8 open-wall inequalities against 2 contact equalities and 1 non-edge inequality, while solve_cell builds 12 containment rows and 3 pair rows — the same twelve and the same three. Every total agrees and every composition does not, so the LP-solve half of the exit is reachable and pair_tests does not transfer between instruments that both report it.

BC-019 is closed. The contact-assembly contract is at contact-assembly-v2-draft and carries the clause it never had — 17 certificates and 13 typed limitations over \(n \le 30\)$n\le 30$ — with the missing grammar move named rather than guessed: a primitive for axis-aligned polyominoes that are not a bar, rectangle or corner L. BC-024 is what made that safe to say: X-008 measures that every component the grammar cannot express is axis-aligned — every other-polyomino in the corpus has angle exactly zero — so all 295 tilted components are already covered. Wall seating splits the residue into two populations with nothing between them: 44 whole-record grid subsets on four walls, 65 corner-seated blocks on two. BC-038 is closed and rejected on measured arithmetic — 35 evaluate_stress calls arrive with eleven distinct number fields, and RowJetInventory refuses a foreign field by identity, so the floor is a 1.54x ceiling against an exit wanting five-fold. BC-010 and BC-029 were gated for four days on independent acceptance of exp-045’s preregistered criterion, which an unattended runner may not grant to itself; on 2026-08-31 the owner accepted the round after session-050’s independent audit (findings and the corroborating -W bridge are the experiment record’s Amendment and D-404), so exp-045 now records decision: accepted, BC-029 is complete, and BC-010’s readiness on the map is genuine.

\(n = 5\)$n=5$ is second-order rigid, and that is a first-party result. X-007 settles the question BC-049 asked, exactly, over \(Q(\sqrt{2})\)$Q(\sqrt{2})$ at Göbel’s construction rather than at the retained decimal witness — which is \(2.4 \times 10^{-30}\)$2.4\times {10}^{-30}$ off the diagonal and so infeasible at the scale a certificate works at. The cone of infinitesimal motions is exactly the line spanned by rotation of the middle square; the other fourteen coordinates are pinned by Farkas certificates verified in the field; and that one direction is refused at second order by a verified self-stress. This confirms and strengthens the numerical account BC-069 reached from the promotion side, including its observation that the contacting corner sits at the midpoint of the contacted edge — which turns out to be the reason for both the first-order blindness and the second-order obstruction.

The frontier property stayed undetermined then, and the reason is worth carrying forward: second-order rigidity is not local rigidity, the step that would close the gap is a curve-selection argument that X-007 writes out as prose and no replay checks, and the property enum has no word for what was actually established. What did change is everything saying why — verified rather than numerically-checked, exact-algebraic rather than numerical-multiprecision, and a first-party evidence id in place of the screen’s — which takes \(n = 5\)$n=5$ out of the assessment tool’s ownership, so it joins \(n = 11\)$n=11$ as left to a stronger argument. Both D-354 guards stayed green without being edited, which was the test the change was held to.

For \(n = 5\)$n=5$ that stronger argument arrived on 2026-09-03. BC-152 wrote the curve-selection step out in full and checked it against an exact accounting of all 400 local inequalities, BC-153 reviewed it independently, and the property now reads locally-rigid at fixed side on a second first-party evidence record — see T-014.

Read OR-4 before trusting any older queue. BC-081 found that agenda-005 was advertising four commitments as takeable which agenda-006 had already discharged, and four more blocked on conditions no reader could observe. That is D-374, and the repair is agenda-map.md, generated from every agenda and drift-checked in --records at 0.14s. It is the queue now; BC-010 maps to its dedicated think-iivb gate, while think-1s0h remains the broader H-023 research owner.

The identity question moved twice, and both moves were corrections. X-005 still declares contact + closure the relation the atlas should count, but D-375 records that it had scored the atlas’s own relation at the wrong level — both of that relation’s inputs are canonical under relabelling and D4 by construction, so it is a quotient statement, and the \(n = 4\)$n=4$ labelled control it was refuted on can refute no relabelling-invariant relation at all.

X-006 then answers the question this handoff previously posed. \(n = 5\)$n=5$ does admit a discriminating control, and it is the pair D-034 has been quoting since 2026-08-23 without ever retaining: two endpoints sharing a contact certificate, differing in geometric key, at a side difference of \(8.9 \times 10^{-16}\)$8.9\times {10}^{-16}$. It is retained now, and it discriminates whichever way its component count resolves — the branch where the count is two refutes contact + closure itself. What it waits on is that count, and exp-042 already names the missing claim: A_to_B_stationary_connection, first of its eleven declared scope refusals. D-034 stays outstanding, and no proof obligation shrank.

Everything below this paragraph is the accumulated record of how the program got here, not the next action; agenda-005 is closed and appears in it as history. Block A is closed: BC-047 under think-y85e and BC-042 under think-zmh8 both met their declared exits in session 035, which is terminal. Precision is now manufactured in-repository rather than read off a source — the published \(n = 29\)$n=29$ system refines to 1000 declared digits with a reported residual bound of \(1.09829 \times 10^{-1039}\)$1.09829\times {10}^{-1039}$ — and the \(n = 29\)$n=29$ contact structure is frozen with 89 incidences, six orientation classes, an empty ambiguity report and \(97.5013\)$97.5013$ decades of separation, with the same extractor reproducing the known \(n = 11\)$n=11$ structure exactly under exact arithmetic. BC-045 is now closed at all four phases, in session 036 and session 037, under agenda-006. The interval route is built, calibrated against \(n = 5\)$n=5$, \(n = 10\)$n=10$ and \(n = 11\)$n=11$, and run at \(n = 29\)$n=29$, where it certifies \(s(29) \le 5.93383346267692918974379895098\)$s(29)\le 5.93383346267692918974379895098$ at a declared relaxation of \(10^{-20}\)${10}^{-20}$. That certificate is retained unresolved with needs_review: true and promotes nothing: it sits \(5.23371 \times 10^{-5}\)$5.23371\times {10}^{-5}$ below the standing verified ceiling, and whether it moves verified_upper_bound is a reviewed human decision through the evidence contract. BC-054 is closed in session 038: contacts now identify which features meet, and assembly turns a structure into equations that vanish at the packing they came from. Three findings there went against the promotion spec — counting rows cannot say whether a system determines the pose, an angle class does not license an angle identity, and seven of the \(n = 29\)$n=29$ squares are reflected and refused by name. The rank half of the first was later found to be measuring a bug rather than the packings: see the BC-059 paragraph below and D-361. BC-056 closed that first stretch, and the run then resumed rather than ending: a review of the commit timestamps showed it had misread its own clock and stopped with most of its budget unspent (D-358). BC-057 is closed in session 039, which built the interval checker and recorded the \(n = 29\)$n=29$ certificate as evidence without promoting it. BC-058 is closed in session 040: a pose is now a centre, an angle and a chirality, so the reflected squares are assembled rather than refused and the \(n = 29\)$n=29$ residual falls from \(2.0\)$2.0$ to \(1.3 \times 10^{-15}\)$1.3\times {10}^{-15}$ with the \(n = 11\)$n=11$ calibration unmoved. The feature-renaming cost that commitment was written to weigh was not paid — reflecting the local axis leaves the corner indices alone. BC-059 is closed in session 041, and the answer was that there were no stationarity conditions to derive. The shortfall close had been reporting — four at \(n = 11\)$n=11$, seven at \(n = 29\)$n=29$ — was a bug in assembly rather than a property of the packings: an edge-edge contact was written as one equation where collinearity in the plane is two, which left one square free to pivot about the shared point and drive its neighbour open at first order. With both endpoints of the edge on the line the contact Jacobian reaches full rank at both sizes — \(34\)$34$ of \(34\)$34$ at \(n = 11\)$n=11$ and \(88\)$88$ of \(88\)$88$ at \(n = 29\)$n=29$ — residuals unmoved at \(8.9 \times 10^{-16}\)$8.9\times {10}^{-16}$ and \(1.3 \times 10^{-15}\)$1.3\times {10}^{-15}$, and close now refuses at both. It is D-361, class soundness, direction conservative: it made the pipeline look further from a solvable system than it was. Göbel’s \(n = 5\)$n=5$ has no edge-edge contact, is untouched by the repair, and kept a genuine shortfall of one. BC-069 closes it, and the answer corrects the form the pipeline had been promising. The condition is not first-order: side_leak reads \(1.00 \times 10^{-16}\)$1.00\times {10}^{-16}$ there, so “no admissible motion decreases the side” is already true and adds a dependent row. The single free direction is a rotation of the centre square about its own centre, and the contacts fail along it at \(-0.25 t^2\)$-0.25t^2$ in both signs — an ordinary second-order obstruction, so the pose is infinitesimally flexible and second-order rigid, and the shortfall is a degenerate root rather than an unpinned optimum. Differentiating the contact map along that direction takes the rank to 16 of 16 with the residual unmoved at \(1.11 \times 10^{-16}\)$1.11\times {10}^{-16}$, and each emitted condition expands to exactly the statement that the contacting corner sits at the midpoint of the contacted edge — an identity of the corner-edge contact type, checked against a midpoint expression written independently of the derivative. Both determined sizes are unmoved. The misnaming is D-363. BC-060 is closed in session 042, with one answer and one refusal. At \(n = 11\)$n=11$ the promotion spec’s frozen margin rule recovers Trump’s published degree-eight minimal polynomial from digits alone — \(C = 12420\)$C=12420$, \(B = 36.85\)$B=36.85$, \(M = 200\)$M=200$, a relative residual of \(4.99 \times 10^{-338}\)$4.99\times {10}^{-338}$ at \(B + M\)$B+M$ still falling to \(3.38 \times 10^{-412}\)$3.38\times {10}^{-412}$ at \(2B + 2M\)$2B+2M$ — and discharges it as irreducible over \(Q\)$Q$ with an isolating interval containing the refined value. At \(n = 29\)$n=29$, on a thousand digits with a reported residual bound of \(1.09829 \times 10^{-1039}\)$1.09829\times {10}^{-1039}$, pslq returns nothing at any degree from 2 through 20 below a coefficient bound of \(10^{22}\)${10}^{22}$: not one degree reached a clause. The contrast is the finding, because the planning probe on the ~98 serialized digits got relations at almost every degree from 8 to 21. A search that answers when under-fed and falls silent when fed properly is evidence about the number, and what it bounds is concrete: if the Kingbird solution has degree twenty or less, some coefficient of its minimal polynomial is at least \(10^{22}\)${10}^{22}$. That is the measured reason the interval route carries the \(n = 29\)$n=29$ bound. BC-065 is closed in session 043, and it says how to read that refusal. Under \(u = \tan(\theta/2)\)$u=\tan (\theta /2)$ the published system rationalises over \(Q\)$Q$ into six polynomials with total degrees \([11, 15, 10, 15, 7, 6]\)$[11,15,10,15,7,6]$, so the Bézout bound on the solution variety is \(1{,}039{,}500\)$1,039,500$: degree twenty surveyed a corner of the space, not the space. Every equation is degree one in \(s\)$s$, and solving the smallest for it gives \(s\)$s$ as a rational function of two half-angles alone, leaving five equations in five unknowns. Eliminating those is where the exact-algebraic route either succeeds or is shown to be out of reach at \(n = 29\)$n=29$, and it is left to its own budget on think-obgk. The bound reads as “not small” rather than “this large” — Bézout is loose for a structured system. The next slice is BC-066 under think-obgk — eliminate the five equations in five half-angles that BC-065 left, inside a declared cap, because it is the only remaining block that can change what this run concludes about \(n = 29\)$n=29$. BC-061, BC-069, BC-067, BC-068, BC-062 and BC-063 follow, with BC-064 reserved and last; the ordering and its reasons are the continuation schedule, and run-002 carries what a fresh agent needs that the diff does not show. Session 044 is terminal, and closed eleven commitments.

The next slice is BC-074 under think-eb29, and it is a documentation-pass. That workflow — W8 — is new, added because this run demonstrated the gap it fills: the record moved a long way in a day while the front door did not move at all, and nothing in the gate noticed. check_synopsis binds this document to the artifacts; there is no equivalent for README.md or TUTORIAL.md, so they drift silently. Its checklist is the documentation-pass runbook, and its one hard rule is that it reconciles rather than authors: a claim the record does not already carry is not a documentation change, and a disagreement the artifacts cannot settle is a defect rather than a rewrite. D-367 is what the alternative looks like.

BC-066 attempted the elimination and reached a measured wall rather than an eliminant, which is the exit that commitment names. Three msolve runs on the six-equation system: over \(Q\)$Q$ in an elimination order, F4 was OOM-killed at degree 32 after 25m09s with 13.8 GB resident, having completed degree 31 on a \(656126 \times 1670545\)$656126\times 1670545$ matrix; mod \(1073741827\)$1073741827$ in the same order the matrix dimensions were identical degree for degree; and mod the same prime in plain grevlex — an order of magnitude cheaper per matrix — the pair list still grew monotonically to 21,661 with no basis inside a declared 25-minute cap. Neither predicted failure mode is what stopped it. Coefficients cannot swell over \(F_p\)$F_p$, and the cheapest monomial order did not terminate either, so what the runs measure is the size of the ideal rather than the arithmetic carried through it. The claim is narrower than “out of reach”: two threads and 15 GB is not a proof of intractability. What it establishes is that the interval route carries the \(n = 29\)$n=29$ bound for a measured reason, and that the next thing to try is a smaller question rather than a bigger computer.

That is BC-070, and its first half has landed. Homotopy continuation needs no basis at all, and the mixed volume of the Newton polytopes bounds the isolated solutions at \(15{,}744\)$15,744$ — sixty-six times tighter than the Bézout bound of \(1{,}039{,}500\)$1,039,500$, computed in nine seconds. The stable mixed volume is equal to it, so the bound covers every isolated solution rather than only those in the torus. So the Kingbird solution has algebraic degree at most \(15{,}744\)$15,744$. Kingbird’s, not \(s(29)\)$s(29)$'s: \(s(29)\)$s(29)$ is the optimum, Kingbird’s packing is the best known and is not proved optimal, and the bound gap there is about \(0.46\)$0.46$. That is still far beyond what an integer-relation search can reach, and saying otherwise would overstate it: what it replaces is an unusable bound with a merely large one, computed from the system rather than guessed.

BC-067 closed the exact route’s loop at \(n = 11\)$n=11$, where the answer is published. discharge stops at the side, which is a claim about a number; the round trip carries it back to a claim about a packing — eleven squares, fourteen touching pairs, valid under exact_sign, and the reconstructed side equal to the field generator exactly. The obstacle is real and \(n = 11\)$n=11$ is where it is avoidable: a pose unknown \(t_i\)$t_i$ is an angle and has no representation in \(Q(s)\)$Q(s)$ at all, but Trump’s construction is already over \(Q(u)\)$Q(u)$ with \(u = \tan(a/2)\)$u=\tan (a/2)$, so the question reduces to recovering \(u\)$u$ from \(s\)$s$. That recovery is a derivation rather than a search — \(Q(s) = Q(u)\)$Q(s)=Q(u)$, both degree eight, so writing each \(s^i\)$s^i$ in the power basis of \(Q(u)\)$Q(u)$ gives a square rational system with one solution, and a singular one is refused rather than fitted. The continuation runs the missing middle layers first, with the efficiency and research cells deliberately last. The full ordering for the sessions after it — including which of the two priority: 0 commitments goes first and why — is the session queue, which is the one place that ordering is written down. The narrative below is historical and its earlier “next bounded slice” pointers are superseded by this paragraph.

The replan followed a correction recorded in X-004. The retained \(n = 29\)$n=29$ SVG does not merely serialize a FindRoot result: it publishes the complete closed system — nine slide scalars in closed form and six equations \(f_1 \ldots f_6\)$f_1\dots f_6$ in \(\lbrace s, a, b, c, d, i\rbrace\)$\{s,a,b,c,d,i\}$ — and the layout map, whose <use> transforms are written symbolically in those same names. cases.kingbird29.verify_svg had already transcribed all of it and used it only to evaluate residuals, never to solve. Solving that same transcription reproduces the record to all fifteen published digits and reaches a maximum equation residual of \(1.11 \times 10^{-1200}\)$1.11\times {10}^{-1200}$ in about six seconds. So BC-042 and BC-043 gate nothing at \(n = 29\)$n=29$; they generalize the route to sizes with no published system.

That moved the prize onto BC-045. Certifying the reported \(n = 29\)$n=29$ value would move verified_upper_bound from the Schadt rational to Kingbird’s, closing \(5.23 \times 10^{-5}\)$5.23\times {10}^{-5}$. Two routes reach it: BC-044 recovers a minimal polynomial and discharges it exactly, which is stronger but of uncertain feasibility — a completed sweep found no integer relation through degree twenty with coefficients below \(10^{22}\)${10}^{22}$ — while BC-045 needs no polynomial at all. The robust route was the one with no specification, so that specification now exists. The witness contract already named interval-certified as a method that may carry verified, and the checker is now built: scalar.kind gains interval-enclosure, exact_verify replays an interval witness instead of raising checker-not-built, and the \(n = 29\)$n=29$ certificate is retained as kingbird-n029-2026-interval under E-n029-interval-certified-upper. Recording is not promotion: verified_upper_bound has not moved to it.

The standing rule is unchanged and applies to every block: an unattended runner may apply the accept rule only conservatively. A round that certifies \(n = 29\)$n=29$ is recorded unresolved with needs_review: true, and a human makes the accept decision.

PR 45 is merged and session 025 is terminal. Session 026 is the terminal first-session midpoint in the two-session balanced ten-hour agenda. Session 027 stopped on an external provider usage limit after ten of eleven phases, and session 028 is the terminal successor that executed its one unexecuted phase. Session 029 closed the remaining agenda-003 commitments on measurement, and session 030 re-glossed BC as bounded commitment, retiring a collision with the linear-programming sense of cell, and made the bead / commitment / phase layering explicit in the orientation docs. Session 031 merged main and found the merged tree failing two gate steps the pre-merge tree passed, because the atlas SVG work pushed the negative-control mutation snapshot past its size cap. That is fixed and pinned, and the gate is green on the merged revision. Session 032 closed agenda-004’s first block: twelve pre-certificate mutations are now enforced on twelve distinct failure identifiers, so exp-045’s admission gap is closed. Session 033 ran exp-045 itself, and session 034 is the terminal successor: it closed BC-035 and BC-041, adding four guards that did not exist, each verified to fire rather than merely to pass and each pinned by its own negative control. Negative controls rise from 76 to 80. The next bounded slice is BC-038 under think-kdil, the row-jet inventory reuse, which exp-045’s terminal disposition unfroze. Both declared determinations report criterion_met — canonical pure -W is excluded at A, the interior, and B, and the -W coefficients equal the separately derived +W values — and record-and-replay agree. The round is recorded unresolved with needs_review, not accepted: an unattended runner may apply the accept rule only conservatively, and the sixth admission condition, an independent post-change audit, is outstanding. The next bounded slice is BC-035 under think-cja6, the pipeline guard consolidation, because exp-045’s acceptance waits on a human and the mixed and transverse successor directions have no instrument. Exactly four distinct reachable failure modes existed, with no slack: a first inventory counted seven candidates by grepping raise sites, and tracing proof_core’s call graph cut that to three reachable identifiers across four conditions. The n=29 certificate was also regenerated at the tool’s default precision, closing a gap between the documented command and the recorded artifact. Q-BC032-a is answered: the \(4.94 \times 10^{-11}\)$4.94\times {10}^{-11}$ relaxation is an artifact of the promotion route, not a property of the pose, and six independently verified promotions beat the recorded baseline. BC-028’s trigger passed, so its inventory-reuse implementation is ready but sequenced behind exp-045. The outstanding work is now carried by agenda-004, which gives each remaining item its own workflow entry. BC-027 is complete. The \(n = 5\)$n=5$ H-023 successor under BC-029, think-whwc, and think-1s0h is no longer an instrument blocker: exp-045 has run and is terminal — accepted since 2026-08-31, after the independent audit its registration required — excluding canonical pure -W at all three strata while every connectivity, component, isolation and terminality claim stays refused. CG-010 is structurally complete under BC-030; BC-016 is blocked under think-3yv8 on retained poses, an executable glued row, symbolic tie labels, and a receipt checker, while BC-017 under think-u97a remains the ready constructive W7 lane.

All \(n = 1\ldots 324\)$n=1\dots 324$ frontier entries now point to normalized witnesses and deterministic house renderings. The first hundred are calibration evidence, not an unseen holdout and not a new proof of optimality; \(n = 101\ldots 324\)$n=101\dots 324$, promoted on 2026-09-07 under the expansion plan and frozen at commit 6e21c4ca, is the unseen corpus a confirmatory run may use once its instrument and grammar are frozen, and the calibration-only layers stay pinned to the first hundred. The atlas source inventory retains attributed Kingbird-derived numerical facts but no raw Kingbird SVG because the review located no express redistribution terms; that conservative repository policy is not a legal conclusion. A broad same-angle contact census covers 1,782 of 1,860 non-grid squares, but the stricter bar/L/rectangle partition establishes 3 of 36 non-grid cases inside its narrow budget. Two cases are conclusively outside that budget, 23 have no partition in the registered candidate universe, and eight are search-capped and therefore indeterminate. Contact components also retain substantial internal sliding freedom, so component count alone is not a defensible chunk cost.

The target-free contact-scaffold layer now retains 11,013 exact size-five signed-contact orbits as an abstract, no-geometry atlas. Its local realization prefilter rejects mixed angle classes before solving and still omits walls, non-edge separation, container fit, whole-packing feasibility, and optimality. CG-010 now adds one separate literal axis-aligned three-square structural cell: all twelve wall decisions, every contact/non-edge pair and oriented axis, the 48 D4-by-relabeling images, a replayable canonical witness, and separate candidate-domain and executed-work prices. It performs zero LP solves and contains no geometry. BC-016 prerequisite instrumentation remains blocked, so the next boundary is BC-017’s target-free tagged structural execution plan and derived accounting. Actual numerical compilation remains blocked on unfrozen open-wall, nonedge, and contact-overlap semantics. This is not an H-044 verdict or an \(n = 11\)$n=11$ run on the inspected calibration corpus.

The H-023 line shows why the distinction matters. Session 004 used W3 to turn an ambiguous terminal-family observation into the falsifiable connectivity hypothesis. Session 009 first used W4 to make basin events and exact identity controls admissible. W6 then produced exp-033’s exact fixed-angle face and exp-034’s angle-and-slide sheet. A W2 instrument review found D-194 and D-195 before the next measurement, preventing a reused contact differential and an invalid alternative-row interpretation from entering the result. W6 resumed only after the corrected criterion was frozen; exp-035 then proved exact first-order directions outside the sheet without proving nonlinear realization. W3 turned that limitation into exp-036’s registered second-order obstruction, and W6 then excluded the displayed direction from the true tangent cone. Exp-038 now certifies the complete branchwise linearization-cone inventory and leaves transverse and mixed nonlinear realization open. Exp-039 then certifies one connected five-dimensional fixed-angle cell-local LP-optimal position polytope and twelve exact paths in release classes R1, R2, R3, and R6. Its positive pathwise first-order stresses do not make the whole polytope stationary or classify a terminal component. When the post-round strict gate failed, W4 separated stale controls from an independent deep-golden solver rejection. That bounded solver repair was recorded under the owning review phase before W7 existed. Future packing-pipeline repairs whose promised output is the implementation itself enter W7; historical phases are not relabelled after the fact. The current terminal transfer line is owned by BC-010 under think-iivb; think-1s0h retains the broader unresolved H-023 question without gating the agenda. Session 015 is terminal after reaching its declared eight-phase cap, and session 016 is the completed final-hour continuation; it preserved the original deadline without extending an expired phase or relying on controller memory. Session 017 is the initial W5 efficiency record, and session 018 is its measured planning refinement. Session 019 corrects the Codex timing instrument, freezes both named task trees, and replaces estimated delay attribution with native per-turn rollups by model and thinking level. Session 020 acts on that baseline: the first hosted required surface finishes in 46 seconds, exhaustive exact work and complete macOS move to direct integration events, and two-worker controls save 58.22 seconds on the full branch. Session 021 updates that lane onto current main, restores cheap exact guards to required PR validation, preserves explicit worker caps, and targets PR 45’s measured census tail. These W5 sessions measure and improve the research and validation loops but do not supersede session 016’s scientific handoff or authorize exp-045 implementation. Session 015’s first bounded W6 slice stopped exp-040 unresolved before retained measurement after independent review found five finite proof-perimeter gaps in the draft R4/R5 checker. Exp-041 froze the exact five-blocker correction at e26fae9, then rejected its complete-zero-inventory criterion on a new endpoint-only axis without refuting path feasibility. Exp-042 corrects that endpoint inventory and meets the full frozen criterion from engine commit 2980fdc: six R4/R5 paths, both owner stresses, and twenty semantic controls pass retained generation and replay. The result is pathwise first-order only. Exp-043 then stops its pure -W test before retained measurement: the draft checker is a resume point, but it does not yet derive production rowwise second-order constants, consume a full exp-034 acceleration witness, or mechanically route the two-scale proof. The following W7 phases provide a case-free exact-jet helper, complete production row builders for all six source matrices, normalized nine-row stress evaluation with every correction column retained, and a formula-derived exp-034 sheet control across both owner inventories. Focused tests and independent review accept that substrate at checkpoint 8ee367b while refusing branch completeness, scale routing, and obstruction. Exp-044 freezes the separate case-level integration but is terminal unresolved with no target run or result JSON. The published checkpoints separate helper substrate 8ee367b, accepted memoryless design 027349b, and full-gate pre-terminal state 3629bf4. Session 016’s terminal handoff owns the branch, read order, validation, exact fifteen-record scale inventory, mutation map, and successor artifact paths, so no controller memory is required. Session 027’s active BC-017 slice under think-u97a builds the admitted target-free tagged structural plan and exact derived accounting. It retains full-cell-execution-semantics-unfrozen instead of compiling or running a numerical full-cell solver before returning to the scheduled W5 inventory. Exp-045 remains a typed instrument blocker with no pure -W target data. The -W, mixed-angle, whole-stationary-component, and unequal-side-clearance questions remain later slices; D-239 is a separate W7 line. Do not start basin-frequency work or reinterpret exp-035 through exp-040 as a connectivity proof.

What Is Built

A documented method here is not necessarily an available one, and implementation status has three values rather than two.

Most of the risk in this project lives in the middle row, because a component that runs and prints a plausible number is the shape of every flattering soundness defect logged here.

The exact layer—built

D-053 is fixed. NumberField now rejects reducible polynomials, intervals with zero or multiple roots, and endpoint roots before any sign decision. It uses an irreducible finite-field reduction when available and a complete factor-exclusion fallback for monic integer quartics; other inputs fail closed when neither supported certificate establishes irreducibility. Exact rational input is the explicit degree-one case. This makes supported generic algebraic input sound at the field boundary; it does not infer the correct field or exact geometry from an arbitrary decimal source.

The refinement layer—built, with a floor

sqpack.research.quench is the LP-in-cell quench with class bracketing, and cases.trump11.independent_lp_cell is an independent second formulation of the same feasible set. Both are built and agree to \(4.4 \times 10^{-16}\)$4.4\times {10}^{-16}$ on Trump’s cell.

Three named limits travel with every number they produce:

• D-021—the float LP solver has a noise floor of about \(10^{-11}\)${10}^{-11}$ in the side. No numerical comparison may claim a difference finer than that floor. The general fix is an exact LP over certified rational or algebraic coefficients, which is unbuilt; it is purely rational only for rational-coefficient cells.
• D-052—coordinatewise stopping is not a certified local optimum. A quench that stops has stopped; it has not proved stationarity.
• D-126—the work budget is wall-clock time, so contention changes how many LP solves a run performs. Price basin experiments by retained work units, not by the clock.

The proposer layer—one instrument, and the interface is unbuilt

sqsearch/ is the f64 screening annealer, and it is the only proposer the campaign has run. Uniform multistart draws exist inside the census and the checkers, with the census declaring its regime; the proposer interface—the contract that would make two proposers comparable—is unbuilt.

The stock annealer now counts and emits every search-side pair evaluation, including restart initialization, both local scans per move, and final retained-pose screening. Its CLI still enforces move budgets, and the first downstream quench adapter discards the all-chain summary, so this is a meter seam rather than an equal-work proposer interface.

Unbuilt, and each is a registered hypothesis with nothing behind it yet: the proposer interface and pair-budget enforcement (so no two proposers have ever been compared at equal budget), δ-continuation, angle-class search as a search, neighbour-transfer seeding, MAP-Elites retention, and billiard/inflation.

This is the record-finding lane’s live bottleneck. The refiner takes the tested proved-control starts to residuals of \(10^{-15}\)${10}^{-15}$ and leaves the tested \(n = 11\)$n=11$ starts at \(6 \times 10^{-2}\)$6\times {10}^{-2}$, so proposal is where the gap is—and proposal is the layer with the fewest built parts.

The map layer—built, not admissible

distinct_basins is a count of endpoint keys, not of connected terminal components. The exact \(n = 3\)$n=3$ sliding family shows one connected optimal set producing many keys, so the store can split a single component. Until D-034 is resolved the discovery curve cannot plateau, the census cannot saturate, and the rarity premise is untestable rather than untested.

Cheap endpoint summaries such as angle signatures and contact counts exist. Exp-032 now supplies an exact known-answer boundary: complete \(n = 3\)$n=3$ and \(n = 4\)$n=4$ quotient models may assign components, while unsupported numerical observations remain unresolved. A scalable retained-pose classifier is still unbuilt, so steering strategies that depend on sampled component identity or descriptor distances remain unbuilt too.

The promotion pipeline—built end to end, with the promotion itself withheld

The public packing-witness promote command implements robust rational promotion for suitable decimal center-angle poses. It rationalizes centers and rotations, tries an explicitly bounded dilation, writes every corner as a rational, and verifies the result exactly before emitting it. Failure is typed and leaves the source witness unchanged.

The retained Schadt \(n = 29\)$n=29$ pose is the regression case. The source decimal geometry passes its declared 300-digit calculation at tolerance \(10^{-100}\)${10}^{-100}$, with thirteen slightly negative best pair gaps hidden by that tolerance. Robust promotion produces a different, slightly relaxed rational packing at 2966942899906512939318226046481160904289990651293931822604648091421/500000000000000000000000000000000000000000000000000000000000000000, an increase of about \(4.93 \times 10^{-31}\)$4.93\times {10}^{-31}$ in the container side. The generic exact verifier and a small independent rational checker both accept all 29 squares and 406 pairs. This formally proves the weaker upper bound; it does not verify the original decimal pose, the tighter current Kingbird report, or global optimality.

The reported-value path now has every component built, and still promotes nothing. Those are two separate facts and the distance between them is the point.

Each step named as missing when this section was first written now exists and is replayable. promote.contacts infers which features meet and issues a typed refusal for any incidence it cannot decide rather than choosing one. promote.system assembles those into equations that vanish at the packing they came from, one per contact type rather than one per contact. promote.solve recovers a minimal polynomial under a margin rule frozen as a test, because an integer-relation search given enough digits returns a relation whether or not one exists. promote.krawczyk decides existence and uniqueness over a box with directed rounding, returning exists and unique separately, and nothing may be promoted from exists alone. promote.roundtrip rebuilds the packing from the recovered field and compares the reconstructed side against the input, which is what catches a contact structure that is valid but suboptimal.

The contingencies that made this look unbuildable are reported rather than assumed away. At \(n = 29\)$n=29$ the Jacobian turned out well-conditioned enough to contract in two iterations, which was an open question rather than a given, and the contact Jacobian reaches full rank at both determined sizes — \(34\)$34$ of \(34\)$34$ at \(n = 11\)$n=11$ and \(88\)$88$ of \(88\)$88$ at \(n = 29\)$n=29$. The shortfall that had suggested otherwise was D-361, a bug in assembly rather than a property of the packings.

One integration boundary remains. The public packing-witness promote --strategy interval-existence still raises the typed checker-not-built gap, because the certification that has been done ran through cases.kingbird29.certify_interval, a case-specific driver over generic library code. A general path from an arbitrary Witness/v2 to a certificate is not exposed, and the typed refusal is the honest answer until it is.

The interval route certifies \(s(29) \le 5.93383346267692918974379895098\)$s(29)\le 5.93383346267692918974379895098$ at a declared relaxation of \(10^{-20}\)${10}^{-20}$. Review adopted that certificate as the case’s verified_upper_bound and as T-009. It remains \(9.18974379895098 \times 10^{-15}\)$9.18974379895098\times {10}^{-15}$ above the tighter reported value, which is still uncertified at its declared precision.

Exp-033 remains a distinct dedicated result: it bound two retained \(n = 5\)$n=5$ float poses to exact endpoints on one certified fixed-angle optimal face and supplied an exact dual for that cell. The early quench archives still lack complete centers, and current BasinEvent/v3 controls are known-answer material rather than open-case record candidates. Most public frontier entries still record side values without an imported geometry witness.

Verification Capability Ladder

The verification tooling overview maps feasible witnesses, point and threshold certificates, adaptive parent cores, rectangle densities, and mixed covers to their actual checkers and remaining gaps. Native point and threshold gates have complete distinct coverage methods. The native rectangle prototype passes a complete analytic control; existing retained rectangle-bound replays still use Tokoharu’s checker, with independent exact premises and input binding. Complete native coverage of a retained external rectangle certificate remains open under W7 / think-bmf3. The overview also separates the newer zero-margin mixed covers and modified n50 bundle from those formats, and distinguishes full replay, partial samples, receipt audits and formal-kernel evidence.

The proof lane—built and producing theorems

This is the lane that moved furthest in the recent rounds: it carries formal results, not only instruments.

Unbuilt on this lane: the PoseBox scalar and the interval branch-and-bound hook, LP duals as unavoidable-set generators, and any Lean formalization.

Compiled acceleration—unbuilt, deliberately

sqpack-core, the filtered kernel, the FLINT-backed algebraic scalar, and the language bindings are all unbuilt. That is a scheduling decision made by measurement rather than an omission: the current pipeline is quench-dominated, and moving only the geometry kernel to another language would not remove the measured LP-solver and wrapper cost. Direct solver bindings or a compiled batch path may still matter; the phase begins by re-measuring and builds only what the profile names.

Reading the gate

packing-validate runs the steps registered by its validation table; packing-validate --list prints the authoritative current inventory. A green gate means every built component behaves as its checks describe; it says nothing about the unbuilt ones, and it does not upgrade an inadmissible output.

The gate is not environment-independent. Endpoint identity depends on floating-point behaviour in a degenerate linear program, so the same seed can reach a different endpoint under a different toolchain, and a check written around one observed endpoint can fail elsewhere. Separating portable mathematical predicates from stochastic characterization is open work (D-059).

Terminology

These words are used in a narrow sense throughout this directory, the campaign artifacts, and the beads. Three carry controlled multiple senses—exploration, cell, and quench—and for each, the rule for which form to write is stated with the definition. Nothing below is a synonym for anything else below.

Assurance, Methods, and Claims

Verified means formal throughout this project. An exact check, rigorous certificate, or complete proof must decide the scoped claim and discharge its preconditions. Every finite-precision calculation is numerically checked, regardless of its digit count or tolerance. A source statement not established through either path is reported.

Assurance does not encode the method:

“Arbitrary precision” may describe a library; a result states the precision actually used. numerical-multiprecision at 30, 100, or 300 digits remains numerical, and a tolerance of \(10^{-100}\)${10}^{-100}$ remains a tolerance. Conversely, a rigorous interval certificate can be formal without listing one symbolic coordinate, because outward rounding proves the claim for every point in its enclosure.

Reader views also name origin and independence. A complete published proof may be formally valid without a local audit. Whether anyone here has read it is a separate fact and is recorded separately, in external_review: not-reviewed when the claim is transcribed and nobody here has worked through the argument, informally-verified when someone here read it and found no error, defect-found when someone here read it and it was wrong.

That field changes no assurance and promotes no method — a published proof proves its claim whether or not we read it, and reading one is a careful human act, not the machine check proof-assistant-checked names. What it changes is whether a reader can tell the two apart. Four of the six external proofs the register carries are not-reviewed. The two that have been read are [Nagamochi 2005], the register’s most load-bearing external argument, read on 2026-08-30 and recorded informally-verified, and [Bentz 2010], recorded defect-found after the machine audit found Lemma 10’s replacement point transposed in print. The distinction is not hypothetical: [Stromquist 2003]'s \(n = 11\)$n=11$ argument needed a source-distinct repair, which E-n011-repaired-lower supplies without repairing the printed proof. An external certificate and a repository replay remain separate evidence records. Running the generator’s own checker is not an independent implementation. A page that says “interval verified” but publishes no certificate or replayable checker stays reported with a public-certificate-missing blocker.

The evidence inventory is the generated roll-up of all four facts across the register, including which evidence the hundred cases actually lean on. That last column is the one worth reading, and it needs its qualifier: the most-cited record overall is the Kingbird register at 98, which is the catalogue everyone reports from and is labelled reported. The dependency that matters is the most-cited argument this repository did not produce — E-nagamochi-lower, cited by 88 of the hundred cases and carrying the verified lower bound in 83 of them, the difference being the cases this project’s own certificates have since taken off it: \(n = 11\)$n=11$, \(n = 12\)$n=12$, and \(n = 17\)$n=17$ through \(n = 21\)$n=21$. Being cited that heavily is a reason to open an argument, not a reason to trust it, so it was read here on 2026-08-30; its record carries what was re-derived and the four things that were not.

Novelty—whose result this is—is a further separate fact. Its values differ in what they oblige, which is why each is recorded explicitly rather than inferred from an absence:

An entry without the field makes no novelty statement: not yet assessed, or the record declines one, as exp-014 does for the quotient refinements. Absence never means “not novel”. check_evidence_semantics enforces the two obligations a machine can check.

Every formal conclusion names its object:

Thus a verified feasible placement is a formal upper bound, not a verified record optimum. The frontier may call the optimum proved only when its verified lower and upper lanes meet. “Exact” should qualify the object—exact coordinates, predicate, bound, or proof step. An exact formulation passed to a floating solver still produces a numerical result.

Work Units and Records

Packing exploration. The complete self-contained project at packing/: research documents, sources, code, tests, plans, and campaign record. Write the full phrase when this directory is meant. Bare exploration retains the mathematical meaning under The Operations.

Campaign. The durable, multi-session square-packing research program under one registry, evidence contract, and generated record. This campaign lives in campaign/ and contains bounded search, proof, validation, and infrastructure questions. Basin cartography is its current search objective, not the definition of the whole program. A campaign can span many series and agent sessions; neither is a synonym for it.

Series. One campaign-wide tooling generation and comparability boundary. Open a new series when an instrument or regime change makes earlier conclusions unsafe to compare or carry forward. Each experiment still records its narrower subject, instrument, and provenance, so sharing a series does not make unlike result shapes comparable. The open series-000 predates strict application of this rule; its series note states the safe reading, and think-i08r owns the persisted-record migration.

Agent session. One bounded interval of orchestrated work. It may produce zero, one, or many experiments. Most routine sessions need no separate record; session-NNN is the versioned recovery and handoff artifact used when the escalation criteria apply, not a scientific measurement.

Workflow phase. One contiguous interval inside a versioned agent session with one workflow, one primary focus, one objective, and one clock. A focus-only change starts another phase with the same workflow; a changed purpose starts a phase under a different workflow.

Focus. The primary quality dimension emphasized during a phase: correctness, process, insight, or efficiency. The other principles still constrain and may contribute to the work. Focus answers what quality is being privileged, while workflow answers what kind of result the phase promises.

Slice. The smallest time-bounded action inside a phase. It ends at a concrete evidence checkpoint and may be renewed only by stating the next bounded question. A slice is not automatically an experiment; source inspection, a checker repair, or one proof derivation can each be a slice. A delegated mechanical slice inherits the coordinating phase unless it opens its own independently tracked session.

Hypothesis. One registered claim stated so it could be wrong, with a criterion, regime, and instrument. It persists across sessions and series and may be tested by several experiments. An open question that cannot yet carry a falsifiable criterion is recorded honestly as such.

Experiment. One durable exp-NNN artifact recording one preregistered research round in exactly one series. It contains the method, typed results, effort, verdict, and links to raw evidence. An experiment can aggregate several lower-level runs and is not an agent session.

Round. The bounded research work recorded by one experiment. Use round for the act or its place in a sequence and experiment for the durable exp-NNN record. They are one-to-one in this campaign; neither means one solver invocation.

Run. One invocation or trial of a tool, solver, or proof checker. Several seeds or conditions can produce several runs inside one experiment. runner.py run is a command name that sequences experiments; it does not change this definition.

Result. One typed observation inside an experiment—a record score, categorical determination, paired comparison, or condition comparison. The verdict applies the preregistered rule to the results; it is not another result shape.

Ledger. A generated view over session, agenda, series, hypothesis, experiment, and effort artifacts. It summarizes authoritative sources and is never edited by hand.

Exploration report. One free-form X-NNN idea record from which hypotheses may be mined. Write the full phrase for the artifact. It is distinct from both the packing exploration directory and the basin-exploration operation below.

The objects

Configuration. A placement of all \(n\)$n$ squares: a centre \((x_i, y_i)\)$(x_i,y_i)$ and an angle \(\theta_i \in [0, \pi/2)\)${\theta }_i\in [0,\pi /2)$ for each, together with a container side \(s\)$s$. That is \(3n + 1\)$3n+1$ real coordinates, 34 at \(n = 11\)$n=11$. A configuration is valid when the interiors are pairwise disjoint and all squares lie in \([0, s]^2\)$[0,s{]}^2$; touching is valid.

Cell—always a cell of configuration space: a choice, for each of the \(C(n,2)\)$C(n,2)$ pairs, of one candidate separating axis together with an order (which square is on the low side). A configuration lies in a cell when those choices genuinely separate those pairs in that order. Fixing the angles and a cell turns the problem into a linear program; that is T-2.

Instance cell—an \(n\)$n$ carrying a declared role in the sweep: \(n = 10\)$n=10$ positive control, \(n = 11\)$n=11$ target, \(n = 12\)$n=12$ open-case calibration, \(n = 17\)$n=17$ mechanism-matched calibration. A control cell is an instance cell whose answer is known before the run, and a breach of one rejects the round regardless of outcome.

Three senses collide, and all three appear in this document. Write “cell” for the configuration-space object, “instance cell” for a sweep position, and “event cell” for a region of admissible centres—never bare “cell” for either of the last two. In running prose about a round, prefer naming the \(n\)$n$. The three are unrelated objects: one is where the LP is solved, one is what a round is run on, and one is where a certificate’s covered mass is constant.

Basin (point-basin where the distinction matters). The preimage of one pose returned by a deterministic quench: the set of configurations the refiner carries to that numerical endpoint. A point-basin is therefore defined relative to a specific quench, which is why basin identity may not inherit the search’s tuning parameters—a quench that merged nearby angles would make the word depend on the merge tolerance (D-020). The current quench gives each terminal pose a reproducible numerical candidate, but that does not make the terminal set discrete or decide whether two candidates belong to one connected component. D-021 bounds error in the scalar side only; it is not a pose- or component-resolution theorem (D-039).

The point-basin exists, but it can be the wrong counted object. A deterministic quench returns a pose even when that pose lies on a connected terminal family. Different neutral coordinates then produce different point-preimages and keys inside one terminal component. D-034 records why a component census must quotient that family using independently validated connectivity rather than declare the quench map undefined.

The ladder. The proved instances used as controls—n = 5 and \(n = 10\)$n=10$, both \(45^{\circ}\)${45}^{\circ }$ mechanisms with closed-form optima. The ladder validates machinery: no proved case exercises an irrational oblique angle, so passing it says nothing about strategy at \(n = 11\)$n=11$.

The weighted-certificate objects

The lower-bound lane has its own vocabulary, and it is narrow in the same way the rest of this section is. Each term is defined where the conditions themselves are stated, and TUTORIAL.md develops all five from first principles.

Condition 1 to Condition 5 name the five conditions a certificate must satisfy and are stated in the module above; they are not the confirmation rungs C0 to C5, which epistemics.md owns.

The operations

Quench. Two senses, both in use, and they do not conflict. As a map, in Stillinger and Weber’s sense: the function sending a configuration to the local optimum a deterministic refinement carries it to. As a component, sqpack.research.quench: this project’s implementation of that map—solve the LP in the current cell, move the angles, re-solve, until fixed. Say “the quench map” where the distinction matters.

Polish. Refinement within the basin a configuration is already in—driving the side down to the local optimum without changing which local optimum that is. This is what the quench does, and all it does.

Exploration—without a qualifier, the operation of reaching a different basin. No amount of polish performs it, and nothing currently in the toolkit does it reliably at \(n = 11\)$n=11$. Write packing exploration for the project directory and exploration report for an X-NNN artifact.

Proposer and refiner. The two halves of the loop, named separately because the measurement that matters is which one is failing. The proposer emits candidate configurations (today: the sqsearch annealer); the refiner is the quench. Building a better refiner cannot fix a proposer failure.

Angle class. A set of squares constrained to share one angle. Trump’s packing has two classes at \(n = 11\)$n=11$: six squares at \(0^{\circ}\)$0^{\circ }$, five at \(a^{\ast}\)$a^{*}$. Class bracketing is the angle search that optimises over merged classes by bracketing rather than by gradient, which is what a corner requires; class_tol is the tolerance that decides which angles merge into one class.

Corner (equivalently kink). A point where the LP optimum as a function of the angles has distinct one-sided derivatives, so no method assuming a smooth local model converges to it. Measured at \(n = 11\)$n=11$: \(0.1747\)$0.1747$ and \(0.384\)$0.384$ per radian, through two independent implementations (T-3). Not a synonym for “sharp minimum”—the derivative does not become large, it fails to exist.

Rigidity. A packing that has no non-trivial feasible infinitesimal or local motion under the declared quotient and container condition. Contact counts and visual pinning are candidates for this property, not proofs; they require an active-constraint rank or stronger local certificate. Exp-013 supplies that stronger certificate for Trump’s packing: every complete branchwise fixed-side linearized cone is zero, and a finite-branch argument proves local isolation. It does not quantify the neighborhood or prove global optimality.

Terminal family (called a flat basin in older campaign prose). A local-optimal terminal set that is not an isolated point. Its local dimension is the nullity of the appropriate independent active-constraint Jacobian after quotienting symmetries and accounting for inequalities and stratum changes. Raw contact counts cannot supply that rank: contacts may be dependent, one contact description may encode several scalar conditions, and angles and separating cells may change along a motion.

At \(n = 3\)$n=3$, the exact family with centres \((1/2,1/2)\)$(1/2,1/2)$, \((3/2,1/2)\)$(3/2,1/2)$, and \((t,3/2)\)$(t,3/2)$ for \(t \in [1/2,3/2]\)$t\in [1/2,3/2]$ proves that terminal continua occur and that the current endpoint key splits one connected optimum component. At \(n = 5\)$n=5$, exp-033 proves that the two equal-side rows with different geometric keys share one exact connected fixed-angle LP optimal face. Its fixed-side active nullity is one in the interior and zero at the two boundary strata. Exp-034 proves that face lies in a two-parameter angle-and-slide sheet of orientation-indexed LP optima. Exp-035 derives the full active first-order systems at both endpoints and one interior point; every owner branch admits one exact direction outside that sheet. Exp-036 proves that displayed direction is not a true Bouligand tangent: both possible nearby owner axes have strict exact second-order obstructions. Exp-038 certifies the complete branchwise linearization inventory: endpoint quotients have eight rays, interior quotients have six, and both owner branches coincide. Transverse and mixed nonlinear realization remains unclassified. This is not a local-isolation theorem, a proof of a five-dimensional family, or a classification of the complete nonsmooth stationary component (D-034, D-041).

This distinction should have existed from the first day. “Rigidity” was treated as an informal visual property of the target while the census silently assumed every terminal was isolated. The exact \(n = 3\)$n=3$ control falsifies that assumption directly. That is a documentation failure before it is a code one, and it is why D-034 was found by reading a census output rather than by reading the plan.

The measurements

Gap. Always best_side − standing_best, in units of the container side, and always signed. A negative gap from a numerical method is solver noise, never a discovery.

Standing best. The best side ever published for that \(n\)$n$, read from frontier/—an upper bound, and for the open cases not known to be optimal. Distinct from the analytic optimum, which exists only where the case is proved. At \(n = 5\)$n=5$ and \(n = 10\)$n=10$ they coincide; at \(n = 11\)$n=11$ the standing best is Trump’s construction and the optimum is unknown.

Polish failure and exploration failure. The decomposition of a gap, and the campaign’s central diagnostic. A polish failure is a gap that the declared refiner closes, as \(n = 10\)$n=10$ was, from \(4.19 \times 10^{-4}\)$4.19\times {10}^{-4}$ to \(1.33 \times 10^{-15}\)$1.33\times {10}^{-15}$. An exploration-or-model failure is a gap that remains after that local procedure, as the tested \(n = 11\)$n=11$ starts did, from \(8.85 \times 10^{-2}\)$8.85\times {10}^{-2}$ to \(6.29 \times 10^{-2}\)$6.29\times {10}^{-2}$. Neither numerical behavior proves a terminal-component relation. “Right basin” and “wrong basin” require the component evidence tracked by H-021 through H-023.

reached_basin. A recorded outcome meaning best_side − standing_best < 1e-4. It is a numerical proxy for “found the right combinatorial class”, not evidence of it—establishing the class means comparing contact graphs. A round claiming reached_basin must say which it means.

Pair-test. The budget currency: one evaluation of one pair of squares for overlap. Machine-independent, unlike wall clock or moves, which is why proposer comparisons are denominated in it. Tiers S/M/L are \(10^9\)${10}^9$/1e11/1e13.

Assurance. What the evidence may conclude: reported, numerically checked, or verified. Assurance is separate from method, actual precision, tolerance, and origin. The full contract is under Assurance, Methods, and Claims. beat_record: true requires verified assurance. A floating LP endpoint is numerically checked and remains subject to the \(10^{-11}\)${10}^{-11}$ side floor in D-021.

Not used here

Two coinages appear in side work and are deliberately not adopted, because the project already has clearer words for both.

• “polish gap” / “exploration gap.” Write polish failure and exploration-or- model failure for the scoped procedure outcome. Reserve right basin / wrong basin for a state supported by a declared terminal-component relation. A gap is a number; whether it is polish or exploration is a conclusion about that number, and the two-word compound hides the inference. Neither compound occurs anywhere in this directory and neither should start.
• “the quench” for a fixed-angle solve. A quench includes its angle half. See A cell is not a basin—the conflation cost a correct finding (D-029).

The deliverables, and what each one currently is

These four words name the cartography strategy’s intended outputs. Two now have code behind them and two do not, and neither pair has yet produced the object the word promises. What Is Built is the component-level view.

Atlas. The deduplicated store of known basins for an \(n\)$n$, keyed by canonical basin identity. The stated deliverable of the cartography strategy. Code exists; it stores endpoint keys, which are not certified terminal components. The atlas is also the flagship cross-focus instrument: Insight specifies views that could expose mathematical structure—symmetry orbits, terminal components, contact types, transitions, continuation across \(n\)$n$, proposer-conditioned frequency with uncertainty; Efficiency makes those views responsive and reproducible; Process owns the event and provenance contract; and Correctness decides which relations are observed, inferred, or certified. A visual embedding is never evidence by itself that two basins are adjacent or that a sampled cluster is a connected component.

Census. An enumeration of the basins at one \(n\)$n$, run to saturation. Code exists; saturation is unreachable while the thing being counted is undefined.

Descriptors. Structural coordinates of a packing—contact counts, angle classes, symmetry—used to steer search toward diversity rather than toward loss. Unbuilt, and every steering strategy waits on them.

Meter. The instrument that counts pair-tests, so two proposers can be compared at equal budget. The stock annealer’s search paths are metered; pair-budget enforcement and campaign-wide stage receipts are unbuilt, so no two proposers have been compared at equal budget.

Identifiers and Control Records

Round and series are defined once under Work Units and Records. Under the current experiment contract, every round tests exactly one registered hypothesis. The field remains an array for format compatibility; one verdict is never applied to several claims.

Agenda. A mutable priority queue of cells (BC-001, …) ordering upcoming work by dependency and readiness, rendered into the ledger. It is a coordination artifact, not a second hypothesis registry and not a scheduler.

Block commitment (BC). One bounded question or deliverable in an agenda, with entry and exit conditions, an effort estimate, dependencies, and an accountable bead. Its hypotheses field links the scientific questions it serves. A planning or tool commitment can produce no experiment; a research commitment may produce several, each with its own registered claim. Completing a BC settles its declared scope, not the whole H-item or agenda.

Program and parallel group. Labels on BC items. A program groups a continuing research direction; a parallel group identifies work that can have a separate owner. A strategic lane is such an assignment, not a new record type. Actual capacity, dependencies, and shared writes determine which groups run together.

Planning block. A W10 commitment that assesses the current questions and selects future work. A linked tbd plan retains rationale and alternatives; the H-items and agenda receive its operational decisions before it closes. Sessions then record how that work actually ran.

Defect. One record in defects.yaml—what went wrong, what caught it, and what now stops it recurring—rendered to defects.md.

Bead. One tracked work item (think-xxxx) in the tbd queue; every open defect carries one.

Soundness perimeter. The rule that every component emitting a configuration is checked by sqpack through code it does not share, enforced by devtools.check_soundness_perimeter. A component joins it in the same change that introduces it—not doing so is how D-014 was possible.

The Problem

A packing of \(n\)$n$ unit squares in a container square of side \(s\)$s$ is a placement of the \(n\)$n$ squares, each free to translate and rotate, whose interiors are pairwise disjoint and which all lie inside the container. \(s(n)\)$s(n)$ is the infimum of the \(s\)$s$ for which one exists. Touching is allowed, and in good packings it is pervasive.

For most \(n\)$n$ the answer is uninteresting: \(s(m^2) = m\)$s(m^2)=m$ by the grid. It becomes interesting just above a perfect square, where the leftovers must be tilted in.

At \(n = 11\)$n=11$ Walter Trump’s 1979 construction still supplies the exact upper bound. T-060’s independently audited global proof supplies the matching lower bound. The earlier lower-bound program passed Stromquist’s bound on 2026-09-04:

The exact optimum: a certified degree-8 construction with a matching global lower bound. The segment and dot contact marks are exact, not tolerance-based visual guesses.

The value T-018 displaces is Stromquist’s \(2 + 4/\sqrt{5} = 3.788854382\ldots\)$2+4/\sqrt{5}=3.788854382\dots$, stated in Memo III, p. 10 on November 15, 1984, and published in 2003. The memo states the unrestricted bound without supplying its proof. The memo review records the source distinctions and the helper-argument followup. The current audit found an explicit strict box avoiding all twelve printed Figure 14 points, so the paper’s unavoidability subclaim is false as printed (D-152). Exp-017 independently certifies the same numerical inequality by moving only \(G=(.8,1.85)\)$G=(\mathrm{.8},1.85)$ to the source-distinct \(G'=(.79,1.85)\)$G^{\prime }=(\mathrm{.79},1.85)$ and replaying the complete finite cover and capacity argument (T-010). The repaired coordinate and certificate are results of this repository, not claims attributed to Stromquist.

Trump’s packing is six axis-aligned squares plus a block of five tilted at \(a^{\ast} \approx 40.181937290329714^{\circ}\)$a^{*}\approx {40.181937290329714}^{\circ }$. The container side is an algebraic number of degree 8, the root of

s⁸ − 20s⁷ + 178s⁶ − 842s⁵ + 1923s⁴ − 496s³ − 6754s² + 12420s − 6865 = 0

lying in \([3.87, 3.88]\)$[3.87,3.88]$. Exp-013 exactly certifies every complete branchwise fixed-side linearized cone and proves the pose locally isolated by a finite-branch subsequence argument. This qualitative local theorem does not provide an explicit radius or explain the global search difficulty.

Why exactness is not optional

Disjoint interiors means touching is legal, and record packings touch a great deal. In Trump’s packing 14 of the 55 pairs are separated by exactly zero, and 20 corner coordinates lie exactly on the container boundary.

Floating-point evaluation can certify a strict inequality when a sound error bound stays away from zero. It cannot infer that an unrecognised near-contact is exactly equal to zero merely because a computed residual is small. A tolerance-based f64 verifier therefore needs a tolerance to accept Trump’s rounded algebraic contacts, and that tolerance is a blind spot that also accepts overlaps smaller than itself; setting it to zero rejects this true packing instead. Both failure modes are demonstrated by cases.trump11.verifier_limits.

The fix is representational rather than numerical: express the configuration in the real algebraic number field it actually lives in, where equality is decidable. That is what the exact sqpack path does. A rigorous outward-rounded interval certificate can also be formal; a finite point evaluation cannot. This is why the campaign permits beat_record: true only under verified assurance.

This is not an abstract concern. The same failure reappeared inside the refiner eight rounds later: an LP solver at its default tolerance returned a packing violating its own separation constraint, and so a side below Trump’s (D-014, critical, caught by the pre-registered rule that beating the record means you have a bug).

The Lay of the Land, by n

Where the program has spent effort, and what came of it.

Three facts about this table drive the strategy.

Every proved control in the ladder is a 45° mechanism. \(n = 5\)$n=5$ and \(n = 10\)$n=10$ are symmetric arrangements that blind search reaches without help. \(n = 11\)$n=11$ needs an oblique core at an irrational angle, which neither control exercises, so the ladder validates machinery, not strategy. T-060’s later proof of \(s(11)\)$s(11)$ is a lower-bound argument, not a search, and does not change this.

The ladder now discriminates sharply, and the target does not move. The bracketing quench takes \(n = 5\)$n=5$ and \(n = 10\)$n=10$ to machine precision and leaves \(n = 11\)$n=11$ essentially where the annealer put it. That is the cleanest statement of where the difficulty lives: the refiner is not the problem.

\(n = 17\)$n=17$ adds one mechanism-matched negative result. It was the only registered instance cell testing record-finding rather than machinery, and it was the last one never run. exp-011 ran it: the annealer reports \(5.0\)$5.0$ on all five binary64 screening seeds—the trivial \(5\times5\)$5\times 5$ grid—against Bidwell’s \(4.67553\)$4.67553$, a gap of \(+0.324\)$+0.324$. The retained final states do not leave the grid basin.

That scopes one failure at a second cell: this implementation, five seeds, and the registered \(10^8\)${10}^8$ moves per chain did not reach Bidwell’s oblique record at \(n = 17\)$n=17$. The retained final best does not show which orientations the trajectory visited, and a single budget cannot establish that no larger budget or related proposer can reach oblique records as a class (H-020).

n = 11, End to End

This section preserves the former open-case account as of Session 156 on 2026-09-23. For the settled result, see T-060 and the proof review. The linked artifacts are authoritative where the historical text and current case record differ. Claims keep the distinctions epistemics.md draws: proved, machine-verified at a stated V/C rung, numerically observed, or conjectured.

As of 2026-09-23, the verified bracket was \(3.875 < s(11) \le 3.87708359002281417\ldots\)$3.875<s(11)\le 3.87708359002281417\dots$, a gap of \(0.002083590022814177\ldots\)$0.002083590022814177\dots$ (n-011). The lower end is Kleddamag’s external certificate, replayed here by two complete methods; the upper end is Trump’s 1979 packing, verified exactly. Every first-party counting family is capped below \(3.875\)$3.875$, no counting certificate can reach the upper end, and the first measured step toward settling the value by verified global optimization built a search tree about a thousand times larger than estimated.

What a proof has to do

An upper bound is a witness. One packing in a container of side \(L\)$L$ proves \(s(11) \le L\)$s(11)\le L$. Trump’s packing, six axis-aligned squares and five sharing a tilt of about \(40.18^{\circ}\)${40.18}^{\circ }$, fits at \(U = 3.87708359002281417730789706010096\ldots\)$U=3.87708359002281417730789706010096\dots$, the root of the degree-8 polynomial under The Problem. T-011 verifies it exactly over \(\mathbb{Q}(u)\)$\mathbb{Q}(u)$ at V4/C3, and Why exactness is not optional explains why its 14 zero-gap contacts put it beyond any floating-point checker.

A lower bound excludes every packing at some side, and at \(n = 11\)$n=11$ only counting arguments have done that. A weighted certificate places atoms of total weight below eleven in the container and shows that every admissible shrunken copy of a unit square captures weight at least one; disjoint squares capture disjoint weight, so eleven cannot fit. The weighted-certificate objects fixes the terms, and the tutorial proves the point-atom version from first principles. Two refinements carry the rest of the story:

• Threshold atoms, from T-025 onward, charge a core that captures at least \(k\)$k$ of a finite point set \(S\)$S$. Disjoint cores divide \(S\)$S$ between them, so at most \(\lfloor \lvert S\rvert/k \rfloor\)$\lfloor \left|S\right|/k\rfloor$ cores are charged and the atom costs that multiple of its weight: a 2-of-3 atom buys two points’ coverage for one point’s budget. The charge is not additive in the points a core captures.
• Parent-core charges, Kleddamag’s form, replace one shrink and one direction net by a catalogue of rows. Each row fixes a half-angle interval for the parent square, a core direction and a core side chosen so that the core fits strictly inside every parent in the interval, and the charge is required only at centres a legal parent can occupy (Kleddamag review).

Point certificates have a proved ceiling. An exact depth-one family of eighty-eight closed shrunken squares at six net directions, of total weight exactly eleven, shows that no D4-symmetric point-atom measure of mass below eleven exists at \(191/50\)$191/50$ for the retained shrink; scaled to unit squares, the same family caps the one-body point method at \(38200/9977 \approx 3.8288\)$38200/9977\approx 3.8288$ (n-011). Threshold charges are not bound by it: T-025 proves \(191/50\)$191/50$ where point atoms are foreclosed, and Kleddamag’s certificate reaches \(3.875\)$3.875$.

Trump’s pose is machine-verified to be locally optimal, and that says nothing far from it. Exp-013 certifies all 128 derivative-distinct fixed-side linearized cones to be zero, so the pose is locally isolated and strictly locally side-optimal. The BC-240 isolation theorem quantifies this in one labelled, anchored 33-coordinate sup-norm chart: within ρ_row = 808514697/200000000000 ≈ 0.0040426 of Trump’s pose, the only labelled packing at side at most \(U\)$U$ is Trump’s own. The source-distinct BC-241 review accepted the packet, and a full radius-generator replay on 2026-09-24 reproduced it value-for-value, with the method-distinct capture_radius control agreeing on every face; its first clause is verified and exact (BC-241 closure). It does not bear on a different contact class.

Settling \(s(11) = U\)$s(11)=U$ is a different kind of statement. Trump’s packing is feasible at \(U\)$U$, so a counting certificate can only exclude sides strictly below \(U\)$U$. Equality needs every part of the feasible set \(\lbrace S \le U\rbrace\)$\{S\le U\}$, over eleven centres and eleven angles, closed by infeasibility, a side inequality, a feasible descent, or capture in Trump’s ball. That is verified global optimization (PR 230 review, findings 1 and 2). The Cell Decomposition is why the centres are the easy half: at fixed angles and separating axes the problem is a linear program, so the eleven angles are the bottleneck.

The first-party ladder, and where it stopped

Stromquist’s published \(2 + 4/\sqrt{5} = 3.788854\ldots\)$2+4/\sqrt{5}=3.788854\dots$, independently restored here as T-010, was the bound until 2026-09-04. Every rung of the first-party ladder beyond it is machine-verified (results register, n-011):

Together they moved the bound about \(+0.038143\)$+0.038143$ past Stromquist. By mid-September three ceilings bounded the retained languages, and the verified bound now sits above all three:

1. The frozen family’s refinement ceiling, \(955000/249507 \approx 3.82755\)$955000/249507\approx 3.82755$. T-033 moved T-026 by \(0.000550\)$0.000550$, half of what the previous net doubling bought.
2. The point-only ceiling, \(38200/9977 \approx 3.8288\)$38200/9977\approx 3.8288$, about \(0.00236\)$0.00236$ above T-026.
3. The retained 181-direction fixed-core point model’s packing-side cap, about \(3.869\)$3.869$ (certificate reach).

A structural program at \(96/25 = 3.84\)$96/25=3.84$ split packings by corner class. It produced two conditional exclusions — T-023, one four-owner class, at V3/C3, and T-031, the all-free octagon class, at V4/C3 — and showed the all-deep class to lie outside the point language, so the corner tree cannot close at that side by clipping alone. No packing was excluded at \(3.84\)$3.84$ unconditionally.

The owner’s 2026-09-14 strategy reset turned this into policy. Agenda 036 keeps paused incremental lanes out of the execution queue unless new evidence changes their expected value; Current Handoff names them, and Session 156 carried the hold forward as a stop condition. The routes chosen after the reset did not move the bound: Route A, a complete physical corner root at \(3.84\)$3.84$, stopped at its representation boundary with no target run, and Route S’s exp-161 encode-only run timed out unresolved (route selection, Research Program Status and Roadmap). The agenda-040 loop registered T-031 and H-232 and moved no bound. At the intake the verified bracket was \(3.826997548829543\ldots \le s(11) \le U\)$3.826997548829543\dots \le s(11)\le U$, a gap of about \(0.0501\)$0.0501$.

What the external intake changed

Kleddamag’s certificate proves \(s(11) > 31/8 = 3.875\)$s(11)>31/8=3.875$. Session 152 retained the pinned v1.0.2 source on 2026-09-22. The container side is \(L = 191/50\)$L=191/50$ and the parent side \(A = 764/775\)$A=764/775$, so the bound is \(L/A = 31/8\)$L/A=31/8$. 679 site orbits expand to 5,284 sites, and 350 positive feature orbits to 2,716 physical features of four kinds: ordinary points, 2-of-3, 2-of-5 and 3-of-5. In units of \(10^{-9}\)${10}^{-9}$ the budget is \(10{,}999{,}479{,}944\)$10,999,479,944$; every core must receive at least \(999{,}962{,}528\)$999,962,528$, so eleven cores need \(107{,}864\)$107,864$ units more than the budget holds. The 12,028 parent half-angle intervals run from \(0\)$0$ to \(207107/500000\)$207107/500000$, past \(\tan(\pi/8)\)$\tan (\pi /8)$. A 2-of-5 feature costs twice its weight, and the review checked that the source’s proof and its budget computation both charge it so (Kleddamag review). The source credits this repository’s T-026.

Which ingredient beat the first-party ceilings is not established. The threshold principle was already here, in T-025 and in sqpack.fractional.threshold. The certificate changes five-site features, movable supports, the parent-centre restriction and the adaptive angle catalogue together, and the review states that no ablation attributes the improvement to any one of them.

It is verified here in three layers:

The case record holds verified_lower_bound: 31/8 on both evidence entries and states that this confirms Kleddamag’s published bound (n-011). The existing T-037 registers that published result at V4/C4; this review adds no new result or C5 claim. The certificate closes 95.89% of the interval from T-026 to \(U\)$U$; the review is explicit that the percentage is not a probability of optimality.

The other external results bear on \(n = 11\)$n=11$ only lightly. Tokoharu’s rectangle-density certificate proves the weaker \(381/100\)$381/100$ here, fully replayed (integration review); wand125’s ten point certificates concern other \(n\)$n$; and Guzhou0806’s R038 scanner enters only as the pinned lineage of Kleddamag’s JavaScript sweep.

The first-party record was reconciled to it. Session 154 kept T-033 registered at V4/C3, rescored from S5 to S3 as method and calibration evidence, and corrected T-024 from C4 to C3, because a derived dilation claim takes the minimum rung over its single exact-algebraic derivation. The integration review’s instruction for research is that a first-party rung below \(3.875\)$3.875$ is controlled evidence or a simpler certificate, not a public lower-bound advance.

After the intake: explorations, reviews, and the settlement ladder

PR 230 published three explorations and moved no bound. Session 155 retained three diagnostic tools, seven receipts and 31 shaped idea rows, and registered no hypothesis.

• X-043 lays out six architectures for stronger counting bounds, from charge-deficit counts on a certificate’s own low-charge poses and co-designed core menus to group budgets, a capture theorem ending in Trump’s ball, a positive-semidefinite kernel, and small higher-order exclusions. Its token-group spike on Kleddamag’s ten 2-of-5 orbits found zero budget saving in all four eligible unions.
• X-044 maps what transfers between the low open cases, keeps \(n = 11\)$n=11$ first and makes \(n = 12\)$n=12$ the next mathematical target.
• X-045 aims at the exact value. Its cutoff composition theorem: given a witness at \(U\)$U$, attainment, a verified \(s(11) \ge L\)$s(11)\ge L$, and every local side minimum with side in \([L, U]\)$[L,U]$ having side \(U\)$U$, then \(s(11) = U\)$s(11)=U$. It proves that there are finitely many local-minimum side values, since the local minimizers form a semialgebraic set with finitely many components on each of which the side is constant, so some cutoff \(L < U\)$L<U$ exists, with no effective value. Throughout \([31/8, U]\)$[31/8,U]$, at most three squares touch any wall. An exact audit adds two negatives: Trump’s top-right corner is empty, so an all-four-corners premise is false, and Kleddamag’s first row already fails at \(U\)$U$, its unchanged core capping that row near \(3.8750124\)$3.8750124$.

Session 156’s reviews changed what counts as progress. Four independent reviews of PR 230 found no fatal error (PR 230 review):

1. No counting certificate can prove \(s(11) = U\)$s(11)=U$. With \(31/8\)$31/8$ known, X-045’s cutoff statement is equivalent to \(s(11) = U\)$s(11)=U$ rather than a partial result; its operational residue is that first-order descent is an admissible leaf.
2. Settling \(n = 11\)$n=11$ is verified global optimization, and the angles are the bottleneck; the X-045 reviewer proposed a rigorous H-112 as the first theorem milestone.
3. Kleddamag’s certificate has no side headroom. Its least core collar \(A - B\)$A-B$ is \(3.26 \times 10^{-9}\)$3.26\times {10}^{-9}$, so the unchanged-core ceiling is \(31/8 + 10^{-8}\)$31/8+{10}^{-8}$, and 11,981 of its rows attain their minimum at the corner-flush parent pose. Any certificate gain at \(n = 11\)$n=11$ needs an adaptive parent-core producer with 2-of-5 and 3-of-5 features, which the record does not have; the cheapest sound next form is H-155’s corner two-band count. Session 156 records these collar and corner-pose figures as exploratory computations.
4. Frozen-weight low-n transfers are arithmetically dead at the old direction nets.
5. The retained evidence is sound: all seven receipts replay to identical exact values.

X-046 turns settlement into a ladder. X-046 finds no dimension-reduction lemma that is both provable with current tools and strong enough to remove angle dimensions. The angle-merging normal form H-121 is the conjecture in another form, not a lemma on the way to it. What can be proved is a ladder of restricted-family theorems, each strengthening Stromquist’s Theorem 3, which puts every packing oriented only at \(0^{\circ}\)$0^{\circ }$ and \(45^{\circ}\)${45}^{\circ }$ at side at least \(2 + (4/3)\sqrt{2} \approx 3.885618\)$2+(4/3)\sqrt{2}\approx 3.885618$, \(U + 0.008534\)$U+0.008534$:

Each box is decided by replacing every square with its rotational core, the intersection of the square over its angle window, so that each leaf is an exact rational Farkas or dual certificate with no interval arithmetic inside the linear program. A full search is priced by two constants: \(c\)$c$, the side lost per radian of box width by the relaxation, and \(V(\varepsilon)\)$V(\epsilon )$, the volume of \(\lbrace f \le U + \varepsilon\rbrace\)$\{f\le U+\epsilon \}$ modulo symmetry. Until both are measured, X-046 prices “settle by search” as between a week and never. Its four unretained f64 probes include one showing that Kleddamag’s per-row minimum charge falls by 68.2% at the axis angle when the container grows to ratio \(3.877084\)$3.877084$, so the certificate carries no transferable slack to \(U\)$U$.

Three experiments ran the ladder’s first lanes the same night.

• exp-227, H-237: the growth-cone route cannot beat Trump’s radius. The exact minimum growth of the side over the whole direction sphere is \(0.0517714532056682325\ldots\)$0.0517714532056682325\dots$, 4.5 times the isolation packet’s uniform modulus \(\kappa \approx 0.01148\)$\kappa \approx 0.01148$. But an exhaustion lemma shows that any certificate bounding each row’s second-order remainder separately is capped by the BC-199 weighted modulus, which is where \(\rho\)$\rho$ came from; the computation confirms it on all 8,448 faces. Along the binding direction 36 of 42 rows do not recover at second order, so what binds is the remainder model, not the geometry. H-237 is exhausted; its successor is idea 246.
• exp-228, H-238: the census found no third orientation below Stromquist’s value. 1,000 jolted starts about Trump’s and Stromquist’s packings were quenched and passed through a new descent filter, which rejects an endpoint only with an exact rational packing verified at least \(10^{-8}\)${10}^{-8}$ below it. It refuted all 85 quench stops with three or more orientation classes below \(3.885618\)$3.885618$. Two descent-stable minima within \(U + 0.02\)$U+0.02$ are new to the record: a two-orientation packing at \(0^{\circ}\)$0^{\circ }$ and \(41.56^{\circ}\)${41.56}^{\circ }$ with side \(3.8867460286\)$3.8867460286$, and a three-orientation packing with no free squares at \(3.8943218738\)$3.8943218738$. Only 94 quenches converged under host load, and the census cannot be replayed bit for bit. H-238 is confirmed at its declared census scope only: numerical observation, not proof.
• exp-231, H-236: rung 0 is mostly closed, at a thousand times its estimated cost. The producer fixed_angle_tree.py and the independent reader fixed_angle_tree_check.py passed their controls, among them the \(n = 5\)$n=5$ family closing at \(s(5) - 10^{-3}\)$s(5)-{10}^{-3}$ in 229 nodes. A W2 review found the certificate contract sound, with one material finding: the registered \(n = 11\)$n=11$ negative control is met only at producer level (rung-0 review). In about 6.4 hours of wall, 198 of 256 subtrees closed on \(1.19 \times 10^8\)$1.19\times {10}^8$ nodes; 58 remain at the wall cap. The reader accepted all 84,777,070 exact leaf certificates and 14,041,104 branch nodes, the three Trump-degenerate leaves close through the BC-240 local theorem, and no leaf below \(U\)$U$ has appeared. Exp-232 then ran the last 58 with the same bytes, and the reader closed the complete tree: 119,556,859 leaf certificates and 19,883,887 branch nodes, three Trump-degenerate leaves, no unresolved leaf. H-236 is confirmed: at Trump’s own angle, within \(10^{-6}\)${10}^{-6}$ in the half-tangent, no packing beats \(U\)$U$; its terminal leaves use BC-240’s first clause, verified and exact since the BC-241 closure. After a Fable max review it is registered as T-035, the machine-verified reduction to the BC-240 ball, and T-036, the composed optimality theorem. The whole tree cost about \(1.7 \times 10^8\)$1.7\times {10}^8$ nodes. Each added square multiplies the tree by roughly six or seven, so rung 1 is out of reach with this relaxation; the lever is a stronger bound per node, not more boxes.

What worked and what did not

One dependency sits outside the record: the rung-0 tree is 5.5 GB in the Session 156 worktree’s attic/rung0/, so resuming it depends on that directory surviving.

Identified but not pursued

The owner’s 2026-09-14 hold still stands, and the owner’s decision on retiring H-121 as a route, which X-046 recommends, is open. Statuses below are the ledger’s and the idea board’s; blockers and next steps are those the records name.

Registered \(n = 11\)$n=11$ hypotheses that are open, blocked or stopped:

Idea-board rows not yet registered, from X-043, X-045, X-046 and exp-227, with the older \(n = 11\)$n=11$ rows they touch:

Three directions the PR 230 review lists as missed are not yet rows: symmetry canonicalization on the cover side of a verified search; a threshold-language ceiling family near \(3.876\)$3.876$, to bound how far counting can reach; and the pruning tests of the verified-global-optimization literature, from Markót and Csendes’s circle packings to Montanher and coauthors’ unit squares in a circle.

The exact n = 11 result

Established. \(s(11) = T = 3.877083590022814\ldots\)$s(11)=T=3.877083590022814\dots$, the exact side of Walter Trump’s packing. T-011 verifies the algebraic witness and T-060 supplies the matching global lower bound for arbitrarily rotated unit squares with disjoint interiors and boundary contact allowed. The latter is Queuingtheorydotcom’s Astra-assisted proof, building on this project and Kleddamag, independently replayed and mathematically audited here at V3/C3/S5.

The proof review maps the 2,184 canonical patterns, 2,180 exclusions, four symmetric survivors, exact D4 bridge, complete capture tree and fixed-side local isolation. The replay uses pinned source inputs and shares the mathematical geometry primitives disclosed in the review; it is an exact computational proof audit, not a proof-assistant formalization or a second independent method. Four final-state digests in the publisher’s cached audits are stale, so those cached PASS records do not establish the claim; the fresh source-bound replay and final composition do.

Kleddamag’s \(s(11) > 31/8\)$s(11)>31/8$ (T-037) remains an earlier, independently verified lower bound. The restricted six-plus-five theorem and local Trump theorem (T-035 and T-036) retain their own scopes. The separate wand125 ceiling and row-minimum reports (T-058 and T-059) have not been promoted by T-060’s verification. Global optimality of the side does not assert uniqueness of the optimal arrangement. The earlier research program and its unpriced routes are retained in X-046 as the history of how the gap was approached before this proof.

Theoretical Results

Results state their assurance and basis rather than compressing both into a tier name. verified below is formal; numerical rows say numerically-checked and name their method. A mathematical proof may be external, locally audited, or replayed here, and that origin remains visible in the frontier evidence. The results themselves carry the same distinction: T-1 confirms a published construction, T-2 is elementary and proved in place, and T-3 and T-4 are apparently novel—first established here and, to the best of this project’s knowledge, not previously published; computer-assisted and not externally peer-reviewed. Assurance, Methods, and Claims defines the qualification.

Results relied on from the literature

Cited near the claims they support in the n = 11 report; listed here so the dependencies of this program are explicit.

• \(s(10) = 3 + \tfrac{1}{2}\sqrt{2}\)$s(10)=3+\frac{1}{2}\sqrt{2}$, Stromquist 2003, Theorem 1. Ten unavoidable points, then case analysis. Not pigeonhole alone.
• The published statement \(s(11) \ge 2 + 4/\sqrt{5}\)$s(11)\ge 2+4/\sqrt{5}$, Stromquist 2003, Theorem 2. D-152 and exp-016 give a strict counterexample to the printed Figure 14 unavoidability claim, so the published proof is not relied on as complete. The same inequality is established independently as T-4 below, using H-041’s separately preregistered source-distinct repaired point set.
• \(s(11) \le 3.877083590022814\ldots\)$s(11)\le 3.877083590022814\dots$, Trump 1979, by construction. Every upper bound in this subject is a construction; no non-constructive upper bound has ever been obtained.
• The \(0^{\circ}\)$0^{\circ }$/45° class cannot achieve it. Stromquist bounds that orientation class below at \(2 + (4/3)\sqrt{2} \approx 3.885618\)$2+(4/3)\sqrt{2}\approx 3.885618$, which Trump’s oblique packing beats. This makes \(n = 11\)$n=11$ the first case where genuinely oblique tilt is proved to improve on the \(0^{\circ}\)$0^{\circ }$/45° class, and is the sharpest available statement of why the target differs structurally from the ladder.

Results established here

The authoritative, prioritized list of whole results is now the results register (packing/frontier/results.yaml), graded on the verification and confirmation ladders epistemics.md defines and re-derived by devtools/check_results.py on every validation run; the repair below is registered there as T-010, the Trump validity check as T-011. This section keeps the original \(n = 11\)$n=11$ statements with their replay commands — the single-digit T-N ids are this document’s declared shorthand, retained where the surrounding prose cites them, and the structural results T-2 and T-3 live only here and in their registry artifacts.

T-1 is also an independent check of the published record: the 33 digits on the Squares in Squares record page agree with the value computed here from the field. The 14 zero-gap pairs are precisely the ones a finite point evaluation cannot decide as exact contacts.

T-2 originated in the standing review as observation R-2 and has now been implemented twice, independently—see below for why that matters.

T-014, the newest whole result: Goebel’s \(n = 5\)$n=5$ optimum is locally rigid at fixed side, proved exactly. For \(s = 2 + \sqrt{2}/2\)$s=2+\sqrt{2}/2$ and Goebel’s labeled pose \(P^0\)$P^0$ in \(C = (\mathbb{R}^2 \times S^1)^5\)$C=({ℝ}^2\times S^1{)}^5$, \(P^0\)$P^0$ is an isolated point of Feas(s) — closed unit squares in \([0, s]^2\)$[0,s{]}^2$, pairwise disjoint interiors — equivalently there is no nonconstant continuous feasible path from \(P^0\)$P^0$ and no sequence of distinct feasible poses converging to it, so the packing is rigid at fixed side in the catalogue’s sense. The proof is exact over \(Q(\sqrt{2})\)$Q(\sqrt{2})$: one intrinsic half-angle chart, all 400 elementary inequalities classified by exact sign, a neighbourhood cut out by 128 strict conditions on which the local feasible set is exactly twenty active rows, T-012’s first-order cone and non-negative self-stress transferred to that chart, then semialgebraic curve selection on the punctured feasible set and an induction on a putative arc’s Taylor coefficients that the self-stress contradicts at order \(2m\)$2m$. It is registered at V3/C5 — the exact quantities are machine-confirmed here, the two steps that close the argument are an audited proof, no instrument decides isolation, and that C3 is raised to C5 by the mapped review artifact below, rather than to C4 by a second method — and apparently-novel at S3 on BC-153’s independent review, which rebuilt every exact quantity from scratch in code sharing nothing with the author, replayed the instrument from clean roots, and accepted the novelty basis: Kingbird asserts the property with no argument, Goebel does not state it, and Friedman does not annotate it. Not claimed: any isolation radius; rigidity with the container side free, which X-007 measured to be false; global uniqueness; any other \(n = 5\)$n=5$ optimum; applicability of the Connelly–Whiteley tensegrity theorems as stated; and any novelty of method — the closing principle is the classical second-order sufficient optimality condition, and the proof shape is Connelly–Whiteley 1996 Theorem 4.3.1’s. The proof is X-012, the round is exp-058, and the review’s six named gaps are listed in that record’s amendment. None is a condition of the pass, and one of them is the unread printed page of the cited curve-selection lemma.

Apparently novel here, in the qualified sense above: the falsification of Stromquist’s printed Figure 14 argument and the source-distinct repaired certificate for \(s(11) \ge 2 + 4/\sqrt{5}\)$s(11)\ge 2+4/\sqrt{5}$ (exp-016, exp-017); the corner at Trump’s cell (T-3, exp-010); the local-isolation theorem for Trump’s pose (exp-013); and the exact \(n = 5\)$n=5$ terminal-family chain—shared optimal face, two-parameter sheet, second-order obstruction, complete first-order inventory, and connected position polytope (exp-033 through exp-039); and the verified relaxed rational witness at \(n = 29\)$n=29$ (E-n029-schadt-rational-upper), a new construction proving a slightly weaker bound than the reported record. The \(n = 3\)$n=3$ and \(n = 4\)$n=4$ quotient classifications are established here with no novelty claim: the published hard-squares computations cover their labelled and unlabelled pieces, and the record declines to call the quotient refinements new. T-3 was found while building the quench, registered as H-019 before the round that observed it was recorded, and confirmed as its own round. Under the directory’s ownership rule the registry artifact decides both; the T- ids here are this document’s shorthand.

The Cell Decomposition

The result the refiner rests on, stated so it can be checked.

Setup

Fix \(n\)$n$ unit squares. A configuration is

• a centre \((x_i, y_i) \in \mathbb{R}^2\)$(x_i,y_i)\in {ℝ}^2$ and an angle \(\theta_i \in [0, \pi/2)\)${\theta }_i\in [0,\pi /2)$ for each square \(i\)$i$, and
• the container side \(s\)$s$,

so \(3n + 1\)$3n+1$ real coordinates in all, which is 34 at \(n = 11\)$n=11$.

The four corners of square \(i\)$i$ are \((x_i, y_i) + R_i\cdot(\pm\tfrac{1}{2}, \pm\tfrac{1}{2})\)$(x_i,y_i)+R_i·(\pm \frac{1}{2},\pm \frac{1}{2})$ where \(R_i\)$R_i$ is rotation by \(\theta_i\)${\theta }_i$. Write \(o_{ik} \in \mathbb{R}^2\)$o_{ik}\in {ℝ}^2$ for the four corner offsets, \(k = 1\ldots4\)$k=1\dots 4$. Once \(\theta_i\)${\theta }_i$ is fixed the \(o_{ik}\)$o_{ik}$ are constants, and every corner is an affine function of the centre alone.

Two squares have disjoint interiors exactly when some line separates them, and for convex polygons it suffices to test lines parallel to their edges. A square has two distinct edge normals (opposite edges are parallel), so a pair has four candidate axes; these too are functions of the angles alone.

Define a cell of the configuration space to be a choice, for each of the \(C(n,2)\)$C(n,2)$ pairs, of one candidate axis together with an order (which square lies on the low side). A configuration lies in a cell when that axis genuinely separates that pair in that order.

Statement

T-2. Fix the angle vector \(\theta\)$\theta$ and fix a cell \(C\)$C$. Then

minimise   s
subject to  the configuration lies in cell C and inside [0, s]²

is a linear program in the \(2n + 1\)$2n+1$ variables \((x_1,\ldots,x_n, y_1,\ldots,y_n, s)\)$(x_1,\dots ,x_n,y_1,\dots ,y_n,s)$.

Why

Four observations, each immediate once the angles are fixed.

1. Corners are affine in the centres. Corner \(k\)$k$ of square \(i\)$i$ is \((x_i, y_i) + o_{ik}\)$(x_i,y_i)+o_{ik}$ with \(o_{ik}\)$o_{ik}$ constant.
2. Containment is linear. Each corner must satisfy \(0 \le x_i + o_{ik,x} \le s\)$0\le x_i+o_{ik,x}\le s$ and \(0 \le y_i + o_{ik,y} \le s\)$0\le y_i+o_{ik,y}\le s$. Note that \(s\)$s$ appears here, and only here, as a variable.
3. Separation along a fixed axis is linear. For axis \(\nu\)$\nu$ and order (i before j), separation says every corner of \(i\)$i$ projects at or before every corner of \(j\)$j$: \(\langle \nu, (x_i,y_i) + o_{ik} \rangle \le \langle \nu, (x_j,y_j) + o_{jl} \rangle\)$⟨\nu ,(x_i,y_i)+o_{ik}⟩\le ⟨\nu ,(x_j,y_j)+o_{jl}⟩$ for all \(k, l\)$k,l$. Since \(\nu\)$\nu$ is a constant vector, each is a linear inequality in four of the variables.
4. The objective is linear, being \(s\)$s$ itself.

The nonlinearity of the original problem is entirely in two places: the trigonometric dependence of \(o_{ik}\)$o_{ik}$ and \(\nu\)$\nu$ on the angles, and the discrete choice of cell. Neither is present once both are fixed.

Note what the statement does not claim. The LP optimises within one cell. A different cell may have a lower optimum, and finding the best cell is the combinatorial part of the problem, which none of this makes easy.

A cell is not a basin, and this trap has been walked into

The statement above fixes the angles and a cell. A point-basin does not: it is the preimage of a quench endpoint, and the quench moves the angles and may cross cells. So a configuration can sit at exactly its fixed-angle cell optimum and still be far from its quench endpoint, with every remaining unit of gap in the angles and none of it in the centres.

Nor does a point-basin classify a flat terminal component

The section above separates a fixed-angle cell solve from the full quench. There is a second separation, discovered later and the harder of the two: the quench returns a point, while the terminal optimum need not be isolated.

Where the optimum is flat, two quenches into the same connected terminal component can legitimately stop at different places in it. Every symptom then mimics a real discovery—distinct coordinates, distinct geometric keys, two rows in the atlas—while the side agrees exactly and an open stratum can share one contact graph. Neither the key nor that graph alone decides component identity; wall strata can change inside the same connected family. That is D-034, and the shape of the error is the same as the cell/basin trap: an object that fixes more than the mathematics does, mistaken for the mathematics.

The consequence is a reading that looks safe and is not: a fixed-angle solve that stops improving has not converged to a local optimum of the problem—it has run out of things it is allowed to move. Watching it flatten and concluding “wrong basin” is exactly backwards, and it is what the right basin looks like when the residual is angular.

That is not hypothetical. Checking exp-001’s polish/exploration split, an agent built a probe doing one LP solve at fixed angles, called it “the quench”, and retracted a correct finding when it stalled (D-029). On exp-002’s seed 2:

“Quench” names all three stages—solve the cell, re-read the cell to a fixed point, refine the angles. The cell solve alone is one third of it and answers a different question. devtools.check_regressions pins this discrimination under D-029.

Two implementations, on purpose

The row count depends on how separation is written, and this directory now has both forms:

Both are correct formulations of the same feasible set, and neither shares constraint-assembly code with the other. That redundancy is deliberate, and it is the postmortem’s rule R1: a component checked against its own model of correctness is checked against the thing most likely to be wrong. D-014 happened precisely because the quench was validated only against its own constraint rows.

The instance: Trump’s cell

cases.trump11.independent_lp_cell reads the cell off sqpack’s exact certificate—eleven angles and fifty-five axis choices, and nothing else—rebuilds the LP from scratch, and solves it. The centres are never given to the solver. They are what it must reconstruct.

The cell, read off the exact certificate
  distinct angles:  [0.0, 40.18193729] deg
  tilted squares:   [6, 7, 8, 9, 10]
  axis choices:     55 pairs
  LP shape:         23 variables, 1056 constraints  (= 16 x (11 + 55))

Solving it, without telling the solver where the squares go
  LP optimum        s = 3.8770835900228136
  exact value       s = 3.8770835900228140
  |difference|        = 4.441e-16
  worst centre error  = 1.332e-15

sqpack.quench’s single-cell solve at the same angles agrees to the digit—4.441e-16, recorded as a mechanism result of exp-006. The cell containing Trump’s packing, solved as a linear program, is Trump’s packing, through two unrelated constraint sets.

What “exact” does and does not mean here

The formulation is exact; the build is not, and conflating the two caused a critical defect. Three corrections, recorded in the plan spec’s revision note:

• A float LP solver does not deliver the cell optimum. At its default primal feasibility tolerance of \(10^{-7}\)${10}^{-7}$ HiGHS returned a packing violating its own separation constraint by \(9.876 \times 10^{-8}\)$9.876\times {10}^{-8}$, and so a side below Trump’s (D-014). Pinned at the solver’s floor of \(10^{-10}\)${10}^{-10}$, and with every returned solution post-checked against the constraints imposed on it, the residual in the side is about \(10^{-11}\)${10}^{-11}$. That floor is D-021, still open, and eight rounds sit on it.
• The polish step does not produce exact output. R-2 said it produced rational output; HiGHS returns floats. Exact output needs an exact LP over the cell’s certified rational or algebraic coefficients, which is unbuilt and tracked.
• A finite-precision LP endpoint remains a numerical result. Earlier records called this precision stage polished; that local label was retired because it says neither which arithmetic ran nor what precision was achieved. The method is numerical-f64, its actual tolerance and residual must be recorded, and it is only numerically checked. Formal promotion requires a separate exact or rigorous certificate that sqpack can replay.

Thirty-four dimensions become one

Trump’s packing uses two distinct angles: \(0^{\circ}\)$0^{\circ }$ on six squares and \(a^{\ast}\)$a^{*}$ on five. Holding the cell fixed and varying the single free angle gives a function

φ(a) = the LP optimum of Trump's cell with the five tilted squares at angle a

which is the entire problem, restricted to this cell, in one variable.

A 2,001-point scan of \([38^{\circ}, 42^{\circ}]\)$[{38}^{\circ },{42}^{\circ }]$ puts the minimum at \(40.182^{\circ}\)${40.182}^{\circ }$, one grid step (\(0.002^{\circ}\)${0.002}^{\circ }$) from \(a^{\ast}\)$a^{*}$.

Trump’s angle is not an input to this computation. It is the argument that minimises a one-dimensional function anyone can plot. For this structured cell, the centre coordinates remain LP variables and only one nonlinear angle parameter remains. This demonstrates a useful compression, not a theorem that angle-class count equals the local dimension of the full packing problem; other records already use more classes, and each reduction must be derived from its contact structure.

The Corner, and the Method It Forced

The most useful result the campaign has produced, because it is a full loop: a measurement, a mechanism, a prediction, and a method built on the prediction that works.

The measurement

\(\varphi\)$\phi$ is not smooth at its minimum. Measuring one-sided slopes and refining the step:

Both converge, and they converge to different values, ratio \(2.1973\)$2.1973$. The derivative does not vanish at \(a^{\ast}\)$a^{*}$; it jumps.

exp-010 measured the same quantity through sqpack.quench—a different LP formulation, a different code path—and recorded \(0.1747\)$0.1747$ and \(0.3841\)$0.3841$, ratio \(2.198\)$2.198$, stable over five decades on each side. Two implementations, one number.

The mechanism

Where the LP’s optimal basis is locally constant, \(\varphi\)$\phi$ is smooth and its derivative is read off that basis. A corner occurs where the optimal basis switches as \(a\)$a$ crosses \(a^{\ast}\)$a^{*}$. Because a basis is only a subset of the active rows, a basis switch alone does not show that the full active-contact set changed. The switch at the minimum establishes a kink in this one-dimensional class-angle objective. It does not by itself prove rigidity of the full packing; that requires ruling out every other feasible motion, not just motion along this slice.

The prediction, and what it cost to ignore

A kink invalidates derivative-based smooth local models, but does not imply that every derivative-free method must fail. In this implementation and from these starts, exp-006: finite-difference descent stalled five orders short, and Powell and Nelder-Mead both did worse than descent (\(+1.06 \times 10^{-2}\)$+1.06\times {10}^{-2}$ and \(+3.34 \times 10^{-6}\)$+3.34\times {10}^{-6}$ against descent’s \(+2.78 \times 10^{-7}\)$+2.78\times {10}^{-7}$).

The method, and what it bought

Replace the smooth descent with a bracketing search over merged angle classes—a method that tolerates non-smoothness—and hold everything else fixed. On the same annealer output:

Seven orders at \(n = 5\)$n=5$ and twelve at \(n = 10\)$n=10$, from changing only how the angle half searches. At \(n = 5\)$n=5$ both quenches find the same contact structure and the same two angle classes, so the difference is entirely in whether the search can land on the corner.

This is strong method-selection evidence, not a convergence theorem. The successful bracketing run and the failed tested alternatives justify the current implementation choice; H-019 does not prove that every derivative-free method fails or that bracketing is necessary.

And what it did not buy

Nothing at \(n = 11\)$n=11$. The bracketing quench moves the target from \(8.85 \times 10^{-2}\)$8.85\times {10}^{-2}$ to \(6.29 \times 10^{-2}\)$6.29\times {10}^{-2}$ (exp-009), against machine precision on both proved instance cells. The tested starts remain far from Trump’s construction after the local procedure. An LP-in-cell solve is local: it returns the best packing in the cell it is given. That explains the lack of rescue without deciding whether the endpoints belong to a distinct terminal component.

Other consequences

• The refiner is an LP solve per cell, at solver precision, and it is built. That is the campaign’s middle tier, and it is real.
• Terminal endpoint observations become inspectable. The free-angle pass removes one merge-tolerance artifact and returns a pose with side length good to \(\approx10^{-11}\)$\approx {10}^{-11}$, so retained endpoints can be compared and replayed. It does not make local minima discrete or define component identity: the exact \(n = 3\)$n=3$ continuum proves that one connected stationary family can produce many endpoint keys. A census, atlas, or basin statistic remains inadmissible until the component relation is resolved (D-020, D-034).
• The search space factorises into a small continuous part (the angles) and a combinatorial part (the cell), which is the premise of H-001—now with a concrete prior, since the class-constrained search reached the solver floor in 70 LP solves where free descent needed 1,024 and landed five orders worse.
• Rational-slope tilts would need no number field. At a Pythagorean angle such as \(\arctan(3/4)\)$\arctan (3/4)$ every coordinate and the cell optimum are rational, so exact verification would be \(\mathbb{Q}\)$\mathbb{Q}$-arithmetic at degree 1. Realising that needs the exact rational LP, which is unbuilt.

Reproducing all of it

cd packing
uv run --frozen python -m cases.trump11.verify_exact
uv run --frozen python -m cases.trump11.independent_lp_cell
uv run --frozen python -m cases.campaign_smoke.quench_experiment
uv run --frozen --group dev packing-validate

cases.trump11.independent_lp_cell asserts every figure quoted above, including agreement with H-019’s registered slopes, so a change that breaks one fails the gate rather than silently editing the record.

The Program So Far

Deliberately historical: it records the order in which things were done and why, because several decisions were made by measurement and the measurements are why later work is shaped as it is.

Establish the frontier, then the mathematics. The \(n \le 100\)$n\le 100$ corpus was built first, one validated artifact per case, so that “the standing best” is a fact read from a file rather than a number retyped into a paragraph. Retrieving the primary sources corrected the record in ways secondary summaries had not: one widely-repeated explicit constant appears in no primary paper at all. That episode is why the grounding rule for every later lane is that nothing enters a prompt or an artifact unverified.

Build the exact verifier before the search. Rigidity means a float check cannot decide record packings, and the tolerance blind spot is a correctness concern rather than a rounding one. sqpack was written, validated against Trump’s packing (T-1), and given a negative control demonstrating both float failure modes.

Price the stack rather than argue it. The pipeline spans seven orders of magnitude, from a 0.025 µs annealer move to a 129 ms exact verification, and its middle—the LP quench at 1.28 ms—is where nearly every planned strategy spends its time, at the same rate in any language. So the spine is Python, and compiled code is deferred to a phase scoped by a profile of a campaign that has actually run.

Write the search engine; two formulations failed first. Fixing a container side and asking whether the squares fit needs an outer loop that decides when an anneal has failed, and it starts from the trivial grid, which is exactly jammed. Two versions were built and measured: the first crawled, the second never left the grid basin (D-001). The replacement removes the container from the variables, minimising required_side + λ·total_overlap with a linear penalty.

Run the baseline, and discover the instrument was lying. A restart cap stopped every chain before the declared move budget did, so --budget-moves was inert and two strategies compared “at equal budget” would have had unequal work (D-002). The tell was that results got worse at a larger declared budget.

Add the method, and find the missing stage. A standing review audited the toolkit documents and found that all of them presumed a refinement stage none of them built. In looking for it, the review found T-2 and supplied the experimental method the project lacked: a hypothesis register with kill criteria written before the run, a run protocol, and a seven-series plan.

Adopt a strategy, and register the premise so it can fail. Record packings may be unusually constrained and may have low hit probability under specified baseline proposers. If so, scaling the same proposer multiplies effort against the measured probability. Because the whole strategy rests on that argument, the measurement that would refute it (H-012) is registered in the cheapest tier and scheduled early.

Ask what the premise silently assumes about its denominator. Optima need not be isolated: the exact \(n = 3\)$n=3$ terminal family proves that one connected optimal component can produce many endpoint keys. So the census that is supposed to establish rarity is counting representation-dependent objects, and the denominator of “rare” is not yet a number (D-034). The premise may well be true. It is not yet measurable, which is a stronger objection than doubting it.

Ask whether the basin has a wall, and get a better question back. exp-005 started inside Trump’s packing and walked outward. There is no wall to find: the return distance is linear in the perturbation over four decades with no threshold, and halves when effort is multiplied by ten. What was measured is the refiner’s convergence rate, not a basin radius. The sharper result was incidental—started \(10^{-5}\)${10}^{-5}$ from a configuration that has stood since 1979, the campaign’s default annealing schedule wanders off and lands with a median side gap of \(0.27\)$0.27$, worse than it reaches from cold starts.

Build the quench, and have it beat the record. The first working version reported a side below Trump’s. The runbook’s pre-registered rule held—a run that beats the record has found a bug—and it had (D-014). The fix pinned the solver tolerance and post-checks every solution against its own constraints; the postmortem generalised it into four rules and a soundness perimeter that every configuration- emitting component now joins.

Follow the corner. The quench’s angle half stalled, the reason turned out to be geometric rather than numerical, and acting on it took the two proved instance cells to machine precision. That chain runs exp-006 to H-019 to exp-007–exp-010, and is the campaign working as designed.

How rounds are run

The full contract is the runbook; the parts that matter for reading the results below follow. The four-cell and five-seed rules apply only to numerical pose-search proposer comparisons. Fractional, theorem, exact-certificate, and review rounds use their own preregistered criteria and method-specific controls.

• Assurance, method, and arithmetic are separate. A result is reported, numerically-checked, or verified; only the last is formal. The method may be numerical-f64, numerical-multiprecision, interval-certified, exact-algebraic, or a proof method. Numerical results record the precision, rounding policy, tolerance, and observed margins actually used. Basin or terminal-component identity requires its own evidence. beat_record: true may only be written for a verified result.
• Five standing instance roles: \(n = 10\)$n=10$ positive control, \(n = 11\)$n=11$ target, \(n = 12\)$n=12$ open-case calibration, \(n = 16\)$n=16$ proved not-below control, and \(n = 17\)$n=17$ mechanism-matched calibration. A guard breach rejects a round regardless of outcome, because it means the instrument is wrong rather than the strategy good.
• Five seeds minimum per cell, median and min–max range both reported. Overlapping ranges mean no detectable effect, never “a small win”.
• Every round declares a timebox before it starts and every terminal round records an effort block. stopped_by is mandatory; wall_seconds, agent_minutes, and pair_tests are recorded when applicable and measured. A round that stopped on its criterion answered its question; one that stopped on its timebox did not, and must name where a successor resumes.
• Three terminal states are distinct: rejected (measured and missed), abandoned (budget gone, no determination, resumable), exhausted (re-running under this regime would add nothing).
• Negative results are kept, and a defective artifact is corrected by dated annotation rather than rewriting.

The Hypothesis Registry

Each claim or open question is codified as an artifact. The standing review’s complete H-001 through H-015 block is now in the registry; later ids carry campaign-native claims and explicit open questions. The ledger is generated from the artifacts and is the current view; this section is the reading of it. Rounds and effort below repeat the ledger’s per-hypothesis totals, which count every round that names the hypothesis, control roles included.

Confirmed

H-019—Trump’s tested shared- tilt slice is non-smooth at the published optimum. Registered by the runner of exp-006 before recording that round, because the round measured something H-002 did not predict; confirmed by exp-010. Elaborated in The Corner above. It is the campaign’s first confirmed claim, and the one that changed a method.

Refuted, and what each refutation bought

H-016. The null: a serious budget on a general-purpose annealer finds the best known packing. Within \(10^{-4}\)${10}^{-4}$ only at \(n = 12\)$n=12$. The refutation is not the interesting part—the two failures were different in kind. At \(n = 10\)$n=10$ later cell polishing showed the candidate had the record’s declared structure and stopped \(4.19 \times 10^{-4}\)$4.19\times {10}^{-4}$ short (polish); at \(n = 11\)$n=11$ it remained \(3.73 \times 10^{-2}\)$3.73\times {10}^{-2}$ above Trump and no terminal-component relation was measured. That operational distinction set the next four rounds without proving a topological one.

H-002. Claimed that alternating LP solves with local angle moves refines any annealer output to the analytic value. Refuted as stated, and the cell-level split is the result:

The word that failed is any. The quench is a polisher, not a rescue: it makes the declared cell optimum reproducible to solver precision, which is an input to the census and atlas, and it does not lift the burden of finding a competitive region off the proposer.

H-018. Predicted an \(\varepsilon\)$\epsilon$ at which the return rate collapses, which would be the basin’s radius. Observed rate at the registered \(\varepsilon = 10^{-3}\)$\epsilon ={10}^{-3}$: 0 of 40 in every arm. The residual scaled approximately linearly with \(\varepsilon\)$\epsilon$ under the tested finite schedules and decreased with more effort. That diagnoses incomplete convergence of this refiner; it does not prove an attracting basin through \(\varepsilon = 10^{-1}\)$\epsilon ={10}^{-1}$, distinguish an isolated endpoint from a terminal family, or establish component membership for the perturbed trajectories.

Blocked, and on what

The priority-1 agenda has two independent bottlenecks. The basin lane is blocked on the measurement system around the quench: terminal-component identity, endpoint classification, event provenance, coverage estimation, independent validity, and a named proposer regime. The proof lane now has both halves of its calibration: exp-016 falsifies Stromquist’s printed certificate, while exp-017 certifies a complete source-distinct repair. The same two-sided falsifier/certificate architecture can now target a new lower bound at \(n=12\)$n=12$.

• H-011 (census at \(n \le 10\)$n\le 10$) needs H-021’s classification evidence, event records, and a coverage estimator.
• H-012 (the premise the cartography programme rests on) needs H-011’s machinery plus an explicit \(n=11\)$n=11$ sampling cell. Kill: record-basin probability within ~10× of the modal basin’s, in which case the cartography program stands down and the campaign reverts to throughput. Still untested, which is the largest open question about the strategy.
• H-001 (angle classes) now has a strong prior from exp-006 but remains unmeasured as a search claim: the class-constrained arm assumed the answer’s own structure, so it shows the angle search method decides the outcome, not that an unguided method would find that structure.
• H-010 (Stromquist calibration) is terminally refuted by exp-016. An exact strict box avoids every printed Figure 14 point, so the five-node conjunction fails at its fourth node. The result rejects the published proof as printed, not the numerical lower bound.
• H-041 (proof repair) is confirmed by exp-017 after moving only G.x from .8 to .79. The complete exact repair proves the same lower bound with 26 repaired Figure 14 faces and thirteen passing mutations; it does not make the published proof correct as printed.

H-017 (100× budget) stays open and demoted behind a short response curve. It is operationally shaped, and D-044 — the boundary that made it inadmissible unattended — is repaired against the producer and independently reviewed. D-044 stands contained rather than fixed: the review of 2026-09-03 returned BOUNDED-CAVEAT, and one clause of the defect’s source finding plus three residuals on the same archive boundary are named in the record and not closed. No live round has passed through the repaired boundary, so admitting it unattended is still a review decision rather than a settled one.

D-460 is the other entry standing contained, and it is a contract gap rather than a finding: agenda-022’s BC-206 declared purpose: research with no hypothesis, and the experiment contract requires at least one, so a cell could be drafted, budgeted, dispatched and completed before anything noticed its output had nowhere to go. Its hundred minutes and thirteen run blocks are retained as nine covering-value rows and a run register — the more accurate description, since nothing was pre-registered and so nothing was tested — but the ledger’s round count and effort attribution do not see them. The check that would refuse the shape at draft time, rather than at the experiment record, is named in the entry and not built.

D-467 stands outstanding, and it is the one entry here that no check inside this repository can close. Two branches allocated D-455, D-456 and D-457 to six different defects while both were open, and the collision repeated one level down at D-458 when the second branch merged. conventions.md already carries the rule — the later branch takes the next free ids and moves its references in the same change — which is what was done, twice, and each renumbered entry says so in its own text rather than only in a commit message. What is missing is detection: the schema enforces uniqueness within a file, which is exactly the property that still holds on both sides of a collision, so seeing one requires comparing against the merge base. That is a merge-time check and it is not built (think-8bcl).

The idea board carries the full registered portfolio alongside raw ideas and dead ends. The registry artifact, not the review’s historical prose or this summary, owns each current criterion and kill rule.

The mutable size-by-size run order lives in the basin-map confidence ladder, not in this status document. It labels every cell as tool validation, measurement validation, or genuine research. The event-retention controls through \(n = 8\)$n=8$ and the bounded \(n = 9\)$n=9$ performance cell are complete. The random-start size ladder stops there. BC-008’s source-bound \(n = 10\)$n=10$ seeded-pose entry point now passes replay and a bounded run-path smoke test. Exp-031 completes its four-perturbation known-answer experiment at 4/4 converged, independently valid, and admissible. Exp-032 completes BC-009: exact \(n = 3\)$n=3$ and \(n = 4\)$n=4$ component controls pass while all 16 retained f64 observations remain unresolved. Exp-033 completes the first bounded BC-010 \(n = 5\)$n=5$ connectivity slice: the equal-side pair shares one exact fixed-angle optimal face. Exp-034 embeds that face in an exact two-parameter angle-and-slide sheet, but complete stationary identity and the unequal-side rows remain open. Exp-035 derives the complete active first-order systems at both endpoints and one interior point and finds an exact direction outside that sheet in every owner branch; exp-036 excludes that displayed direction from the true Bouligand tangent cone by exact second-order inequalities in both owner branches. Exp-038 completes the first-order inventory with identical owner-branch V-representations, eight endpoint quotient rays, six interior quotient rays, and both derived face vectors. Transverse and mixed nonlinear realization remains open.

Sessions Conducted

An experiment records what was measured about square packing. A session records what an agent did for a stretch of hours, and until recently it recorded that without recording what the stretch cost: phases and outcomes were in one file while harness measurements were elsewhere, and nothing joined them. session-close-report.yaml is that join, one validated entry per session, written by devtools.close_session --render from the session records and the rollups rather than from anybody’s recollection, and drift-checked in packing-validate --records. The tables below are its reader-facing view.

Two numbers here are easy to get wrong in the same direction, so both are stated. A session’s cost is not a share of a log, and the campaign’s cost is not a sum of sessions. Several sessions can run inside one harness log, each legitimately declaring the whole of it; charging it to each of them read as 117.9 hours for a campaign that had spent 43.7, so every total is taken over distinct rollups and the shared log gets its own row rather than a footnote. And a receipt exists on disk whether or not a session claims it, so the ones nobody claims are counted rather than dropped — the gap between those two rows is coverage, not rounding. Claude’s branch-aware log totals and Codex’s declared task-tree intervals stay in separate tables: their units differ, and the same work can appear in both.

Unmeasured sessions include live work awaiting a retained receipt and older closed sessions whose harness logs were not retained. Missing measurements are not zero cost. The Claude rollups no session claims are the delegated half of the same period: sub-agent logs that survived while the session records that would have claimed them predate the field. Claude backfill needs only a retained log; Codex interval refresh needs the root task id and the two declared cutoffs. The relevant generator writes the receipt, and the entry fills in on the next close_session --render.

Experiments Conducted

There are 187 rounds registered in series-000.

They record 2512.1 agent-minutes and 5729.8 wall-minutes. These totals exclude four historical annealing rounds with unrecorded timing; their wall and operator costs are unknown, not zero. Exp129 closed as blocked without invocation and contributes zero scientific elapsed time; its source-free development and review costs belong to Session097. Exp-114 completed its one target and independent replay. Reader development costs are recorded separately from those process times. Exp-056 stopped at its fixed timebox with a 170-row agreeing prefix and no canonical result; exp-057 stopped before target access; exp-058 stopped on the review it was waiting for, which arrived and accepted it. Exp-058 records no agent-minutes, because the lane that produced its mathematics did not retain its operator time; the agent-minute total above therefore understates what H-060 has cost. Their instruments are sqsearch 0.1.0 (the f64 screening annealer), sqpack.quench (0.1.0 with angle descent and 0.2.0 with class bracketing), the high-precision Kingbird SVG reconstruction, the exact Trump linearized-cone checker, the exact small-moduli checker, the exact Stromquist printed-set falsifier, and the exact repaired-cover certificate, the exact terminal-component known-answer checker, and the exact \(n = 5\)$n=5$ fixed-angle face, angle-sheet, full-angle tangent, and second-order obstruction checkers, plus the exact branchwise tangent-inventory checker. Exp-058 alone used no repository instrument: its numbers come from read-only sympy scripts retained verbatim in its results record, which is why it is not a receipt.

No record-search round has produced verified assurance, so no result below claims a new record. Exp-012 is an exploratory reconstruction of a published record witness; its six-class determination leaves H-024 unresolved because the source has no formal feasibility certificate. Exp-037 separately rejects H-042’s serialization-scoped three-class claim. Neither round certifies the source geometry or optimality.

The roughly 100-digit retained n = 29 witness is evaluated at 160 decimal digits of working precision and passes all 406 pair checks at tolerance 1e-80. The figure therefore says “numerically checked,” not “verified,” “exact,” or “proved optimum.”

Roll-up

Every figure is lifted from the round’s frontmatter, which is lifted from the JSONL archive beside it.

Cost and provenance

What the 187 rounds jointly establish

The 187 rounds use 2512.1 agent-minutes and 5729.8 wall-minutes under the campaign’s retained effort accounting. The never-invoked exp129 adds no scientific result or execution time. Exp-114 contributes 2.46 seconds of target/replay effort; its readiness work is recorded separately in Session089.

The numerical basin event trust boundary now retains complete declared blocks through \(n = 8\)$n=8$ plus one bounded \(n = 9\)$n=9$ performance event; exact component controls pass only at \(n = 3\)$n=3$ and \(n = 4\)$n=4$. Exp-018 through exp-020 retain twelve independently valid historical v2 poses at \(n=3\)$n=3$ through \(n=5\)$n=5$, including four at the proved \(n=3\)$n=3$ and \(n=4\)$n=4$ optima, but D-165 correctly remains recorded on those artifacts. Exp-021 adds one v3 \(n=3\)$n=3$ event whose 2,037 fixed-point evaluations are all retained and settled, whose pose independently verifies, and whose admissibility claim replays. Exp-022 completes the four-seed v3 block at 4/4 admissible: three endpoints reach side 2 and one reaches the valid nonoptimal side 2.362735797795. These events are evidence for the producer contract and terminal outcomes, not terminal-component counts. Exp-032 freezes the missing evidence rule: the complete exact \(n = 3\)$n=3$ quotient is one interval across four geometric keys and two contact signatures, and the complete exact \(n = 4\)$n=4$ quotient is one point. All current f64 events remain unresolved because none carries an exact component-membership witness. Exp-033 adds the first exact relation between sampled \(n = 5\)$n=5$ source poses: after one D4 action and relabelling, two different golden keys share a one-dimensional fixed-angle optimal face at side \(1 + 5\sqrt{2}/4\)$1+5\sqrt{2}/4$. It does not assign a full terminal component. Exp-034 embeds that face in an exact two-parameter angle-and-slide sheet. Exp-035 then retains six exact active-system matrices across A, the interior, and B and verifies a non-sheet direction against every row. Exp-036 proves that displayed direction cannot be a nonlinear path tangent: the only two nearby pair \((3,4)\)$(3,4)$ owner-axis branches have exact second-order obstruction margins. Exp-038 then certifies the complete first-order inventory and both pointed-quotient face vectors. This strict linearized-versus-true-tangent gap and finite inventory do not classify transverse or mixed nonlinear realization or assign a component. Exp-039 exactly continues four release classes through twelve sharp fixed-angle paths in one connected five-dimensional cell-local LP-optimal position polytope. Both owner branches carry positive structurally derived first-order stresses on those paths. This does not make every point of the polytope stationary, certify an A-to-B stationary path, classify R4, R5, -W, or mixed-angle directions, or assign a terminal component. Exp-023 reaches proved side 2 on three of four n=4 starts and preserves the fourth event’s post-check rejection. That stop exposed D-171: two rows were already outside the screen before an argmax-only retry. Exp-024 applies one complete offending-set retry and reaches side 2 on all four starts, with 14,301 of 14,301 evaluations settled and all four events admissible. Exp-025 extends the unchanged event path to \(n=5\)$n=5$: all four starts independently replay, all 14,219 fixed-point evaluations settle, and the run observes three descriptors at two nonoptimal side values. Those descriptors are not component identities, and none of the four starts finds the proved optimum. Exp-026 then finds the next retention boundary: three \(n=6\)$n=6$ events reach side 3 and replay, but seed 3 fails independent validity and is censored when event validation raises before writing it. D-183 now routes independently invalid endpoints through the same atomic retention path as every other terminal outcome. Exp-027 retains all four starts: three admissible side-3 events and one independently valid, non-admissible time-budget stop at side 3.040392660291. The earlier invalid endpoint does not reproduce because open D-126 makes wall-clock-limited work load-dependent; neither round supports frequency or component claims. Exp-028 retains four independently valid \(n=7\)$n=7$ outcomes but only one converges; three carry typed time-budget stops. This validates the event path at \(n=7\)$n=7$ while showing that the ten-second cell is already too censored for landscape statistics. Exp-029 retains four independently valid \(n=8\)$n=8$ outcomes: one admissible side-3 event, one typed unsettled cell-cycle stop, and two typed time-budget stops. Its bounded cost audit measures median four-event independent screening at 0.000684 seconds and canonical key computation at 0.004956 seconds, versus 38.004 seconds of retained quench wall. Canonicalization is therefore not yet the event-loop bottleneck at n=8, while the 3/4 typed-stop rate again bars landscape statistics. Exp-030 retains one independently valid \(n=9\)$n=9$ time-budget stop and completes the frozen command in 21.36 seconds, below its 30-second profile trigger. Median one-event keying costs 0.001074 seconds versus 20.062 seconds of quench wall, so canonicalization remains negligible at n=9. This one censored event is a performance control, not an n=9 landscape sample. The blind random-start size ladder stops after n=9. A source-bound n=10 entry point now reconstructs the published Göbel pose from the retained fixture, records its source URL, replays deterministic perturbations, and retains typed failure. A one-second smoke run reaches a valid endpoint at the proved side but times out before producer convergence. Exp-031 then converges on all four preregistered perturbations: every endpoint validates and replays, all 6,631 fixed-point evaluations settle, and the maximum proved-side error is \(2.221 \times 10^{-15}\)$2.221\times {10}^{-15}$. This is a local known-answer control, not a random-search or component claim. The exact small-moduli controls remain valid; component identity is the next blocked layer. The \(n=12\)$n=12$ calibration returns exactly \(4.0\)$4.0$, but that is not a known-answer guard. The runner’s full-pose independent verification boundary is repaired but not closed under D-044: a scored line must carry the pose, record re-checks the archived geometry in a separate process before writing a round, and an independent review on 2026-09-03 reproduced every refusal. That review returned BOUNDED-CAVEAT, and the record now names why — the float screen still demands an exact zero overlap where the source finding asked for an independently bounded one, and record never binds the lines it scores to the bytes the child verified. A producer-reported overlap scalar still does not close it.

Trump’s exact pose is locally isolated. Exp-013 retains all 512 raw active-feature selections as 128 derivative-distinct matrices. Every matrix has exact rank 33 and a strictly positive exact \(Q(u)\)$Q(u)$ stress, so every branchwise fixed-side linearized cone is zero. A finite-branch subsequence argument upgrades that result to local isolation and strict local side optimality in the anchored pose–side chart, modulo finite symmetries. It does not prove global optimality or give an explicit isolation radius.

Goebel’s \(n = 5\)$n=5$ optimum is locally rigid at fixed side, and that is a first-party result. Exp-058 registers the BC-152 proof packet: an intrinsic half-angle chart injective on all of \(R^{15}\)$R^{15}$, all 400 elementary wall-corner and pair inequalities classified by exact sign (confirming the agenda’s 16/64 and 4/6 counts with no discrepancy), a neighbourhood cut out by 128 strict sign conditions on which the local feasible system is exactly the twenty active rows, T-012’s 28 Farkas certificates and self-stress replaying on the chart with w · q_chart = -2√2 < 0, and an order-2m coefficient induction that contradicts a nonconstant analytic feasible arc. H-060 is confirmed on BC-153’s independent review, which returned PASS on 2026-09-03 against a criterion frozen before the target work and met as written: the reviewer replayed the instrument from clean roots under both interpreters and got this chart’s neighbourhood back exactly, and rebuilt every exact quantity from scratch in code sharing nothing with the author before accepting each step from nonisolation to the second-order contradiction. What is established, exactly: for \(s = 2 + \sqrt{2}/2\)$s=2+\sqrt{2}/2$ and Goebel’s labeled pose \(P^0\)$P^0$ in \(C = (\mathbb{R}^2 \times S^1)^5\)$C=({ℝ}^2\times S^1{)}^5$, \(P^0\)$P^0$ is an isolated point of Feas(s), so no nonconstant continuous feasible path leaves it and no sequence of distinct feasible poses converges to it — hence rigid at fixed side in the catalogue’s sense. Registered as T-014 at V3/C5, apparently-novel at S3: the exact quantities are machine-confirmed here, the curve-selection lemma and the induction that close the argument are an audited proof, and no instrument decides isolation — isolation_decided is false unconditionally, by design. Not claimed: an isolation radius, the side as a variable (false, X-007), global uniqueness, any other \(n = 5\)$n=5$ optimum, applicability of Connelly–Whiteley as stated, or novelty of method. Exp-034’s two-parameter feasible family is not a counterexample: it lives at side \(1 + 5\sqrt{2}/4\)$1+5\sqrt{2}/4$, disjoint from the feasible set at Goebel’s side, and X-012 runs it as the C8 control on which the instrument must refuse a receipt. Six gaps stay named and none is a condition of the pass — the printed BCR page behind the curve-selection citation is still unread, and the review replaces it with a derivation from primary-text Basu–Pollack–Roy plus the one-variable Puiseux fact rather than closing it. The corroborating second-order-sufficiency proof in the packet reaches the same conclusion from weaker hypotheses and discharges nothing, because acceptance was preregistered on the curve-selection route.

The optimal configuration spaces at \(n = 3,4\)$n=3,4$ are now exact controls. Exp-014 proves that \(F_3(2)\)$F_3(2)$ is two labelled circles, its S3 quotient is one circle, and its \(D_4 \times S_3\)$D_4\times S_3$ quotient is an interval whose corner endpoint changes the active signature and whose midpoint only changes the stabilizer. Exp-015 proves that \(F_4(2)\)$F_4(2)$ is 24 isolated labelled grids and both declared quotients are one point. Arbitrary rotations add no side-2 configurations in either case. Generation plus complete replay costs 1.28 wall seconds, so both controls belong in every gate. H-032 remains open at \(n = 5,6\)$n=5,6$.

The published \(n = 11\)$n=11$ lower-bound proof is false as printed. Exp-016 exactly certifies an open box of side \(10001/10000\)$10001/10000$ that fits Stromquist’s claimed container and strictly avoids all twelve printed Figure 14 points. This rejects the registered five-node H-010 conjunction but not the numerical lower bound itself.

The numerical lower bound now has an independent exact certificate. Exp-017 moves only Figure 14 point G.x from .8 to .79 and exactly certifies the complete five-node argument. Its 18-cell Figure 13 cover plus four Klein-four-related exceptions, 26-face repaired Figure 14 tiling, exact lemma premises, and \(3+9\)$3+9$ count prove \(s(11) \ge 2 + 4/\sqrt{5}\)$s(11)\ge 2+4/\sqrt{5}$. This source-distinct computer-assisted result is not attributed to Stromquist, is not externally peer-reviewed, and does not close the gap to Trump.

The tested class-bracketing refiner separates the proved controls from the target. It takes the tested \(n = 5\)$n=5$ and \(n = 10\)$n=10$ starts to \(10^{-15}\)${10}^{-15}$ and leaves the tested \(n = 11\)$n=11$ starts at \(6 \times 10^{-2}\)$6\times {10}^{-2}$. That makes proposer quality the next empirical bottleneck; it does not certify general local optimality or finish the quench contract (D-052).

The \(n = 11\)$n=11$ failure is consistent with an exploration problem. Five annealer seeds land in a band five times narrower than the remaining gap and the local quench improves those tested starts by only 1.3×. Starting near Trump’s reference, the default schedule moves far away; that is refinement evidence, not a certified basin-membership test.

Two rounds have been re-read by later ones. exp-005’s finite-quench residual is now scoped to the tested refiner and no longer called component attraction (D-083). exp-003’s \(n = 11\)$n=11$ result is therefore a combined proposer/refinement observation, not a pure basin-finding diagnosis.

Known defects in the record

The full log is defects.md; these are the ones that bear on reading the table above.

• exp-001’s archive carries no configurations and its engine commit was orphaned by a rebase (D-006, D-010). Cite exp-002–exp-004 for anything configuration-level.
• exp-001 and exp-006 each record a three-cell sweep as one cell (D-010, D-017—the second a verbatim repeat of the first, because the first fix left no regression check). Their numbers stand; the ledger’s sweep coverage misreported them until the successor rounds split the cells.
• D-021 is contained. Floating-point LP refinement has a noise floor of about \(10^{-11}\)${10}^{-11}$ in the side, and eight rounds sit on it. Those numerical results may not claim a difference smaller than the floor.
• D-403 is contained. The negative controls run only in the full gate, and a pull request runs --fast, so a branch can be green on every push while its controls rot — six of a hundred and fifty were not firing when this was checked. A control that does not fire is worse than an absent one, because the suite reports a count that reads as coverage. The runner is what saves it: an unmatched anchor is reported rather than skipped, and “failed, but not with the expected message” is distinguished from a real firing. Moving the suite onto the pull-request surface would push that surface past the point where it gets run at all, so what is owed is a cheap anchor-resolution check in --records rather than a faster suite.
• D-405 and D-406 are the reassessment auditing itself. BC-088’s entry sequenced X-009 on an unmeasured gap claim — the measured spread is \(0.056\)$0.056$–0.536, structured by \(k = m^2 - n\)$k=m^2-n$, and devtools/gap_ranking.py now carries it — and BC-092 was stopped on an enumeration price quoted without its artifact and against that artifact’s own isomorph-free decision at \(n = 5\)$n=5$. X-010 carries the corrected sequencing input; the repricing is open on the x-010 beads.

The Defect Record

Kept with the same discipline as the experiment record, because the aggregate says things no individual bug report can. The log contains 519 defects, one line each, generated from defects.yaml and checked in the gate.

One entry is filed under a class it only half fits, and the table reads accordingly. D-484 carries two defects with a single cause: an escape screen that finished only when the runner was kind, which is robustness, and a behavioural lane that completed but cost 1020.77 s where 718.52 s was available, which is performance in D-456’s sense. It is filed as robustness, for the half that took main red, so the performance row here reads one low. The entry names that call rather than leaving it implicit; the alternative was two ids sharing every other field.

D-502 remains open: the implicit local pre-push allocation left a costly partial reachable-test selection serial until its 900-second command cap. A ten-worker retry completed below that cap under a different PACK_JOBS shape, so it is an observed workaround rather than a controlled speedup or validation of the proposed cost-aware allocation. That allocation remains unimplemented and needs measurement.

Two observations the log exists to make.

84 of the 108 soundness defects pointed in the flattering direction, where the error looks like a success. That is the dangerous class, and it is the majority of it.

The automated gate has caught eighty-two defects in 519, and no soundness defect ever. Every soundness failure was found by a control cell whose answer was known in advance, a rule written down before the measurement, a generated view contradicting its source, or someone reading carefully. Gates confirm what you already thought to check; these were found by devices built to be surprised. Gate-detected entries here are mechanical process, implementation, or test-validity failures, found by contiguity, integration, mutation-anchor, reconciliation, or known-answer checks. The supported distinction is that the gate has never caught the mathematics being wrong.

D-490 is contained, and it is the log’s cleanest case of a detector that fired correctly and said nothing usable. The Pages job draws the explainer to a PDF twice and requires the two to agree; on 2026-09-10 they did not, by two bytes out of 786119, and the failure line carried those two lengths and nothing else — no object, no offset, no kind, and both renders discarded. It also asserted a cause: that something the page draws was unfinished when it was captured. A control on one container changed the PDF by 211351 bytes when the print faces were omitted, while forty complete renders on that host agreed. That makes the measured missing-face state a poor match for the observed two-byte delta on that host; it does not identify the runner’s cause or rule out another readiness failure. The cause stays open under think-ptit; the next occurrence will name the object or outside-object PDF section containing the first difference.

D-509 is open, and it is D-490 again, past the containment D-490 built: PR 235’s pdf job failed on a records-only commit with two equal-length draws differing inside one untyped deflate stream where the page content streams sit. Locally, five of 104 page loads placed one prepared-math glyph a fifth of a pixel off the others’ placement and then printed that placement identically, four prints running, so drawing each load twice cannot see it. It is contained on both sides. --update publishes only a document two of up to three page loads drew, and refuses when no two agree. When the first fresh load does not reproduce the stored PDF, --check-artifact draws up to four loads and passes only if one does and the rest drew a single other document. A refusal names the moved Tm line. At the local rate that leaves about one run in 110 refused, against one in eleven before, and the cause stays open under think-6dle.

D-489 is open, and it is the log’s clearest case of a guard that reads like soundness and acts like a filter. devtools/screen_corner_dual_salvage.py screens a retained depth-one family against an owner class’s guaranteed patch and reads the survivor weight as a weak-duality lower bound on that class’s residual cover value. Its source predicate requires the source receipt’s failures to be exactly ["K3 total weight at least n"] — the failure a family records when its total weight is below \(n\)$n$ — so it accepts only a family that falls short of the mass the bound is made of, and refuses every proved ceiling family. Exp137 and exp138 deliberately named a source family about \(0.6158\)$0.6158$ short of eleven; exp141 independently confirmed their exact negative results on that source. Those results remain valid. They do not establish that no other fractional family obstructs the residual problem, or that a useful conditional cover exists. The later X1 screen uses a different mass-eleven family and leaves exact survivor mass ten on four screened single-corner endpoint-patch relaxations. Its depth-one survivors obstruct a point cover below ten on those particular domains.

The source guard is still a reuse defect: it must be repaired before admitting a valid mass-eleven source through that CLI, as tracked by think-rm5c. That defect and the change of source do not reverse exp137/138’s scoped arithmetic. The corrected X-026 separates measured neutrality for the endpoint-patch family from the open questions of physical owner routing, stronger domains and conditional threshold covers. Neither a universal conditional-method refutation nor equal reach or runtime follows.

D-470 records a deferred exhaustive test that still asserted the rung T-021 displaced. The full gate caught the stale transcription after the PR 83 merge; the test now re-derives its values from the moving certificate pointer. The optional pre-merge deep gate now exercises the deferred surface; the post-merge exhaustive tier remains the backstop when that gate is not requested.

D-471 records three further conflicted-branch CI blackouts. A branch whose merge ref GitHub cannot synthesize receives no pull-request workflow run. The push-triggered git merge-tree guard now detects that state after every branch push; an idle branch can still become conflicted when main moves underneath it.

D-478 records a missing witness for BC-206’s reported cutting floor. The value near \(10.845594\)$10.845594$ at side \(3.97\)$3.97$ survives only in a text log. Its generating family is unavailable for replay after the cutting-screen repairs, so it is qualified as an unreplayed historical report. think-aenh owns recovery or recomputation with a retained exact witness.

The generated log currently has 68 open entries: 41 outstanding and 27 contained. The W9 candidate think-cyko owns their systematic risk ordering and bounded repair waves; the synopsis names the cases that matter to current claims rather than pretending the examples below are the whole backlog. D-406 waits on the enumeration repricing X-010 filed. One older entry is worth naming because refusing was the whole of the available fix: D-391 is the first-order rigidity assessor intersecting a tangent cone that is a union: two squares meeting at a single corner are held apart by two axes, and non-overlap asks that either keep separating, so the linearized feasible set is a union of half-spaces and not a polyhedron. Intersecting them is a subset of every branch, so a pose reads as more rigid than it is. \(n = 5\)$n=5$, the only size this instrument had produced a retained claim about, has no such pair; Göbel’s \(n = 40\)$n=40$ has 42 of its 98 touching pairs, and there the error inverts the answer rather than merely weakening it. That pose has an infinitesimal motion — all sixteen squares of its tilted block turning together, each about its own centre — which gives up one separating axis at 24 of the 42 corner contacts and keeps the other, which is all non-overlap asks. An assessor that intersects reads those given-up rows as violations and certifies every one of the 120 coordinates as pinned, reporting a packing rigid that is not. Removing the defect is what found the witness. It is still not a motion: the gaps curve shut at order \(t^2\)$t^2$, so \(n = 40\)$n=40$’s record stays undetermined and the catalogue’s annotation stands.

Four agenda-015 review findings are also open. D-418 records eight declared parser or recursion bounds without the named exceeding controls BC-140 required. D-419 stops exp-057 because two six-decimal coordinate rules were applied to a fourteen-digit release-text side token without source provenance. D-420 keeps BC-142 partial because its benchmark selection test proves a bounded inclusion and refusal, not exact reachable-set equivalence. D-421 records that the wave-efficiency renderer accepts Codex receipts but not the Claude receipts retained by this bridged wave, so BC-143 keeps a typed no-change/refusal instead of hand-computing incomparable telemetry. D-422 began as the snapshot cap refusing all 155 negative controls before one of them ran, and that half is discharged: pruning four large result files at a478744a took the counted surface from 90,031,065 to 56,219,144 bytes, and the suite then ran three times on this branch with all 155 controls firing as expected — the first direct evidence here that the controls catch what they were written for rather than only that their anchors resolve. What stays open is the diagnosis that replaced it, and the entry is retitled to it: the portable fallback still copies untracked build caches into every worker, and the cap is held by a per-file prune that was never meant to be durable. The cap itself is checked on the pull-request surface; the cache accounting is checked by nothing. D-434 is the one an overnight run should know about: the covering program’s separation oracle scores a placement cell by its centre, while the exact sweep that decides the certificate scores every cell whose slab meets the admissible domain — 1.1 to 1.2 per cent more cells away from the axes. The search therefore optimises against a weaker constraint set than the verifier enforces, and two \(n = 12\)$n=12$ pushes to side \(39/10\)$39/10$ converged below twelve and were then refused on placements they were never shown. The gap is one-sided, so every accepted certificate stands and T-017 is untouched; what it costs is candidates. Hosted CI is now red on that same assertion: the planning branch’s pull-request surface failed it at 67,173,741 bytes on 2026-09-04 and main’s post-merge run at 9d5eae0f fails the same step, so the repair scheduled as BC-168 is what turns the hosted gate green as well. D-423 records that the lemma closing the Green17 cover certificate’s top strips is printed non-strict in Stromquist 2003 and Bentz 2010 and strict in Friedman’s DS7, and that the repository holds all three. The readings agree everywhere except on the boundary the certificate uses, so the boundary case is an unrecorded source obligation rather than a settled step.

The W9 remediation lane leaves three open entries of its own, and the reason they are open is the more useful part. D-044 and D-046 were marked fixed at 08:25Z on 2026-09-03; the independent review that was meant to gate that disposition began at 08:46Z and returned BOUNDED-CAVEAT for both, so both are now contained. Both repairs are real and were reproduced against the code rather than against the record: the producer-side attack D-044 names is closed, and all twelve of D-046’s clauses are closed, including the seven guards that turn the suite red only when reverted in a copy. What holds them back is that both records summarise findings from the PR #14 review, the repairs were written against the summaries, and four clauses of the source findings never reached the summaries — the float screen’s exact-zero overlap, pre-run engine dirtiness, per-cell timebox semantics, and reporting runnable-but-unrun work. All four are conservative; none flatters a result; none is repaired. Three undisclosed residuals sit on the same archive boundary and close together with one receipt written by execute and compared by record. D-426 is the finding that review turned up on D-046’s own edge: a control-cell breach is a declared stop condition that the session does not honour, because run resets its failure count on the breached round and continues on the same suspect instrument. Nothing has been recorded through any of this — no live round has run, nothing has been recorded through the unattended runner, and the numerical runner stays NO-GO. An earlier form of that sentence gave the reason as the search engine not being built here; a release binary was built at packing/sqsearch/target/release/sqsearch at 10:30Z on 2026-09-03, nothing has been executed against it, and the conclusion rests on the absence of a recorded round rather than on the absence of a binary.

D-427 came out of the same day’s work on the control harness and is the weakest in degree of the three, and the broadest in reach. run_one scores a control on its mutated run alone — non-zero exit plus the expected string — and never requires the unmutated checker to have been green, so a control can report a pass over a checker that was already failing for an unrelated reason. It was demonstrated rather than argued: delete one archived fixture from a worker clone, and check_canonical turns red before any mutation while all four of its controls still score a pass with empty detail. D-413 is the same mechanism having already happened once; its fix pinned a green baseline for one of the forty distinct control commands, and the general form stayed open.

D-428 is a record claiming a check that is not there. The \(n = 17\)$n=17$ successor’s validate_result rebuilds all 181 hash-chain links from the two certificate summaries and compares them with the emitted spine, but never compares that rebuild with the carried boundary it is supposed to terminate on, so a carried row altered identically in both summaries — with the spine and last row hash recomputed around it — is accepted. The round record asserted the stronger claim, that an altered manifest cannot survive; that holds for the executed admission boundary, which ties the retained prefix to exp-056 on disk before assembly, and not for the validator alone. The published result satisfies the tie and the record has been corrected; the code has not.

D-429 is a guard that would have fought the formatter forever, recorded before it ever fired. Generated blocks inside formatted documents are compared by what a line says rather than by its bytes, so flowmark may own the typography inside them; the fold that makes that comparison work maps … back to ... but not the space flowmark inserts before it. No generated cell has carried an ellipsis until the results headline, whose \(n = 17\)$n=17$ row does, so the failure has never happened — a render and the formatter would have rewritten each other on every commit, which is the churn .flowmarkignore exists to stop, reappearing inside a block the formatter is allowed to touch. The headline works around it locally and the shared fix is deliberately unapplied: a one-line change to a comparison guard backing several views, made unreviewed at the end of an unattended session, is the shape of D-425.

Two entries were added while planning Agenda 017, both found by re-running what the record already said. D-430 is the frontier prose saying sixty-three open cases rest on Nagamochi’s closed form a day after the 4.5058 adoption made it sixty; the README and sixty-seven case bodies were corrected, and check_nagamochi_bounds refuses any prose count that disagrees with the case records — which is why the same sixty-seven bodies now read fifty-eight, T-020 having taken two more cases off the closed form. D-449 was the exact sweep reporting, beside the least covered mass, a witness centre at the midpoint of the attaining event cell, which on most directions lies outside the admissible domain; the value was right and the point was not a witness. The witness is now a point of the cell’s intersection with the domain on both routes, held there on every direction of every retained certificate. D-431 is open: T-009’s significance rationale compares its \(n = 29\)$n=29$ interval certificate against a rational certificate on Schadt’s packing rather than Kingbird’s, and the shipped rational promotion run on the Kingbird witness lands about \(5.4 \times 10^{-20}\)$5.4\times {10}^{-20}$ below the interval bound, the opposite of what the rationale says. Agenda 017’s BC-165 registers that certificate, rewrites the comparison on one packing, and takes T-009 to C4 through the results checker. D-432 was found by the same branch’s own pre-push tier: when the change set touches a file that configures the suite, the tier falls back to the whole suite under a 900-second cap the full-suite steps no longer use, dies at 84%, and names no failing test; the step now takes the fast suite’s own budget when its selector expands to the whole suite, the first commit of the branch that ports PR #80’s findings.

D-393 is the same run being wrong about its own gate. D-381 established --edit as the pre-push floor, and that floor does not run tests: the test step is marked broad, and dropping broad steps is exactly what --edit does. So four pushes went out on a red branch — a stale pin, an undeclared marker, and D-392, a size cutoff meant for generated blobs that went blind when defects.yaml grew past half a megabyte. The wake events naming the failed check were delivered six times and read once, after the fact. The tiers are right; using one of them as though it were the other was not.

D-398 is the record being behind its own toolchain rather than wrong about it. \(n = 40\)$n=40$, \(n = 65\)$n=65$ and \(n = 89\)$n=89$ each declared a blocker of kind mathematics reading “No formal certificate currently supports the tighter reported upper bound”, and each kept its verified ceiling at the integer grid — \(7\)$7$, \(9\)$9$, \(10\)$10$. All three certificates existed and ran in the gate the whole time: 780 pairs decided by exact sign over \(Q(\sqrt{2})\)$Q(\sqrt{2})$ at \(n = 40\)$n=40$, 2080 at \(n = 65\)$n=65$, 3916 at \(n = 89\)$n=89$. A feasible packing at side \(s\)$s$, decided exactly, is a proof that \(s(n) \le s\)$s(n)\le s$, so the mathematics the blocker called missing was done and what was missing was an evidence record naming it.

The promotion is made: all three now cite Göbel’s construction, and the count of cases whose verified ceiling exceeds their best known falls from 33 to 30. The direction was conservative — the register understated what it could certify — but the reason nothing caught it is worth more than the instance. Every check on a frontier record read that record against its own fields, so none could see a certificate it had never been told about. A sweep now runs the other way: each exact verifier declares the sizes it decides, and each of those must reach an evidence record citing that package — with an undeclared verifier a refusal rather than a skip, so a new one cannot opt out by staying silent.

The record can also be wrong about itself, and D-358 is this run being so: an unattended run declared blocks of 150, 180, 180 and 40 minutes and took 31, 42, 29 and 23, because it estimated elapsed time between tool calls instead of reading a clock. The bookkeeping was the smaller half. The misreading also supplied a reason for stopping early -- that later blocks had overrun into the slack -- when nothing had overrun and most of the budget was unspent, which is a constraint the run claimed to meet and in fact a mistake it made.

It said “None automatic” under regression, and a day later it happened again (D-386): a session declared two phases starting an hour and a half after the clock read. A practice change without a check is not a fix, which is the same lesson D-010 and D-017 record one level down. The gate now refuses a session that declares a start time later than the moment of checking, and prints elapsed against budget derived from the record’s own successive timestamps — the line that would have made this visible while it was happening.

The harness that proves those checks fire has a blind spot of its own. D-356 records that run_negative_controls prunes the literature archive and the atlas renderings from its snapshot to stay under a portable size cap, so any check reading one of them fails there on a missing file rather than on the mutation. Three controls written for the \(n = 29\)$n=29$ chain were withdrawn for that reason, and the guards they would have exercised are asserted directly in their test instead. D-357 is the companion, and it is a correction: a synopsis control that failed four times running, including against a clean tree, later fired correctly with nothing changed, so the standing-failure reading recorded first was wrong and the entry now says plainly that the trigger is not identified.

A check can also pass for a reason other than the one it states, and this log now has two of those a day apart. D-359 recorded that the generated atlas SVG’s coordinate precision was inherited rather than pinned: format_svg_number rendered a scalar at whatever precision it was last refined to, so known-best-1-100.svg carried 27 fractional digits in a fresh process and 50 once anything had refined the shared field. The test asserting that the stored PNG was rendered from the current SVG therefore passed on test ordering, and a genuinely stale PNG would have been indistinguishable from the passing case. It is now fixed, and the feared regeneration did not happen: the ambient state came from NumberField.decimal setting the thread-global decimal precision and never restoring it, and the emission is pinned at 28 — the precision every retained figure was already drawn at — so no stored artifact changed a byte.

Fixing it surfaced the second. D-362 is open: validate_translation_only_trajectory compares two independently rounded projections of exact algebraic numbers for exact equality, and they agree to about thirty-one digits rather than exactly. It has never fired wrongly only because nothing had raised the ambient precision before it ran, which is the same accident D-359 was. It is left open deliberately: it is what stands between this repository and a principled emission precision of 32, and that is a decision about what the projection layer promises rather than a rounding to choose in passing.

A control that does not reach its known answer is the third of these, and it took the first full strict run in a while to see it. D-365 records that check_golden_basins --deep fails three oracles at \(n = 10\)$n=10$: the quench reaches \(3.735634792931\)$3.735634792931$ and refuses to certify convergence, and anneal-plus-quench lands \(2.85 \times 10^{-2}\)$2.85\times {10}^{-2}$ above the proved \(s(10) = (6 + \sqrt{2})/2\)$s(10)=(6+\sqrt{2})/2$. Nothing downstream reads the failing value, so no result rests on it; what is lost is the control itself, at the one size in the ladder where the answer is proved and the packing is not trivially a grid. It is proven pre-existing rather than assumed — the identical failures reproduce at the base commit of the session that found them, in a separate worktree — and it runs only in the strict tier, which is why a continuation running the fast gate at every checkpoint never met it.

The gate’s cost is itself a logged defect, and this session added a second one. D-366 records that the negative-control step now outgrows the 900-second per-step timeout: nothing is wrong with the controls — run without the cap the suite completes in 1268s and all 137 fire — but a step that always times out stops distinguishing a control that no longer fires from a machine that was busy. D-355 records that verification runs the whole gate after every change, so cycle time is set by the slowest full-tier step rather than by what the change can reach: a two-file edit measured at 979.79s against the 12.06s its two affected steps need, an 82x overrun. The resolution is not to check less. The efficiency principle asks for iteration as fast as possible and the standing asymmetry lets efficiency simplify process but never weaken assurance, so what is owed is a change-scoped selector that is conservative by construction and can be caught under-selecting — think-9qtn, under BC-084, which carries BC-051’s scope unchanged. Good coverage and short cycles are a design tension, and resolving it is the design’s job rather than the operator’s discretion.

A control can also be wrong by being unable to fail. D-378 records that the declared surviving identity relation, contact + closure, has exactly one distinguishing verdict — agrees on the \(n = 3\)$n=3$ quotient control — and that this verdict cannot test it. The record carries one closure set, closure(G) = [C, G, M], and it covers every stratum that control has, so any faithful implementation returns one there whatever the certificates say; mutating all four samples to distinct certificates, then to a single shared one, leaves the answer at one. That is D-373’s finding one level down: there the problem was that every control’s answer is one, here it is that the closure is degenerate, so even a control whose answer were not one would not separate the relation from a merge-everything one unless it carried two disjoint closure classes. None does. It is contained rather than fixed — the relation now reads both halves of its own definition, and a synthetic two-class control exercises the half no retained control reaches — because a real fix needs a new exact classification.

A record contract can also be wrong by being unable to say something true. D-377 records that a delegation which is read-only by construction cannot be written down while it runs: packing-ledger check requires an in_progress delegation to declare a write_scope, and the schema requires that scope to be non-empty. Investigation, review, and audit are exactly the delegations OR-2 says parallelise best, and all three write nothing. It is contained rather than fixed — such delegations are recorded on completion instead — because the repair is a decision about the session contract, and an explicit read_only flag is better than permitting an empty list that would be ambiguous between “writes nothing” and “nobody filled this in”.

121 fixes left no regression check behind. D-300 remains open: the yielded session id, output, timeout/final poll, and exit survived, but invalid gdate precision left the start and end fields empty, so D-202, D-217, and think-b3bm remain open. D-304 records a contradictory inequality in McClenagan’s printed Section 3 proof. H-037 repairs that local sign step independently from both the figures and the source equations; it does not certify the remaining construction. D-343 records Bui’s printed unbounded replacement instruction. H-037 keeps the source-forced finite range and replays the resulting exact square count; the geometric construction and its asymptotic theorem remain open. D-344, D-345, D-346, and D-347 record four independent gaps in El Moumni’s printed \(n = 7\)$n=7$ proof. The source-distinct Case 1 branch repair and Figure 4 coordinate prerequisite are exact, but the printed length remains defective, the cross-section names o1 where its premises require o4, and the diameter display uses undefined \(i\)$i$ with only a separately tagged midpoint candidate. No surrounding incidence is verified, so the complete source-faithful replay stays blocked under think-trkj.

The entries from D-030 onward sharpen the point rather than softening it. D-283 remains open in the current robustness inventory. D-030 and D-031 were caught by proved control cells while structural store checks stayed green; D-032 and D-033 came from rehearsing recovery paths that had shipped unrun; D-034 found the endpoint-isolation assumption; D-035 found destructive negative-control residue; D-036 found a timeout reported as convergence; and D-037 separated real census counts from a checker’s synthetic re-offers. D-038 separated scalar recognition from an oracle; D-039 separated side precision from component resolution; D-040 made rarity conditional on a durable P/Q/E regime; D-041 rejected rank-free rigidity and dimension claims; and D-042 exposed \(n = 12\)$n=12$ as an open target masquerading as a negative control.

The systematic crosswalk then records every remaining technical finding from the PR #14 review. D-043 closes the archive-before-validation path; D-044 and D-046 repair independent pose validity and the runner state machine and stay contained on the residuals their independent review named; D-045 tracks criterion-specific evaluators; D-047 closes contact-key reflection; D-048 retains unstable tolerance/equality semantics; D-049 tracks factorial canonicalization; D-050 and D-051 separate observation promotion from regime-safe merging; D-052 narrows quench stationarity; D-053 now enforces the generic exact-field preconditions; D-054 separates budgets and final-best records from trajectory claims; D-055 and D-056 correct the angle and \(m^2-3\)$m^2-3$ theorems; D-057 scopes H-020; D-058 reconciles the local handover; D-059 keeps the golden oracle/characterization split open; D-060 restores producer-level strict checks; and D-061 preserves evidence for unrecognised endpoints. D-062 catches the executable \(n=12\)$n=12$ rejection that survived the first D-042 correction; D-063 removes a false contrapositive from the rigidity premise; and D-064 keeps a read-only runner preflight executable inside the gate that mutation-tests it without opening the gate to live campaign execution. D-065 removes the last repeated numeric gate claim from the README and reconciles its remaining qualitative claim to the defect source.

D-066 catches the active baseline script repeating the stale \(n=12\)$n=12$ control claim. D-067 and D-068 restore the omitted eleventh-round wall time and stop calling elapsed time CPU time; D-069 reconciles H-002 with the four rounds that already measured its quench; and D-070 restores exp-011’s execution revision and makes future timing and provenance survive the execute/record boundary. D-071 remains open because the numerical runner’s generated session report still overwrites its predecessor; versioned agent-session artifacts now preserve the outer delegation loop separately. D-072 closes the two direct runner commands that bypassed the cooperative gate marker, and D-073 wires those new session artifacts into the filename/id invariant. D-074 corrects the first D-070 regression claim: receipt parsing alone did not exercise the terminal artifact mapping, which is now centralized and mutation-tested. D-075 narrows PR #16’s cross-environment mismatch to what its aggregate output actually establishes; D-076 keeps the \(n=5\)$n=5$ six-of-six observation from deciding among identity, landscape, stationarity, and numerical explanations; D-077 replaces a stale serial handoff with current parallel lanes; and D-078/D-079 complete the rank and implication corrections in that response. D-080 replaces a vacuous neighbor-transfer target; D-081 keeps a nonempty but underfilled queue from counting as overnight readiness; D-082 records the second overgeneralization of H-020; D-083 retracts an attraction claim inferred from a finite- quench residual; D-084 removes unsupported rigidity and gap-rank facts from the \(n=11\)$n=11$ frontier artifact; D-085 freezes living uv commands; and D-086 replaces stale overnight and handoff state with the current launch agenda. D-087 separates the angle-class algorithm, corpus law, and single-cell kink claims. D-088 through D-105 are source, geometry, identity, and hypothesis-design corrections from the first creativity pass; D-106 and D-107 are the mutation-anchor and synopsis reconciliation failures its first gate attempts caught. D-108 through D-119 are the second-pass corrections: the missing piercing paper, false isostatic and self-stress arguments, fixed-budget and fixed-cell overreach, topology and fractional-LP mistakes, unsupported novelty, stale registry state, the H-012/H-017 estimand conflation, and an impossible continuity-blind angle-sheet criterion. D-120 through D-138 record the engineering delta and first post-merge runs: ulp-sensitive cell selection, gate boundary and skip-contract failures, the per-step worker cap, bounded portable snapshots, a parallel negative-control race, wall-clock scientific budgeting, stale review status, the missing targeted edit loop, unbounded checker children, and a nonunique mutation-control anchor, followed by a lint floor that accepted type-checker warnings and a fixed-cell solver that does not expose whether it settled or hit its cap (D-132), then the search-only determination vocabulary that could not represent H-024’s missing formal prerequisite, the omitted \(n=29\)$n=29$ source provenance that the falsifier exposed, the roll-up’s obsolete blanket claim about exploratory record evidence, the distinction between a branch linearization and a true Bouligand motion, and a certificate replay that did not require one-to-one branch coverage. The next tranche, D-139 through D-171, records the missing hard-square topology literature, a stale closed-family contact claim, exact-moduli integration errors, Stromquist source transcription and proof-chain mistakes, stale campaign effort, the paper’s extraneous Lemma 4 root, and the escaping Figure 14 box. D-153 records that the three 1984 memoranda were directly hosted while the source ledger called them unavailable; D-154 and D-155 close exact-field metadata and cross-platform record gaps in the first uncommitted H-010 checker. D-156 through D-158 close tiling-containment, sign-preservation, and provenance-scope gaps in the H-041 repair checker before any H-041 evidence could land. D-159 keeps immutable scanned PDFs out of Git’s text-whitespace path while preserving strict whitespace checks for the associated hand-written reading aids. D-160 records a D-145 recurrence caught in this round’s own diff: a broad scalar match attached H-010’s regression text to D-002 before an ID-scoped correction restored both. D-161 records the stale forty-hypothesis synopsis count exposed when H-041 became the forty-first artifact; the current consistency check now derives that count from the registry. D-162 records the first consequence exposed by typed fixed-cell termination: a deep rebuild reduces the converged totals at \(n=3\)$n=3$, \(n=4\)$n=4$, and \(n=5\)$n=5$, and exposes unsettled ladder evaluations at \(n=9\)$n=9$ and \(n=10\)$n=10$. Their full poses remain useful evidence, but the small-n convergence totals must be rebuilt before any such event can be promoted to a terminal component. D-163 records the gate failure that first hid that evidence: the historical-regression step continued after its checker failed and returned the status of a later successful probe. The step now propagates the checker failure immediately. D-164 separates one source of the newly visible nonconvergence: a successful HiGHS solve missed the fixed-cell post-check by about \(2 \times 10^{-11}\)$2\times {10}^{-11}$ beyond its cutoff and was labeled mathematically infeasible. Typed outcomes now retain the cause, rows, residuals, retry margins, and actual solver-call count. A single retry tightens the complete initial offending set, leaves the \(10^{-10}\)${10}^{-10}$ acceptance screen unchanged, restores the proved n=3 and n=10 controls, and is replayed against the original LP rows. D-165 records the bounded implementation’s stop condition: initial cell-solve failures still bypass D-132’s typed result and become dummy objectives inside the angle search. That code path is now typed, D-168 closes the n=10 cell degeneracy, and BasinEvent/v3 routes every fixed-point evaluation through one audited path. Exp-021 retains and replays a balanced 2,037-evaluation receipt, so D-165 is fixed; the older exp-018 through exp-020 artifacts remain correctly blocked under their historical v2 contract. D-166 removes the resulting false certificate from BasinEvent/v1. Version 2 retains the full stopping event and independent validity screen but marks every current event promotion-blocked by D-165, and replay refuses a forged admissible flag. D-167 adds the missing per-event wall time, so subsequent seed blocks and larger \(n\)$n$ values can be selected from measured throughput rather than command-level guesses. D-168 separates an equal-objective finite cell closure from a genuinely unresolved cycle. The n=10 control closes after enumerating at most eight adjacent cells; exp-021 then records the new typed path without rewriting the historical blocked events. D-169 fixes a second post-check hole found while typing those failures: containment rows were never replayed. Every accepted cell now passes the full original LP residual vector. D-170 gives D-165 its own bead after the defect log was found to reference the unrelated D-132 tracker; the older bead remains unchanged. D-171 records why the former argmax-only repair left one n=4 event unsettled: rows 16 and 21 already violated the screen together. The complete offending-set retry closes the exact regression, and exp-024 completes the n=4 v3 block at 4/4 admissible without weakening the screen. D-194 and D-195 record two pre-measurement corrections to exp-035: pair \((0,4)\)$(0,4)$ is regenerated at each slide stratum, and pair \((3,4)\)$(3,4)$ has two owner-axis branches whose tied support rows are conjunctive within each branch. The frozen controls now execute and both defects are fixed. D-196 records the integration recurrence caught before commit when a context-poor edit briefly changed D-034 instead of D-194. D-197 records the concurrent checkout caught by the exp-036 commit banner; the isolated checker commit was moved to the campaign branch and the other branch ref restored before push or target execution.

D-289 through D-293 record the H-043 pilot’s remaining validity, robustness, and provenance gaps. D-289 covers row-class normalization in the cone oracle; D-290 keeps certificate replay open; D-291 covers the branch-0 golden’s treatment of valid future refutations; D-292 keeps regenerated branch indices bound to the retained exp-013 universe; and D-293 keeps provenance self-tests from claiming completeness without exact mappings.

The generated defect view owns the aggregate counts; this narrative retains the causal history. The postmortem on D-014 turns this into four rules—oracle coverage through unshared code, tolerances stated relative to what they govern, a discovery treated as a defect until an independent layer agrees, and new components inheriting the perimeter—that apply to code not yet written.

Where This Stands

As of 2026-09-22 the current state and execution order are the checked Research Program Status and Roadmap above. The verified external bound is \(s(11) > 31/8 = 3.875\)$s(11)>31/8=3.875$; the first-party point and threshold families below remain historical method evidence, and their ceilings leave no route to that current bound by net refinement alone. The owner has selected material bound improvement or proof simplification as the governing payoff. The historical synthesis below explains how the program reached that boundary. Its weighted-resource lineage runs through Göbel, Kearney–Shiu, Nagamochi and Bentz; the recent pure-atomic rational direction-net architecture follows Burns, and the LP instance and parameter line follows Massaccesi. This project’s instances and generator moved seven registered cases in one day. \(s(11) \ge 381/100\)$s(11)\ge 381/100$ is T-018, improving Stromquist’s \(2 + 4/\sqrt{5}\)$2+4/\sqrt{5}$, stated in 1984 and published in 2003; the recorded search found no intervening improvement. T-022 proves a small exact refinement to \(3.810025723614703\ldots\)$3.810025723614703\dots$, and T-024 re-certifies the same atoms on a finer direction net and proves \(s(11) \ge 3.816609502788862\ldots\)$s(11)\ge 3.816609502788862\dots$; both use exact dilation-limit arguments. \(s(11) \ge 191/50\)$s(11)\ge 191/50$ is T-025, a certificate of a new kind: threshold atoms, which charge a core holding at least \(k\)$k$ of a set’s points and cost only \(\lfloor \lvert S\rvert/ k \rfloor\)$\lfloor \left|S\right|/k\rfloor$ of the budget, carry the side past the exact ceiling that the point-atom method provably cannot pass. T-026 then re-certifies those atoms on a 1440-step net and proves \(s(11) \ge 3.826447410572939\ldots\)$s(11)\ge 3.826447410572939\dots$ by an exact dilation-limit argument, and T-033 repeats that on a 2880-step net for \(s(11) \ge 3.826997548829543\ldots\)$s(11)\ge 3.826997548829543\dots$. T-033 is the strongest retained first-party rung in this family, while the current verified case bound is the stronger external strict result \(s(11) > 31/8\)$s(11)>31/8$. “Dilation-limit” describes T-033’s proof construction, not a weaker theorem or assurance level. The result retains its historical S5 registration; its current significance is S3 as method and calibration evidence, while the external certificate supplies the current case bound. \(s(12) \ge 99/25\)$s(12)\ge 99/25$ is T-017, proved about twelve squares rather than inherited from eleven, and reached independently of Evan Daniel’s stronger \(15680/3951\)$15680/3951$, which was in his repository from 25 August; that is now the case bound, replayed here on 2026-09-27 (n-012). \(s(17) \ge 459/100\)$s(17)\ge 459/100$, and \(n = 18\)$n=18$ and \(n = 19\)$n=19$ at the same side without a monotonicity step, is T-019 and displaces Massaccesi’s published \(4.5058\)$4.5058$ by \(0.0842\)$0.0842$. \(s(19)\)$s(19)$, \(s(20)\)$s(20)$ and \(s(21) \ge 24/5\)$s(21)\ge 24/5$ is T-020, which carries \(n = 19\)$n=19$ past T-019 the same evening and displaces Nagamochi’s 2005 closed form at the other two — \(1 + \sqrt{13}\)$1+\sqrt{13}$ and \(1 + \sqrt{14}\)$1+\sqrt{14}$ — by \(0.194449\)$0.194449$ and \(0.058343\)$0.058343$. Its \(0.21\)$0.21$ at \(n = 19\)$n=19$ is the largest single-case movement in the register, and twenty and twenty-one had never carried a proved bound of their own. Between them T-019 and T-020 are the only values in print this project has replaced. Evan Daniel has since proved \(s(21) = 5\)$s(21)=5$ (n-021). All four stand at V4: each was decided twice from frozen bytes by an exact event-cell sweep and by an interval branch and bound with directed rounding — two routes that share the certificate and the closed-form conditions but decide Condition 5 by different methods, which fail differently — agreeing on the least covered mass to the digit. Three of them stand at C4, and T-018 at C5 — the rung epistemics.md defines as review-ready, a mapped and non-superseded review artifact, which the adversarial review of PR 78 supplies. None of the four has been read by anyone outside the project, which that rung does not ask for; a self-contained package for third-party checking ships at packing/cases/n11_fractional_certificate/thirdparty/ so that a stranger can decide the \(19/5\)$19/5$ rung without trusting this repository.

That lane also has a measured edge, which is the more useful thing to carry. \(n = 11\)$n=11$ at \(3.82\)$3.82$ is closed to both pre-registered routes and the closure was checked rather than assumed. The covering LP was run on two independent site sets and both converged to an objective of exactly \(11.000000\)$11.000000$ from above, where a certificate needs mass strictly below eleven; the rejection route was then built and decided exactly, and its maximum pointwise depth of \(1925/1152\)$1925/1152$ caps the feasible total at \(1152/175 = 6.58\)$1152/175=6.58$ against the eleven a ceiling needs. Where the two routes fail by an infinitesimal at the same value, neither closes. That is a limit on the method’s reach at that side, recorded as measurement and not as a claim about \(\tau^{\ast}\)${\tau }^{*}$.

The method also has a ceiling that is structural rather than measured, and it forecloses one of the three cases outright. No certificate for \(n\)$n$ can exist at a container side above \(\lceil \sqrt{n} \rceil \cdot B\)$\lceil \sqrt{n}\rceil ·B$: a wider container holds \(\lceil \sqrt{n} \rceil^2\)$\lceil \sqrt{n}{\rceil }^2$ pairwise disjoint axis-parallel \(B\)$B$-squares, direction \(0\)$0$ is always in the net, so Condition 5 gives each of them mass at least \(1\)$1$ and the total passes \(n\)$n$, which Condition 2 forbids. With Condition 4 bounding \(B\)$B$ below \(1 / (1 + D)\)$1/(1+D)$, the ceiling over every shrink a net admits is \(\lceil \sqrt{n} \rceil/ (1 + D)\)$\lceil \sqrt{n}\rceil /(1+D)$, and refining the net raises it only as fast as \(D\)$D$ falls — about \(T / K\)$T/K$, so twice the directions for half the gap, and twice the cost of every decision taken over them. Since the grid packing gives \(s(n) \le \lceil \sqrt{n} \rceil\)$s(n)\le \lceil \sqrt{n}\rceil$ for free, this ceiling always sits strictly below the trivial upper bound: no single certificate of this shape certifies the grid value. For \(n = 12\)$n=12$ that bites: the ceiling is \(4B = 3.9908\)$4B=3.9908$, the conjectured value is \(4\)$4$, and \(99/25\)$99/25$ has \(0.0308\)$0.0308$ of runway to the ceiling and that is all there is for one certificate. What the ceiling does not exclude is a proved family of certificates with sides tending to \(4\)$4$ and a limit argument on top of it; whether such a family exists is a question about the covering value, which nothing here settles. Nor does it bind a certificate of a different shape. Evan Daniel’s third-party \(s(32) = 6\)$s(32)=6$ is a weighted cover of the closed container \([0,6]^2\)$[0,6{]}^2$ itself, decided at margin zero by an exact subdivision of pose space rather than over a direction net, and it certifies the grid value directly (n-032). \(n = 11\)$n=11$ and \(n = 17\)$n=17$ are not foreclosed: their runways are \(0.1808\)$0.1808$ and \(0.3985\)$0.3985$, and both truths sit below their grid bounds. At \(n = 19\)$n=19$, \(20\)$20$ and \(21\)$21$ the ceiling is \(5B = 4.9885\)$5B=4.9885$, so T-020 has \(0.1885\)$0.1885$ above it at twenty and twenty-one; at nineteen the best known packing binds first and the runway is \(0.0856\)$0.0856$. \(s(21) = 5\)$s(21)=5$ was reached by a mixed cover, a certificate of a different shape, which puts mass on the grid lines as well as on points.

Joining that ceiling against the register says the lane has been looking in the wrong place. CERTIFICATE-REACH.md ranks all 100 cases by the most a certificate could add. The two this program has spent itself on are near the bottom: \(n = 11\)$n=11$ has \(+0.0590\)$+0.0590$ to its packing-side cap (\(+0.0671\)$+0.0671$ to Trump’s packing itself, which the cap says no certificate on this net reaches) and \(n = 17\)$n=17$ has \(+0.0810\)$+0.0810$. The largest are all just above a perfect square, where the lower bound is Nagamochi’s closed form and the gap to the best known packing runs near half a unit — eleven cases above \(+0.49\)$+0.49$, headed by \(n = 51\)$n=51$ at \(+0.5364\)$+0.5364$, then \(68\)$68$, \(84\)$84$, \(39\)$39$, \(86\)$86$, \(66\)$66$, \(38\)$38$, \(83\)$83$, \(37\)$37$, \(53\)$53$ and \(26\)$26$. Two cautions travel with that ranking. The prize is what the ceiling allows; the real limit is the covering value at that side. 46 values have been reported for the restricted program, at sides \(2.99\)$2.99$, \(3.81\)$3.81$, \(3.82\)$3.82$, \(3.83\)$3.83$, \(3.84\)$3.84$, \(3.85\)$3.85$, \(3.875\)$3.875$, \(3.95\)$3.95$, \(3.96\)$3.96$, \(3.965\)$3.965$, \(3.969\)$3.969$, \(3.97\)$3.97$, \(3.98\)$3.98$, \(3.985\)$3.985$, \(3.99\)$3.99$, \(4.58\)$4.58$, \(4.59\)$4.59$, \(4.6\)$4.6$, \(4.61\)$4.61$, \(4.67\)$4.67$, \(4.675\)$4.675$, \(4.6775\)$4.6775$, \(4.679\)$4.679$, \(4.68\)$4.68$, \(4.69\)$4.69$, \(4.7\)$4.7$, \(4.80\)$4.80$, \(4.81\)$4.81$, \(4.82\)$4.82$, \(4.825\)$4.825$, \(4.85\)$4.85$, \(4.855\)$4.855$, \(4.86\)$4.86$, \(4.865\)$4.865$, \(4.875\)$4.875$, \(4.88\)$4.88$, \(4.895\)$4.895$, \(4.985\)$4.985$, \(5.13\)$5.13$, \(5.25\)$5.25$, \(5.48\)$5.48$, \(5.59\)$5.59$, \(5.7\)$5.7$, \(5.8\)$5.8$, \(6.75\)$6.75$ and \(6.84\)$6.84$ — the first eight reports, not measurements this repository can reproduce, since no covering-search run log or solver checkpoint was retained for any of them; the ten added on 2026-09-05 by Agenda 021’s BC-200 and BC-197 and Agenda 022’s BC-213 and BC-206 carry run logs; the \(2.99\)$2.99$ pair added on 2026-09-18 by session-139 is H-216 calibration at n=6 (covering \(6.08216\)$6.08216$ and \(6.07724\)$6.07724$ on two named site sets, both ≥ 6, not a bound); \(3.81\)$3.81$ is the session-139 T-025-seeded auto-plus-60 at 381/100, covering \(11.000000\)$11.000000$ unconverged on the eleven plateau, site set refuted, side open; \(3.82\)$3.82$ also has the session-139 T-025-seeded auto-plus-60 plus --seed-windows 5 at 191/50, covering \(11.018646\)$11.018646$ converged, closest session-139 point-atom construction, site set refuted; T-026-seeded auto-plus-60 at the same side converged \(11.033743\)$11.033743$, worse than the threshold seed; \(3.83\)$3.83$ is the session-139 n=11 probes at 383/100, covering \(11.192598\)$11.192598$ (auto grids), \(11.142857\)$11.142857$ (four-grid), and \(11.140351\)$11.140351$ (T-025-seeded four-grid), all site sets refuted, side open; \(3.84\)$3.84$ is the same T-025-seeded auto-plus-60 construction at 96/25, covering \(11.371819\)$11.371819$ converged, site set refuted; \(3.85\)$3.85$ also has the session-139 T-025-seeded auto-plus-60 at 77/20, covering \(11.456576\)$11.456576$ converged, site set refuted; \(3.875\)$3.875$ is the same construction at 31/8, covering \(11.561186\)$11.561186$ converged, site set refuted, 0.002 below the packing; \(3.965\)$3.965$ is the session-141 n=12 T-017-seeded auto plus windows 7 at 793/200, covering \(12.067502\)$12.067502$ unconverged, still above twelve, the first first-party covering row at that side; a session-141 T-017-seeded four-grid plus windows 7 finished at \(12.066995\)$12.066995$ unconverged, still above twelve; \(3.969\)$3.969$ T-017-seeded auto-grid dropped to \(12.118036\)$12.118036$ unconverged, still above twelve; T-017-seeded four-grid at the same side dropped to \(12.116115\)$12.116115$ unconverged; a session-140 leftover T-017-seeded four-grid plus windows 7 finished at \(12.091168\)$12.091168$ unconverged, still above twelve; \(4.6\)$4.6$ is the session-139 n=17 auto-grid probe at 23/5, covering \(17.331710\)$17.331710$ unconverged, site set refuted, side open; the T-019-seeded auto grid at the same side dropped to \(17.049597\)$17.049597$ unconverged, still above seventeen; T-019-seeded auto plus --seed-windows 5 dropped to \(17.042346\)$17.042346$ unconverged; a session-140 T-019-seeded four-grid plus windows 8 finished at \(17.120106\)$17.120106$ unconverged, still above seventeen; \(4.61\)$4.61$ is the session-140 leftover n=17 T-019-seeded auto plus windows 5 at 461/100, covering \(17.195968\)$17.195968$ unconverged, one cent above \(23/5\)$23/5$; \(4.67\)$4.67$ is the session-139 n=18 auto-grid probe at 467/100, covering \(18.000000\)$18.000000$ unconverged, cannot confirm; the T-019-seeded auto grid at the same side converged \(17.875567\)$17.875567$ with least_covered 1, freeze-then-decide retained T-027 at \(s(18) \ge 467/100\)$s(18)\ge 467/100$; \(4.675\)$4.675$ is the session-140 T-027-seeded auto plus windows 5 at 187/40, freeze-then-decide retained T-028 at \(s(18) \ge 187/40\)$s(18)\ge 187/40$; \(4.6775\)$4.6775$ is the session-141 leftover T-028-seeded auto plus windows 5 at 1871/400, freeze-then-decide retained T-029 at \(s(18) \ge 1871/400\)$s(18)\ge 1871/400$; \(4.679\)$4.679$ is the session-141 T-029-seeded auto plus windows 5 at 4679/1000, freeze-then-decide retained T-030 at \(s(18) \ge 4679/1000\)$s(18)\ge 4679/1000$; \(4.68\)$4.68$ T-019-seeded auto-grid locked at exact mass \(18.000043\)$18.000043$ converged, cannot confirm; T-019-seeded auto plus --seed-windows 5 at \(4.68\)$4.68$ locked \(18.000000\)$18.000000$ unconverged; T-027-seeded auto at the same side locked \(18.000000\)$18.000000$ unconverged; \(4.69\)$4.69$ T-019-seeded auto-grid locked \(18.000000\)$18.000000$ unconverged; \(4.7\)$4.7$ T-019-seeded auto-grid converged \(18.165413\)$18.165413$, cannot confirm; retained checkpoint and frozen-certificate availability differs by row. \(4.81\)$4.81$ is the session-140 n=19 T-020-seeded auto plus windows 6 at 481/100, covering \(19.132115\)$19.132115$ unconverged, closer than the same construction at \(4.85\)$4.85$ (\(19.808958\)$19.808958$); a session-141 T-020-seeded four-grid plus windows 7 finished at \(19.111435\)$19.111435$ unconverged, still above nineteen. \(4.82\)$4.82$ is the session-140 leftover n=19 T-020-seeded auto plus windows 6 at 241/50, covering \(19.247109\)$19.247109$ unconverged, farther than \(4.81\)$4.81$ on the same site set; a session-141 T-020-seeded four-grid plus windows 7 finished at \(19.224565\)$19.224565$ unconverged, still above nineteen. \(4.855\)$4.855$ is the session-140 leftover n=20 T-021-seeded auto plus windows 6 at 971/200, covering \(19.910044\)$19.910044$ unconverged, still below 20. \(4.86\)$4.86$ is the session-141 n=20 T-021-seeded four-grid plus windows 7 at 243/50, covering \(19.887914\)$19.887914$ unconverged, still below 20. \(4.88\)$4.88$ is the session-156 n=21 exp-229 trio at 122/25: a T-021-seeded auto plus windows 6 stopped at its deadline at \(20.040960\)$20.040960$ unconverged; seedless auto plus windows 5 converged at \(20.131946\)$20.131946$, but the interval route stalled on a seam where window rows sit exactly \(B\)$B$ apart and refused the freeze, which decides nothing; seedless auto with no windows converged at \(20.145556\)$20.145556$, and freeze-then-decide retained T-034 at \(s(21) \ge 122/25\)$s(21)\ge 122/25$. \(5.13\)$5.13$ is the session-141 n=26 seedless auto plus windows 5 at 513/100, covering \(25.000000\)$25.000000$ unconverged, still below 26, the first first-party covering row at that size. \(5.25\)$5.25$ is the session-141 n=27 seedless auto plus windows 5 at 525/100, covering \(25.000000\)$25.000000$ unconverged, still below 27, the first first-party covering row at that size. \(5.48\)$5.48$ is the session-141 n=29 seedless auto plus windows 5 at 548/100, covering \(26.040745\)$26.040745$ converged with freeze mass \(26.0409395\)$26.0409395$; the interval route refused the freeze, the first first-party covering row at that size. \(5.59\)$5.59$ is the session-141 n=30 seedless auto plus windows 5 at 559/100, covering \(27.178193\)$27.178193$ unconverged, still below 30, the first first-party covering row at that size. \(5.7\)$5.7$ is the session-141 n=31 seedless auto plus windows 5 at 57/10, covering \(28.331329\)$28.331329$ unconverged, still below 31, the first first-party covering row at that size. \(5.8\)$5.8$ is the session-141 n=32 seedless auto plus windows 5 at 29/5, covering \(29.803318\)$29.803318$ unconverged, still below 32, the first first-party covering row at that size. \(6.75\)$6.75$ is the session-141 n=44 seedless auto plus windows 5 at 675/100, covering \(41.236782\)$41.236782$ unconverged, still below 44, the first first-party covering row at that size. \(6.84\)$6.84$ is the session-141 n=45 seedless auto plus windows 5 at 684/100, covering \(42.137360\)$42.137360$ unconverged, still below 45, the first first-party covering row at that size. Several sides are reported more than once from site sets built differently, which is the point of reporting them that way: at \(4.85\)$4.85$ the difference is between a wall and the certificate T-021 rests on, at \(4.865\)$4.865$ it is two independent walls plus a session-140 four-grid-plus-windows-7 construction that stopped at \(19.930198\)$19.930198$ unconverged without crossing, and at \(3.97\)$3.97$ it is a converged grid optimum of \(12.364038\)$12.364038$ above a cutting-plane row LP of \(12.248227\)$12.248227$ and a session-140 T-017-seeded four-grid-plus-windows-7 freeze at \(12.133391\)$12.133391$, and a session-141 T-017-seeded auto-plus-windows-7 row at \(12.097146\)$12.097146$ unconverged, with a historical reported floor of \(10.845594\)$10.845594$. That floor cannot currently be replayed because its generating family and state are missing; D-478 records the evidence gap.

The middle tier is built and works within the explicit boundaries above. Two instruments now agree on the cell decomposition to \(4.4 \times 10^{-16}\)$4.4\times {10}^{-16}$ and on the corner’s slopes to three decimals. Floating-point LP refinement reaches its declared solver floor on both proved instance cells. The current hypothesis-status aggregate is reconciled from the generated ledger in Current research readiness, and the campaign has a defect log that has already predicted a recurrence.

For record-finding, the bottleneck has moved from polish to proposal. Nothing in the current toolkit reaches Trump’s standing side, and the refiner cannot rescue the tested starts by construction; no sampled \(n \ge 5\)$n\ge 5$ full terminal-component relation has been measured. The named candidates are δ-continuation, angle-class search as a search rather than an assumption, neighbour-transfer seeding, and quality-diversity retention—none built.

The cartography premise is still untested, and now blocked on the first nontrivial component question. The claim that mapping terminal components is the best route to records rests on record basins being rare in quench measure, and H-012 is the measurement that would refute it. The independent proof, construction, exact-value, and asymptotic lanes do not depend on that premise. The quench supplies one needed instrument, and exact \(n = 3\)$n=3$/n = 4 identity controls now pass, but sampled terminal identity at \(n = 5\)$n=5$ is not ready. What is not settled is what a basin is.

D-034 is the open defect that says so. The exact \(n=3\)$n=3$ side-2 sliding family proves that one connected optimal set produces many geometric keys. Its open stratum retains one contact certificate, but the wall endpoint has a different certificate after node attributes were restored; exp-014 fixes the stale closed-family claim recorded as D-140. At \(n=5\)$n=5$, exp-033 replaces the matching-summary conjecture with a narrow exact result. After one D4 action and relabelling, four squares coincide and the fifth slides through an exact side-constant segment in one fixed-angle cell. An exact dual proves optimality within that cell, while active fixed-side nullity changes from zero at each endpoint to one in the interior. Exp-034 proves that exact face lies in a two-parameter angle-and-slide sheet of orientation-indexed LP optima. Exp-035 derives both owner-axis first-order systems at the two endpoints and one interior point and verifies one exact non-sheet direction in each. Certified nonlinear continuation must still decide whether that direction is a true motion in the full component; the unequal-side rows still need minimax-clearance bounds.

So distinct_basins currently counts family members, the discovery curve cannot plateau, and H-011’s saturation criterion is unreachable until the definition is fixed. The three candidate definitions are written up on think-1s0h; none is a code tweak, because this is the deliverable’s own shape. Until that is settled and the census runs, the cartography program is a well-argued bet rather than a finding.

The mathematical-frontier review now keeps several independent routes alive rather than making the census spine the whole program: Trump’s nonsmooth local geometry, exact small-n quotient spaces, held-out construction surgery, pure-point piercing limits, robust restricted-angle proofs, \(s(12)\)$s(12)$, \(s(61)\)$s(61)$, exact record fields, and the asymptotic waste exponent.

The small-n lane was missing its direct prior art. D-139 records the omission. Two primary hard-square configuration-space papers are now archived; the Plakhta paper remains explicitly publisher-blocked, so no novelty language is permitted until its scope is checked from a lawful primary copy.

The first fast rotation is cheap and high-information. Exp-012 exposed that H-024’s formal prerequisite was missing, while exp-037 separately rejected the corresponding numerical claim H-042. Exp-013 confirmed H-026 and locally isolated Trump’s pose, and exp-014/015 solved the exact \(n=3,4\)$n=3,4$ quotient controls in 1.28 wall seconds. Exp-033 then certified the \(n = 5\)$n=5$ equal-side pair’s exact fixed-angle face in 0.24 wall seconds of generation plus replay. Exp-034 through exp-036 then certify an exact angle-and-slide sheet, a non-sheet first-order direction, and an exact second-order obstruction to that displayed direction in 0.76 further wall-seconds. Exp-038 adds the complete branchwise first-order inventory in 1.06 wall-seconds. Next certify the discovered fixed-angle optimal-position polytope, test transverse and mixed nonlinear realization, bound clearance between the unequal-side rows, and hide the UnitSquare \(n = 68,69\)$n=68,69$ children for the first parent-surgery test. The quantitative Trump successor is an explicit isolation radius or minimal-support stress analysis, not another rank count. No hour-scale lane is promoted without a known-answer response, independent validity, and a result that changes a decision.

The normal checkpoint and blocking macOS deep golden are green; broader unattended launch is not yet authorized. At that checkpoint the tree passed all 31 normal-gate steps in 97.68 wall-seconds, including seven exact small-n replays, 59 pytest contracts, and all 62 mutation controls. The gate has since grown to 59 steps, of which the pull-request tier runs 35; the sentence is dated rather than restated because no check guards this number, so a current-tense figure here silently goes stale — as it did twice on 2026-09-03, once when a second step budget landed and once when the results-headline check did. The first deep regeneration had reproduced one unsettled \(n=4\)$n=4$ proposal and an \(n=10\)$n=10$ \(1.503 \times 10^{-10}\)$1.503\times {10}^{-10}$ pair-row residual. D-199 identifies and fixes the n=10 cause: repairing first-call offenders 49 and 66 exposes previously clean row 61, which a third conservative call settles with zero all-original-row residual. All seven ladder rungs now converge at pool widths 10 and 1. D-203 isolated the remaining n=4 seed-0 stop as a distinct HiGHS status-4 Solve error. Its retained LP is not malformed or globally ill-conditioned: independent exact primal/dual certificates prove the finite optimum \(2.00103283426408968\)$2.00103283426408968$, rank 9, and zero duality gap. The failure is dual-simplex presolve/postsolve instability on a thin near-degenerate optimal face. Strict highs-ipm solves the identical LP with zero original-row residual; default tolerances and presolve-off simplex are rejected because their residuals exceed \(10^{-10}\)${10}^{-10}$. The status-4-only fallback keeps the same LP, tolerances, four-call cap, and all-row screen. The bounded seed-0 replay reaches proved side 2 with all 3,692 fixed-point evaluations settled; the independent verifier accepts every square and pair. The direct blocking macOS deep golden then rebuilds \(n=4\)$n=4$ at 4/4 converged and passes all seven proved ladder rungs. D-272 records the removal of the temporary expected-failure wrapper after that recovery, with Linux and macOS green at b582fe1. D-266 records a soundness error caught in the first fallback draft: a primary status 4 followed by IPM status 2 was briefly promoted to mathematical infeasibility. The corrected classifier reserves infeasible for a sole primary status-2 receipt and keeps every mixed-method failure numerical. D-260 through D-262 record and correct the fixture-capture hazards found before commit: a cross-wired geometric context, a receipt that initially defined its own acceptance, and a pytest-only completion claim while static checks were red. The retained millisecond fixture now exact-rebuilds all LP inputs, rejects the cross-wire mutation, and either reproduces status 4 or admits only a finite successful solve whose original-row residuals remain at or below \(10^{-10}\)${10}^{-10}$. D-263 records a coordinator recurrence during that reconciliation: a status-only patch again touched D-034 instead of the named new defect. The exact named-status audit restored D-034 and closed only D-260 through D-263. D-225 preserves the decision boundary: a normal no-skip gate and owned limitations suffice for a checkpoint merge, while unattended execution requires fresh strict/deep evidence. It does not turn this repaired small-n result into a general producer-health claim. D-202 separately keeps final-receipt capture open after one delegated long command terminated without returning its output; the evidentiary rerun used a durable parent-owned session. D-217 is the same failure in a local parallel validation wrapper: its unreceipted result was discarded and rerun directly, while think-b3bm still owns the portable yielded-command and terminal-polling rehearsal. D-222 records a separate audit-scope violation caught during this merge review: an explicitly excluded strict run was terminated by exact process group, its partial output discarded, and think-ysz2 owns explicit command and wall ceilings for future bounded delegations. The repaired small-n path no longer blocks the campaign, but unattended numerical work still lacks a reproducible work-based quench budget (D-126), a bound around pure-Python validation workers and the aggregate duration of multi-command steps (D-239), and portable terminal-receipt discipline for delegated long commands (D-202). D-280 records the phase-count cap exhausting the fast campaign early; its continuation remains open.

One open measurement defect constrains timing forecasts. D-101: the historical exp-007/008 round-level wall times disagree with retained per-call durations. Price the first maps from raw calls or a current receipt until those aggregates are reconstructed.

One contained defect constrains every floating-point LP result. D-021: the solver floor is about \(10^{-11}\)${10}^{-11}$ in the side, so this numerical method cannot resolve finer. The general fix is an exact LP over certified rational or algebraic coefficients; the rational special case alone is not a universal remedy.

The destructive negative-control path is closed. D-035: negctl now mutates bounded private source snapshots, so a killed control can abandon only temporary data and cannot leave deliberate sabotage in the checkout.

Mutation-control timeouts are bounded. D-129 is fixed: each control has a finite deadline, runs in its own process group, and is terminated and reaped after TERM and then KILL if necessary. This closes that specific gate-stall path; the unattended numerical runner still has the separate launch requirements above.

Validation subprocesses now have finite POSIX deadlines. The shared captured-command path and quiet Git provenance probes use a 900-second production default, configurable by CLI or environment, and retain smaller call-site caps. Timeout and coordinator interruption terminate and reap the registered process groups. D-239 remains open because pure-Python worker code, aggregate multi-command duration, detached daemons, and Windows process-tree cleanup are not bounded by that policy. A strict gate therefore still needs an independent outer watchdog for unattended use.

One open defect makes quench evidence load-dependent. D-126: the scientific work budget is still wall-clock time, so contention changes the number of LP solves and probes performed. Price and compare basin experiments by retained work units; use the wall clock only as a recorded outer deadline.

A second contained defect makes the LP count itself unreliable on aborted runs. D-349: _free_sweep accumulates its own LP count and returns it, and quench_bracket adds that total only on the normal return path, so a sweep that raises on its wall budget or on an unsettled cell carries the partial count away with it. The reported lp_solves therefore understates any run that stopped inside a free sweep. The direction is conservative and the fix is deferred because it changes figures already reported in past rounds, but a per-solve efficiency number computed from a budget-cut run is too favourable until it lands. The Motion Lab timeline is what made it visible: it retains one event per solve, so an aborted sweep has more retained events than the counter describing them.

References

Primary sources are archived locally under resources/; the citation keys below resolve there and in the per-case frontier/ artifacts. Each entry names what this project relies on it for.

• Stromquist, W. (2003). Packing 10 or 11 unit squares in a square. Electronic Journal of Combinatorics 10(1), R8. Supplies \(s(10)\)$s(10)$, states the \(s(11)\)$s(11)$ lower-bound value, and proves the \(0^{\circ}\)$0^{\circ }$/45° class bound. Exp-016 refutes its printed unrestricted Figure 14 cover; exp-017 independently certifies the same value with a source-distinct repair.
• Trump, W. (1979). The \(n = 11\)$n=11$ packing, as published on the Squares in Squares record page with Ellsworth’s exact solution in the SVG source. The standing upper bound.
• Friedman, E. (2009). Packing Unit Squares in Squares: A Survey and New Results. Electronic Journal of Combinatorics, DS7. The survey the corpus is checked against.
• Erdős, P. and Graham, R. L. (1975). On packing squares with equal squares. The asymptotic waste line of work.
• Nagamochi, H. (2005). Packing unit squares in a rectangle. The general closed-form lower bound used where the register has no stronger formal evidence.
• Montanher, T. et al. (2018). Rigorous packing of unit squares into a circle. The only rigorous computer-assisted optimality proof for rotatable unit squares in any container, and the scope limit on what sqpack claims.
• Doye, J. P. K., Miller, M. A. and Wales, D. J. (1999). The double funnel energy landscape of the 38-atom Lennard-Jones cluster. The precedent behind the rarity premise.
• Stillinger, F. H. and Weber, T. A. (1982). Inherent structures and the quench map. The decomposition T-2 supplies a cell-exact version of.
• Mouret, J.-B. and Clune, J. (2015). Illuminating search spaces by mapping elites. The precedent behind H-015.