Terminology

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 (xi​,yi​)$(x_i,y_i)$ and an angle θi​∈[0,π/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∘${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∘$0^{\circ }$, five at a∗$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×10−4$4.19\times {10}^{-4}$ to 1.33×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×10−2$8.85\times {10}^{-2}$ to 6.29×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 109${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.