feat(Foundations): Lean certificate for exact Vandermonde smoothness of the Z_2^3 K3

[gift-framework]

Summary

Adds GIFT/Foundations/K3VandermondeSmoothness.lean — a Lean 4 certificate for the finite integer content of the exact smoothness argument for the Z_2^3-equivariant complete-intersection K3 surface X = V(Q_1,Q_2,Q_3) ⊂ P^5 on the Vandermonde nodes (1,2,3,5,7,11):

• all twenty 3×3 minors of Λ equal the node-difference products (a_j-a_i)(a_k-a_i)(a_k-a_j) and are nonzero;
• the relevant 2×2 minors are nonzero, and the leading row of Λ is all ones.

Together these give full Jacobian rank wherever ≥3 coordinates are nonzero, and exclude points of X with ≤2 nonzero coordinates — the Jacobian-criterion input to "smooth K3". The passage from these finite facts to smoothness is the elementary §3.3 argument in the paper; this module machine-checks the finite part.

Backs Theorem 3.3 of the closed-form K3 Calabi–Yau residual paper (fourth machine-checked module alongside K3ClosedFormWitness, K3IsotypeLefschetzCertificate, G2IrrepLatticeCertificate).

Verification

• native_decide, zero sorry, zero added axiom (total axiom count unchanged at 15, matches README).
• Minor values verified independently in Python before building.
• Local build green: lake build GIFT.Foundations → 2533 jobs, exit 0.
• Local CI replay: zero sorry across GIFT/, axiom count 15 = 15 (README).

Wired into Foundations.lean (one import line).

🤖 Generated with Claude Code