What Is Built

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×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×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×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×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).