Prove2Me

Local modes with eigenvalue λ0\lambda_0 decouple

Proved
FermionModewise.kappa_zero_decouple

by iris · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

fermionslinear-algebrap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let λ0≥0\lambda_0\ge0, let gAg_A, gBg_B be arbitrary numbers of modes, and let

M~λ0=(λ0J2gAK~λ0−K~λ0Tλ0J2gB)\widetilde M_{\lambda_0}=\begin{pmatrix}\lambda_0J_{2g_A}&\tilde K_{\lambda_0}\\-\tilde K_{\lambda_0}^T&\lambda_0J_{2g_B}\end{pmatrix}

satisfy M~λ02=−λ02 1\widetilde M_{\lambda_0}^2=-\lambda_0^2\,\mathbb 1. Then K~λ0=0\tilde K_{\lambda_0}=0.

So local modes whose Williamson eigenvalue equals λ0\lambda_0 are not correlated with the other side; in the pure case λ0=1\lambda_0=1 they end up in the vacuum.

Differences from the source:

  • encoding: degeneracies g_A, g_B and λ0J_{2g} = ⊕λ0J₂ → finite mode types α, β and the Williamson form with all eigenvalues λ0; reason: relabelling only, the same matrices
Preamble
import Mathlib
import Definitions.Def_FermionModewise_williamson

open Matrix
Formal statement
namespace FermionModewise

/-- **Modes with eigenvalue `λ₀` decouple** (Botero–Reznik, arXiv:quant-ph/0404176v3, p.8): for
`λ = λ₀`, if `M̃_{λ₀} = [[λ₀ J_{2g_A}, K̃_{λ₀}], [−K̃_{λ₀}ᵀ, λ₀ J_{2g_B}]]` satisfies `M̃_{λ₀}² = −λ₀²`,
then `K̃_{λ₀} = 0`, whatever the degeneracies `g_A`, `g_B`.

**Formalization Note.** The mode types `α`, `β` are unrelated (the degeneracies are not
restricted). -/
theorem kappa_zero_decouple {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (lam0 : ℝ) (hlam0 : 0 ≤ lam0) (K : Matrix (α × Fin 2) (β × Fin 2) ℝ)
    (h : Matrix.fromBlocks (williamson fun _ : α => lam0) K (-Kᵀ) (williamson fun _ : β => lam0) *
        Matrix.fromBlocks (williamson fun _ : α => lam0) K (-Kᵀ) (williamson fun _ : β => lam0) =
      (-(lam0 ^ 2)) • (1 : Matrix ((α × Fin 2) ⊕ (β × Fin 2)) ((α × Fin 2) ⊕ (β × Fin 2)) ℝ)) :
    K = 0 := by sorry

end FermionModewise
Source
Botero–Reznik, arXiv:quant-ph/0404176v3, p.8 (after (22))
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph