A two-variable Fischer norm inequality and Pate's two-index permanent inequality

This preprint presents the Pate two-index permanent inequality for complex Hermitian positive-semidefinite matrices of every finite size at least two, with sharp constant 2 and the complete equality characterization. Equality holds exactly when the matrix has a zero row or both selected rows have zero off-diagonal entries. The release includes a complete Lean 4 formalization with pinned Mathlib dependencies, a readable Fischer-norm proof, and preserved successful clean-build, native-kernel replay, Lean4Lean replay, transitive axiom-audit and manuscript-versus-Lean statement-comparison evidence. The formal theorem is Pate.full_target. The inequality is the two-index challenge attributed to Pate and recorded as Conjecture 11 in Wanless (2022). This release makes no claim of first proof, first formalization or worldwide novelty. It does not assert the stronger full permanental eigenvalue conjecture. This is a preprint, not peer reviewed or independently verified by a human referee. AI assistance in research exploration, mathematical derivation, drafting, code generation, formalization, verification and release preparation is disclosed in AI_USE.md. The manuscript and research documentation/data use CC BY 4.0; source code and scripts use MIT, as specified in LICENSE.md. GitHub repository: https://github.com/gkamal666/pate-two-index-inequalityGitHub release v1.0.0: https://github.com/gkamal666/pate-two-index-inequality/releases/tag/v1.0.0