A Machine-Checked Numerical Ledger for the Locked Sextic Fourfold x0^5x3+x3^6+x1^5x4+x4^6+x2^5x5+x5^6 in Lean 4

A core Lean 4 development (no Mathlib) recording numerical and combinatorial data for the sextic fourfold X=V(F) in P^5, F=x0^5x3+x3^6+x1^5x4+x4^6+x2^5x5+x5^6, plus a status ledger for the open question of whether X has a nontrivial Fourier–Mukai partner. Proved (36 kernel-checked theorems): the Berglund–Hübsch–Krawitz exponent block and transpose (determinant 30 per block, 30^3 total), dual weights, recorded intersection numerals for a plane and the residual quintic surface, sample evaluations of a polynomial identity, and a specification record for a written partner. Not proved: the numerals are recorded values checked by computation; the geometry producing them is not formalized, and no derived equivalence is constructed or claimed. The Fourier–Mukai partner question remains open. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/DerivedCategories at commit 7623188a2fafb28496e2144d0c932fb7679669f7.