Mellin Gamma Kernel Identities and a Reciprocal Gamma Lattice in Lean 4

This preprint presents a scoped Lean 4 formalization built around the real kernel exp(-x^4). It defines an abstract complex Mellin transform slot, records the identity M(s) = (1/4) Gamma(s/4) as the explicit analytic input MellinKernelFormula, and proves that the corresponding reciprocal-Gamma expression equals the negative reciprocal of M(s). The package also verifies the real logarithmic readout ln(exp(-4k)) = -4k and membership of the points -4k in a discrete real lattice. The governing pinned project passed its Lake build, and the publication source and axiom audit passed trust-zero checks in that environment. The release includes the manuscript, Lean source, axiom audit, pinned dependency manifest, and verification receipt.