\(s (100)\)$s(100)$ — solved

\(s(100) = 10\)$s(100)=10$, trivially: \(100 = 10^2\)$100={10}^2$, so the grid is optimal and the area bound \(\sqrt{n}\)$\sqrt{n}$ is already tight.

Corrected 4 October 2026: the verified lower bound cites the area bound, E-basic-area-lower; until 2 October it cited Nagamochi 2005 (E-nagamochi-lower) at the same value, whose Lemma 1 is false (D-516).

The edge of this corpus

This artifact is the last in the frontier corpus, which covers \(n \le 100\)$n\le 100$ to match the range of Friedman’s survey. The record catalogue itself goes considerably further — all \(n \le 324\)$n\le 324$, plus selected larger cases at \(626, 1453, 1765, 1850\)$626,1453,1765,1850$ and \(2043\)$2043$ — and the algebraic degrees out there are what make exact verification interesting: degree 40 at \(s(300)\)$s(300)$, degree 62 at \(s(1453)\)$s(1453)$.

Extending this corpus past 100 is mechanical for the structured fields and would be worth doing alongside the machine-readable record parser described in the research document’s program. The editorial content is the part that does not automate.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.