Verification

Each result has an identifier, a claim, and three ratings: S, its significance; V, the strongest verification its original evidence supports; and C, what this repository has confirmed independently. For results by others, this repository assigns V and C under its review policy. Each ladder links to its rubric; each rung has a tooltip with its full meaning.

Level
Significance How significant is the result?
Verification How was it originally verified?
Confirmation How has it been confirmed?
Level 5
Moves a central open case, or broad adoption
V5Formal, expert-reviewed
C5Formal, replayed here, open, two experts
Level 4
Reusable technique, bound family, or settled value
V4Mechanized, AI-reviewed, human-overseen
C4Mechanized confirmation, AI-reviewed, overseen
Level 3
A substantive case result or machine audit
V3Checkable; review record pending
C3Machine-replayed; review record pending
Level 2
A citable detail that changes no theorem
V2Proof asserted, not recoverable
C2Replayed, no machine certificate
Level 1
Bookkeeping or a routine consequence
V1Numerically checked
C1Read
Level 0
V0Claimed or recorded only
C0Recorded

The ladders grade a result. Its evidence carries an assurance label: reported, a named source’s claim not checked here; numerically checked, a finite-precision calculation with its precision, rounding and tolerance recorded; or verified, an exact check, rigorous interval certificate or complete proof covering the claim and its preconditions. A verified packing proves an upper bound; optimality also needs a matching verified lower bound.

Finite precision is not enough where squares touch exactly. A tolerance that accepts a true zero-gap contact also accepts a small overlap, so a contact-heavy packing requires exact algebraic signs or outward-rounded intervals (why). Schadt’s n=29 packing passes its 300-digit numerical check, while the verified interval witness proves a slightly weaker side. Trump’s n=11 packing is verified exactly over a degree-eight number field, including fourteen zero-gap contacts.

These checks also audit published work: T-004 and T-008 check Bentz’s 2010 Theorem 8, including both halves of s(46)=7, and T-011 checks Trump’s 1979 packing for eleven squares. The theorem remains the source’s; this repository adds an exact machine check.

A result’s kind is lower bound, upper bound, optimality (settling an exact value), or a kind that bounds no case, such as rigidity, case exclusion, simplification (a simpler proof of a value another result establishes) or formalization (a proof in a proof assistant of a value another result establishes).

Credits name the source’s authors; this project’s results are credited to Levy as Levy. X after Y means X’s result rests directly on Y’s proof, method or tool.

A result’s status is recorded (registered from its source without review or replay here), reviewed (its argument read here), confirmed (its certificate replayed successfully) or incomplete (a known defect remains open). Of the 261 results, 212 are confirmed; the rest are 33 recorded, 14 reviewed and 2 incomplete. Status follows the confirmation rung and is never set by hand; the status policy defines it. In analysis marks a review or replay under way here; waiting on marks a request with the source or another party.

A bound is superseded when no current case bound rests on it and the bounds recorded for its cases match or beat it. A better bound not yet adopted by its case records remains unmarked. For other kinds, superseded means the register records a later result implying the whole claim; superseded in part means it implies only part, so the original remains current. The table names the most recent replacement, with “and others” when needed; the full record lists every replacement.

Project Epistemics