OccupationHilbertContractions

Abstract

Completed fermionic operators and their correlational estimate.

All types range over arbitrary universes. Underscores in declaration names appear as typographical subscripts and retain the full Lean spelling. Juxtaposition and the displayed binders use Lean function-application syntax; sums and products use Lean’s typed binder syntax. Bracketed typeclass requirements are anonymous instances. Real and complex casts retain their target-type annotation. Submodules and lp spaces in type position carry the ordinary CoeSort coercion. Nat subtraction is truncated, Nat division is Euclidean division, and field division is written with a slash. Named constants retain their actual Lean spelling. The three-dot marker suppresses only proof fields and proof arguments, which are proof-irrelevant; it never suppresses mathematical data. The additional h and g binders in construction equations stand for proofs of the displayed propositions; proof irrelevance makes the equation independent of their choice. Completed tensors are UniformSpace.Completion of the Mathlib Hilbert tensor product.

Definition 1.1 (CanonicalSequence).

$$\mathrm{CanonicalSequence}.\mathrm{mk}:(\mathrm{coeff}:\mathbb{N}\to \mathbb{R})\to (\forall (i:\mathbb{N}),0\le \mathrm{coeff}i)\to (\mathrm{Summable}\mathrm{fun}(i:\mathbb{N})\mapsto (\mathrm{coeff}i{)}^2)\to \sum ^{\prime }(i:\mathbb{N}),(\mathrm{coeff}i{)}^2=1\to \mathrm{CanonicalSequence}$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.CanonicalSequence (✓ std3).

Citation. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.2 (weighted_schur).

$$\forall \{\iota :\mathrm{Type}\}[\mathrm{Fintype}\iota ](K:\iota \to \iota \to \mathbb{R}),(\forall (ij:\iota ),0\le Kij)\to (\forall (ij:\iota ),Kij=Kji)\to \forall (f:\iota \to \mathbb{R}),(\forall (i:\iota ),0<fi)\to \forall (z:\iota \to \mathbb{C}),(\sum i:\iota ,\sum j:\iota ,((Kij):\mathbb{C})\ast \mathrm{star}(zi)\ast zj).\mathrm{re}\le \sum i:\iota ,(\Vert zi\Vert {)}^2\ast ((\sum j:\iota ,Kij\ast fj)/fi)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.weighted_schur (✓ std3). ∎

Citation. Issai Schur (1911). Bemerkungen zur Theorie der beschränkten Bilinearformen mit unendlich vielen Veränderlichen. DOI: 10.1515/crll.1911.140.1. URL: https://doi.org/10.1515/crll.1911.140.1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.3 (pairKernel_weighted_row).

