Theoretical Results

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+21​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)≥2+4/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\dots$$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∘$0^{\circ }$/45° class cannot achieve it. Stromquist bounds that orientation class below at 2+(4/3)2​≈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∘$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+2​/2$s=2+\sqrt{2}/2$ and Goebel’s labeled pose P0$P^0$ in C=(R2×S1)5$C=({ℝ}^2\times S^1{)}^5$, P0$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 P0$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(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)≥2+4/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.