Orlov's Equivalence for a Sextic Fourfold as an Explicit Hypothesis: A Machine-Checked Lean 4 Interface

For the sextic F=x0^5x3+x3^6+x1^5x4+x4^6+x2^5x5+x5^6 (Gorenstein parameter 0), Orlov's theorem gives D^b(Coh V(F)) ≃ HMF^gr(F). This is recorded in Lean 4 as an explicit hypothesis structure (two placeholder types and a type equivalence). Proved, conditional on that structure: the forward map is bijective and inhabitation transfers; unconditionally, the recorded Gorenstein parameter is 0. Not constructed: any category, coherent sheaf or matrix factorization; Orlov's theorem is cited, not formalized. 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/orlov-equivalence-VF at commit a902788382a408bf15050b84a4f7b1a49669551e.