$$\forall \{\iota :\mathrm{Type}\}[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ](a:\mathbb{R})(p:\iota \to \mathbb{R}),0\le a\to (\forall (i:\iota ),0\le pi)\to \forall (D:\mathrm{Finset}\iota ),(\sum E:\mathrm{Finset}\iota ,\mathrm{pairKernel}pDE\ast \mathrm{comparisonVector}apE)/\mathrm{comparisonVector}apD\le (\sum i\in D,pi)+((D.\mathrm{card}:\mathbb{R})+a\ast (\sum i\in D,pi))\ast (\sum j\in D^c,pj/(1+a\ast pj))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_weighted_row (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The product comparison vector bounds every pair-incidence row. A zero coefficient receives weight one, so the vector remains positive.

Theorem 1.4 (pairKernel_row_bound).

$$\forall \{\iota :\mathrm{Type}\}[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ](p:\iota \to \mathbb{R})(m:\mathbb{N}),1\le m\to \forall (\alpha :\mathbb{R}),0\le \alpha \to (\forall (i:\iota ),0\le pi)\to (\forall (i:\iota ),pi\le \alpha )\to (\sum i:\iota ,pi)\le 1\to 2\ast (m:\mathbb{R})\ast \alpha \le 1\to \forall (D:\mathrm{Finset}\iota ),D.\mathrm{card}\le m\to (\sum E:\mathrm{Finset}\iota ,\mathrm{pairKernel}pDE\ast \mathrm{comparisonVector}((m:\mathbb{R})-1)pE)/\mathrm{comparisonVector}((m:\mathbb{R})-1)pD\le (m:\mathbb{R})-(m:\mathbb{R})\ast ((m:\mathbb{R})-1)\ast (\sum i:\iota ,(pi{)}^2)+5/2\ast ((m:\mathbb{R}){)}^3\ast (\alpha {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_row_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.5 (pairKernel_row).

$$\forall \{\iota :\mathrm{Type}\}[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ](p:\iota \to \mathbb{R})(f:\mathrm{Finset}\iota \to \mathbb{R})(D:\mathrm{Finset}\iota ),\sum E:\mathrm{Finset}\iota ,\mathrm{pairKernel}pDE\ast fE=\sum i\in D,\mathrm{Real}.\mathrm{sqrt}(pi)\ast \sum j\in (D.\mathrm{erase}i{)}^c,\mathrm{Real}.\mathrm{sqrt}(pj)\ast f(\mathrm{insert}j(D.\mathrm{erase}i))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_row (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.6 (pairKernel).

$$\forall (\iota :\mathrm{Type})[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ](p:\iota \to \mathbb{R})(D:\mathrm{Finset}\iota )(E:\mathrm{Finset}\iota ),(\mathrm{pairKernel}(p)(D)(E):\mathbb{R})=(\mathrm{dotProduct}(\mathrm{fun}(R:\mathrm{Finset}\iota )\mapsto \mathrm{pairIncidence}pRD)(\mathrm{fun}(R:\mathrm{Finset}\iota )\mapsto \mathrm{pairIncidence}pRE))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.7 (pairIncidence).

$$\forall (\iota :\mathrm{Type})[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ](p:\iota \to \mathbb{R})(R:\mathrm{Finset}\iota )(D:\mathrm{Finset}\iota ),(\mathrm{pairIncidence}(p)(R)(D):\mathbb{R})=(\sum i:\iota ,\mathrm{if}i\in D\wedge R=D.\mathrm{erase}i\mathrm{then}\mathrm{Real}.\mathrm{sqrt}(pi)\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairIncidence (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.8 (denominator_sum_bound).

$$\forall \{\iota :\mathrm{Type}\}[\mathrm{Fintype}\iota ](p:\iota \to \mathbb{R})(a\alpha :\mathbb{R}),0\le a\to 0\le \alpha \to (\forall (i:\iota ),0\le pi)\to (\forall (i:\iota ),pi\le \alpha )\to (\sum i:\iota ,pi)\le 1\to \sum i:\iota ,pi/(1+a\ast pi)\le 1-a\ast (\sum i:\iota ,(pi{)}^2)+(a{)}^2\ast (\alpha {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.denominator_sum_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The rational cubic remainder is bounded using the coefficient cap and total mass. This estimate retains the negative fourth-moment correction for unrenormalized finite cutoffs.

Definition 1.9 (comparisonWeight).

$$\forall (a:\mathbb{R})(p:\mathbb{R}),(\mathrm{comparisonWeight}(a)(p):\mathbb{R})=(\mathrm{if}p=0\mathrm{then}1\mathrm{else}\mathrm{Real}.\mathrm{sqrt}p/(1+a\ast p))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonWeight (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.10 (comparisonVector_pos).

$$\forall \{\iota :\mathrm{Type}\}(a:\mathbb{R})(p:\iota \to \mathbb{R}),0\le a\to (\forall (i:\iota ),0\le pi)\to \forall (D:\mathrm{Finset}\iota ),0<\mathrm{comparisonVector}apD$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonVector_pos (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.11 (comparisonVector).

$$\forall (\iota :\mathrm{Type})(a:\mathbb{R})(p:\iota \to \mathbb{R})(D:\mathrm{Finset}\iota ),(\mathrm{comparisonVector}(a)(p)(D):\mathbb{R})=(\prod i\in D,\mathrm{comparisonWeight}a(pi))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonVector (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.12 (adapted_hilbert_basis).

$$\forall \{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{CompleteSpace}E]\{\iota :\mathrm{Type}\}\{v:\iota \to E\},\mathrm{Orthonormal}\mathbb{C}v\to \exists (w:\mathrm{Set}E)(b:\mathrm{HilbertBasis}(w:\mathrm{Type})\mathbb{C}E),\mathrm{Set}.\mathrm{range}v\subseteq w\wedge (b:(w:\mathrm{Type})\to E)=\mathrm{Subtype}.\mathrm{val}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.adapted_hilbert_basis (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.13 (annihilationCoordinate).

$$\forall (N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))(i:\mathbb{N})(R:\mathrm{Finset}\mathbb{N}),(\mathrm{annihilationCoordinate}(\psi )(i)(R):\mathbb{C})=(\mathrm{if}\neg (i\in R)\wedge (\mathrm{insert}iR).\mathrm{card}=N\mathrm{then}((-1){)}^{\{k\in R|k<i\}.\mathrm{card}}\ast (\psi :(i:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\to (\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})i)⟨\mathrm{insert}iR,\dots ⟩\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.annihilationCoordinate (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.14 (canonicalRayleigh).

$$\forall (N:\mathbb{N})(c:\mathrm{CanonicalSequence})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2)),(\mathrm{canonicalRayleigh}(c)(\psi ):\mathbb{R})=(2\ast \sum ^{\prime }(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}),(\Vert \sum ^{\prime }(i:\mathbb{N}),((c.\mathrm{coeff}i):\mathbb{C})\ast \mathrm{pairCoordinate}\psi (2\ast i)(2\ast i+1)(R:\mathrm{Finset}\mathbb{N})\Vert {)}^2)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.canonicalRayleigh (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.15 (coordinateClaim).

$$(\mathrm{coordinateClaim}:\mathrm{Prop})=(\forall (m:\mathbb{N}),1\le m\to \forall (c:\mathrm{CanonicalSequence})(\alpha :\mathbb{R}),(\forall (i:\mathbb{N}),(c.\mathrm{coeff}i{)}^2\le \alpha )\to 2\ast (m:\mathbb{R})\ast \alpha \le 1\to \forall (\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m\})\mapsto \mathbb{C})2)),\Vert \psi \Vert =1\to \mathrm{canonicalRayleigh}c\psi \le 2\ast (m:\mathbb{R})\ast (1-((m:\mathbb{R})-1)\ast (\sum ^{\prime }(i:\mathbb{N}),(c.\mathrm{coeff}i{)}^4)+5/8\ast ((2\ast (m:\mathbb{R})\ast \alpha ){)}^2))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateClaim (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.16 (coordinateRename).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(e:\mathrm{Function}.\mathrm{Embedding}AB)(h:\mathrm{Orthonormal}\mathbb{C}(\mathrm{fun}a:A\mapsto (\mathrm{lp}.\mathrm{single}2(ea)(1:\mathbb{C}):\mathrm{lp}({\mathrm{fun}}_{:}B\mapsto \mathbb{C})2))),(\mathrm{coordinateRename}(e):(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2){\to }_{li}[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))=(h.\mathrm{orthogonalFamily}.\mathrm{linearIsometry})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.17 (coordinateRename_image).

$$\forall \{A:\mathrm{Type}\}\{B:\mathrm{Type}\}(e:\mathrm{Function}.\mathrm{Embedding}AB)(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2))(a:A),(((\mathrm{coordinateRename}e:(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))\psi ):(i:B)\to (\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})i)((e:A\to B)a)=(\psi :(i:A)\to (\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})i)a$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename_image (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.18 (coordinateRename_outside).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(e:\mathrm{Function}.\mathrm{Embedding}AB)(\psi :\mathrm{lp}({\mathrm{fun}}_{:}A\mapsto \mathbb{C})2)(b:B),\neg (b\in \mathrm{Set}.\mathrm{range}e)\to \mathrm{coordinateRename}e\psi b=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename_outside (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.19 (countable_norm_sq).

$$\forall \{A:\mathrm{Type}\}(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2)),(\Vert \psi \Vert {)}^2=\sum ^{\prime }(a:A),(\Vert (\psi :(i:A)\to (\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})i)a\Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_norm_sq (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.20 (countable_norm_sq_summable).

$$\forall \{A:\mathrm{Type}\}(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2)),\mathrm{Summable}\mathrm{fun}(a:A)\mapsto (\Vert (\psi :(i:A)\to (\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})i)a\Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_norm_sq_summable (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Theorem 1.21 (countable_pair_sign).

$$\forall \{N:\mathbb{N}\}(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))(i:\mathbb{N})(R:\mathrm{Finset}\mathbb{N}),\neg (2\ast i\in R)\to \neg (2\ast i+1\in R)\to \forall (\mathrm{hN}:(\mathrm{insert}(2\ast i)(\mathrm{insert}(2\ast i+1)R)).\mathrm{card}=N),\mathrm{pairCoordinate}\psi (2\ast i)(2\ast i+1)R=(\psi :(i:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\to (\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})i)⟨\mathrm{insert}(2\ast i)(\mathrm{insert}(2\ast i+1)R),\mathrm{hN}⟩$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_pair_sign (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.22 (lift).

$$\forall (d:\mathbb{N})(N:\mathbb{N})(\psi :\mathrm{EuclideanSpace}\mathbb{C}\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\}),(\mathrm{lift}(\psi ):\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}d\to \mathrm{Bool}))=(\mathrm{WithLp}.\mathrm{toLp}2\mathrm{fun}(s:\mathrm{Fin}d\to \mathrm{Bool})\mapsto \mathrm{if}h:D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\mathrm{then}\psi .\mathrm{ofLp}⟨s,h⟩\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.lift (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.23 (orthonormal_countable).

$$\forall \{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E]\{\iota :\mathrm{Type}\}[\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}E]\{v:\iota \to E\},\mathrm{Orthonormal}\mathbb{C}v\to \mathrm{Countable}\iota$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.orthonormal_countable (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.24 (pairContract).

$$\forall (N:\mathbb{N})(i:\mathbb{N})(j:\mathbb{N}),(\mathrm{pairContract}(N)(i)(j):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2){\to }_L[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\})\mapsto \mathbb{C})2))=(\mathrm{partialPullCLM}(\mathrm{pairValid}Nij)(\mathrm{pairInsert}Nij)\dots (\mathrm{pairPhase}ij)\dots )$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairContract (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.25 (occupiedOrderedPairEquiv).

$$\forall (Nij:\mathbb{N})(\mathrm{hij}:i\ne j),(\mathrm{occupiedOrderedPairEquiv}Nij\mathrm{hij}:\{R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}//\mathrm{pairValid}NijR\}\equiv \{S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}//i\in S.\mathrm{val}\wedge j\in S.\mathrm{val}\})=\{\mathrm{toFun}:=\mathrm{fun}(R:\{R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}//\mathrm{pairValid}NijR\})\mapsto ⟨\mathrm{pairInsert}NijR,\dots ⟩,\mathrm{invFun}:=\mathrm{fun}(S:\{S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}//i\in S.\mathrm{val}\wedge j\in S.\mathrm{val}\})\mapsto ⟨⟨(S.\mathrm{val}.\mathrm{val}.\mathrm{erase}i).\mathrm{erase}j,\dots ⟩,\dots ⟩,{\mathrm{left}}_{\mathrm{inv}}:=\dots ,{\mathrm{right}}_{\mathrm{inv}}:=\dots \}$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.occupiedOrderedPairEquiv (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

Ordered pair insertion and removal give inverse maps on the occupied configurations. Proof fields are omitted by proof irrelevance.

Theorem 1.26 (ordered_pair_energy).

$$\forall (Nij:\mathbb{N})(\psi :\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2),(\Vert \mathrm{pairContract}Nij\psi \Vert {)}^2=(\sum ^{\prime }(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),\mathrm{if}i\ne j\wedge i\in S.\mathrm{val}\wedge j\in S.\mathrm{val}\mathrm{then}(\Vert \psi S\Vert {)}^2\mathrm{else}0)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.ordered_pair_energy (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

An ordered contraction counts exactly the configurations containing both distinct modes.

Theorem 1.27 (pairContract_apply).

$$\forall (Nij:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}),(((\mathrm{pairContract}Nij:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\})\mapsto \mathbb{C})2))\psi ):(i:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\})\to (\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\})\mapsto \mathbb{C})i)R=\mathrm{pairCoordinate}\psi ij(R:\mathrm{Finset}\mathbb{N})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairContract_apply (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.28 (pairCoordinate).

$$\forall (N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))(i:\mathbb{N})(j:\mathbb{N})(R:\mathrm{Finset}\mathbb{N}),(\mathrm{pairCoordinate}(\psi )(i)(j)(R):\mathbb{C})=(\mathrm{if}i\ne j\wedge \neg (i\in R)\wedge \neg (j\in R)\wedge (\mathrm{insert}i(\mathrm{insert}jR)).\mathrm{card}=N\mathrm{then}((-1){)}^{\{k\in R|k<j\}.\mathrm{card}+\{k\in \mathrm{insert}jR|k<i\}.\mathrm{card}}\ast (\psi :(i:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\to (\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})i)⟨\mathrm{insert}i(\mathrm{insert}jR),\dots ⟩\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairCoordinate (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.29 (pairInsert).

$$\forall (N:\mathbb{N})(i:\mathbb{N})(j:\mathbb{N})(R:\{R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}//\mathrm{pairValid}NijR\}),(\mathrm{pairInsert}(N)(i)(j)(R):\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})=(⟨\mathrm{insert}i(\mathrm{insert}j((R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}):\mathrm{Finset}\mathbb{N})),\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairInsert (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.30 (pairPhase).

$$\forall (N:\mathbb{N})(i:\mathbb{N})(j:\mathbb{N})(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}),(\mathrm{pairPhase}(i)(j)(R):\mathbb{C})=(((-1){)}^{\{k\in (R:\mathrm{Finset}\mathbb{N})|k<j\}.\mathrm{card}+\{k\in \mathrm{insert}j(R:\mathrm{Finset}\mathbb{N})|k<i\}.\mathrm{card}})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairPhase (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.31 (pairValid).

$$\forall (N:\mathbb{N})(i:\mathbb{N})(j:\mathbb{N})(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N-2\}),(\mathrm{pairValid}(N)(i)(j)(R):\mathrm{Prop})=(i\ne j\wedge \neg (i\in (R:\mathrm{Finset}\mathbb{N}))\wedge \neg (j\in (R:\mathrm{Finset}\mathbb{N}))\wedge (\mathrm{insert}i(\mathrm{insert}j(R:\mathrm{Finset}\mathbb{N}))).\mathrm{card}=N)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairValid (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.32 (partialPull).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(P:B\to \mathrm{Prop})(f:\{b:B//Pb\}\to A)(\mathrm{hf}:\mathrm{Function}.\mathrm{Injective}f)(\mathrm{phase}:B\to \mathbb{C})(\mathrm{hphase}:\forall (b:B),\Vert \mathrm{phase}b\Vert \le 1)(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2)),(\mathrm{partialPull}(P)(f)(\mathrm{hf})(\mathrm{phase})(\mathrm{hphase})(\psi ):(\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))=(⟨\mathrm{partialPullRaw}Pf\mathrm{phase}\psi ,\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPull (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.33 (partialPullCLM).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(P:B\to \mathrm{Prop})(f:\{b:B//Pb\}\to A)(\mathrm{hf}:\mathrm{Function}.\mathrm{Injective}f)(\mathrm{phase}:B\to \mathbb{C})(\mathrm{hphase}:\forall (b:B),\Vert \mathrm{phase}b\Vert \le 1),(\mathrm{partialPullCLM}(P)(f)(\mathrm{hf})(\mathrm{phase})(\mathrm{hphase}):(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2){\to }_L[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))=((\mathrm{partialPullLinear}Pf\mathrm{hf}\mathrm{phase}\mathrm{hphase}).\mathrm{mkContinuous}1\dots )$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullCLM (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.34 (partialPullLinear).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(P:B\to \mathrm{Prop})(f:\{b:B//Pb\}\to A)(\mathrm{hf}:\mathrm{Function}.\mathrm{Injective}f)(\mathrm{phase}:B\to \mathbb{C})(\mathrm{hphase}:\forall (b:B),\Vert \mathrm{phase}b\Vert \le 1),(\mathrm{partialPullLinear}(P)(f)(\mathrm{hf})(\mathrm{phase})(\mathrm{hphase}):(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2){\to }_l[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))=(\{\mathrm{toFun}:=\mathrm{partialPull}Pf\mathrm{hf}\mathrm{phase}\mathrm{hphase},{\mathrm{map}}_{\mathrm{ad}{\mathrm{d}}^{\prime }}:=\dots ,{\mathrm{map}}_{\mathrm{smu}{\mathrm{l}}^{\prime }}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullLinear (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.35 (partialPullRaw).

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(P:B\to \mathrm{Prop})(f:\{b:B//Pb\}\to A)(\mathrm{phase}:B\to \mathbb{C})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2))(b:B),(\mathrm{partialPullRaw}(P)(f)(\mathrm{phase})(\psi )(b):\mathbb{C})=(\mathrm{if}h:Pb\mathrm{then}\mathrm{phase}b\ast (\psi :(i:A)\to (\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})i)(f⟨b,h⟩)\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullRaw (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.36 (sum_pair_energies).

$$\forall (m:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m\})\mapsto \mathbb{C})2))(t:\mathrm{Finset}\mathbb{N}),\sum i\in t,(\Vert (\mathrm{pairContract}(2\ast m)(2\ast i)(2\ast i+1):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m-2\})\mapsto \mathbb{C})2))\psi \Vert {)}^2\le (m:\mathbb{R})\ast (\Vert \psi \Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.sum_pair_energies (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

Definition 1.37 (tensorBasisVector).

$$\forall (E:\mathrm{Type})(F:\mathrm{Type})[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F](\iota :\mathrm{Type})(\kappa :\mathrm{Type})(b:\mathrm{HilbertBasis}\iota \mathbb{C}E)(c:\mathrm{HilbertBasis}\kappa \mathbb{C}F)(p:\iota \times \kappa ),(\mathrm{tensorBasisVector}(b)(c)(p):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF))=((\mathrm{TensorProduct}.\mathrm{tmul}\mathbb{C}(bp.1)(cp.2):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF)))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorBasisVector (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Definition 1.38 (tensorHilbertBasis).

$$\forall (E:\mathrm{Type})(F:\mathrm{Type})[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F](\iota :\mathrm{Type})(\kappa :\mathrm{Type})(b:\mathrm{HilbertBasis}\iota \mathbb{C}E)(c:\mathrm{HilbertBasis}\kappa \mathbb{C}F)(h:\mathrm{Orthonormal}\mathbb{C}(\mathrm{tensorBasisVector}bc))(g:(\mathrm{Submodule}.\mathrm{span}\mathbb{C}(\mathrm{Set}.\mathrm{range}(\mathrm{tensorBasisVector}bc)))\perp =\mathrm{bot}),(\mathrm{tensorHilbertBasis}(b)(c):\mathrm{HilbertBasis}(\iota \times \kappa )\mathbb{C}(\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF)))=(\mathrm{HilbertBasis}.\mathrm{mkOfOrthogonalEqBot}hg)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorHilbertBasis (✓ std3).

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed defining equation retains the data fields; proof fields are omitted by proof irrelevance.

