s(17) > 8893/2000 — a certified lower bound for packing 17 unit squares in a square

s(17) > 8893/2000 — a certified lower bound for packing 17 unit squares in a square Claim (grade: certified): s(17) > 8893/2000. A self-contained result capsule: a theorem, its machine-checkable proof object, and an independent verifier that builds offline from vendored sources (no network, no repository). The trust chain terminates in an artifact, not a process; see CLAIM.md and reproduce.sh. Licensing: code (checker/) is MIT OR Apache-2.0; artifacts are CC-BY-4.0. Result obtained: 2026-07-16. Prior art (improves): s(17) >= (40*sqrt(2)+19)/17 ~= 4.44521.