Theorem 1.39 (tensorHilbertBasis_apply).

$$\forall \{E:\mathrm{Type}\}\{F:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F]\{\iota :\mathrm{Type}\}\{\kappa :\mathrm{Type}\}(b:\mathrm{HilbertBasis}\iota \mathbb{C}E)(c:\mathrm{HilbertBasis}\kappa \mathbb{C}F)(p:\iota \times \kappa ),(\mathrm{tensorHilbertBasis}bc:\iota \times \kappa \to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF))p=\mathrm{tensorBasisVector}bcp$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorHilbertBasis_apply (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Martin Ravn Christiansen (2025). A Correlational Bound for Eigenvalues of Fermionic 2-Body Operators. URL: https://arxiv.org/abs/2505.21167v1.

Commentary.

The displayed statement is proved on the completed Hilbert or occupation carrier shown, with the written hypotheses.

References

• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.CanonicalSequence
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.adapted_hilbert_basis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.annihilationCoordinate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.canonicalRayleigh
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonVector
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonVector_pos
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.comparisonWeight
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateClaim
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename_image
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.coordinateRename_outside
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_norm_sq
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_norm_sq_summable
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.countable_pair_sign
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.denominator_sum_bound
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.lift
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.occupiedOrderedPairEquiv
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.ordered_pair_energy
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.orthonormal_countable
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairContract
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairContract_apply
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairCoordinate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairIncidence
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairInsert
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_row
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_row_bound
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairKernel_weighted_row
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairPhase
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.pairValid
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPull
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullCLM
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullLinear
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.partialPullRaw
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.sum_pair_energies
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorBasisVector
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorHilbertBasis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.tensorHilbertBasis_apply
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/OccupationHilbertContractions.weighted_schur
• Dependency: D5/S3/Observer/HilbertGeometry/HilbertPathFundamentalTheorem
• Dependency: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant
• Dependency: D5/S3/Weil/ProjectiveRayleigh/ScaledComplexQuadraticRowBound