CompletedCorrelationalBound

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.

Theorem 1.1 (standardK_real).

$$\forall \{Ls:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(xy:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),((\mathrm{standardB}\mathrm{coeff}).\mathrm{conjTranspose}\ast \mathrm{standardB}\mathrm{coeff})xy=((\mathrm{realK}\mathrm{coeff}xy):\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.standardK_real (✓ 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.2 (standardB_sector_support).

$$\forall \{LsN:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(\psi :\mathrm{EuclideanSpace}\mathbb{C}\{s_1:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}{s}_1=N\})(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}x\ne N-2\to (((\mathrm{Matrix}.\mathrm{toEuclideanLin}:\mathrm{Matrix}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\mathbb{C}\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}){\to }_l[\mathbb{C}]\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(\mathrm{standardB}\mathrm{coeff}):\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(\mathrm{lift}\psi )).\mathrm{ofLp}x=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.standardB_sector_support (✓ 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.3 (realK_symm).

$$\forall \{Ls:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(xy:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),\mathrm{realK}\mathrm{coeff}xy=\mathrm{realK}\mathrm{coeff}yx$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_symm (✓ 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.4 (realK_row).

$$\forall \{Ls:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(f:(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\to \mathbb{R})(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),\sum y:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool},\mathrm{realK}\mathrm{coeff}xy\ast fy=\sum i:\mathrm{Fin}L,\mathrm{if}\mathrm{pairFull}ix\mathrm{then}\mathrm{coeff}i\ast \sum j:\mathrm{Fin}L,\mathrm{if}\mathrm{pairEmpty}j(\mathrm{removePair}ix)\mathrm{then}\mathrm{coeff}j\ast f(\mathrm{addPair}j(\mathrm{removePair}ix))\mathrm{else}0\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_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.

Theorem 1.5 (realK_nonneg).

$$\forall \{Ls:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R}),(\forall (i:\mathrm{Fin}L),0\le \mathrm{coeff}i)\to \forall (xy:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),0\le \mathrm{realK}\mathrm{coeff}xy$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_nonneg (✓ 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 (realK).

$$\forall (L:\mathbb{N})(s:\mathbb{N})(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})(y:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),(\mathrm{realK}(\mathrm{coeff})(x)(y):\mathbb{R})=(\mathrm{dotProduct}(\mathrm{fun}(z:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\mapsto \mathrm{realB}\mathrm{coeff}zx)(\mathrm{fun}(z:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\mapsto \mathrm{realB}\mathrm{coeff}zy))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK (✓ 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 (realB).

$$\forall (L:\mathbb{N})(s:\mathbb{N})(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R})(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})(y:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}),(\mathrm{realB}(\mathrm{coeff})(x)(y):\mathbb{R})=(\sum i:\mathrm{Fin}L,\mathrm{if}\mathrm{pairTransition}ixy\mathrm{then}\mathrm{coeff}i\mathrm{else}0)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realB (✓ 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.8 (occupiedModes).

$$\forall (d:\mathbb{N})(x:\mathrm{Fin}d\to \mathrm{Bool}),(\mathrm{occupiedModes}(x):\mathrm{Finset}(\mathrm{Fin}d))=(\{i:\mathrm{Fin}d|xi=\mathrm{true}\})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupiedModes (✓ 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.9 (doublePairs_sector).

$$\forall \{Lsm:\mathbb{N}\}(x:\{s_1:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}{s}_1=2\ast m\}),(\mathrm{doublePairs}(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})).\mathrm{card}\le m$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.doublePairs_sector (✓ 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.10 (actual_sector_bound).

$$\forall \{Ls:\mathbb{N}\}(\mathrm{coeff}:\mathrm{Fin}L\to \mathbb{R}),(\forall (i:\mathrm{Fin}L),0\le \mathrm{coeff}i)\to \forall (m:\mathbb{N}),1\le m\to \forall (\alpha :\mathbb{R}),0\le \alpha \to (\forall (i:\mathrm{Fin}L),(\mathrm{coeff}i{)}^2\le \alpha )\to (\sum i:\mathrm{Fin}L,(\mathrm{coeff}i{)}^2)\le 1\to 2\ast (m:\mathbb{R})\ast \alpha \le 1\to \forall (\psi :\mathrm{EuclideanSpace}\mathbb{C}\{s_1:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}{s}_1=2\ast m\}),(\Vert ((\mathrm{Matrix}.\mathrm{toEuclideanLin}:\mathrm{Matrix}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\mathbb{C}\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}){\to }_l[\mathbb{C}]\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(\mathrm{standardB}\mathrm{coeff}):\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(\mathrm{lift}\psi )\Vert {)}^2\le ((m:\mathbb{R})-(m:\mathbb{R})\ast ((m:\mathbb{R})-1)\ast (\sum i:\mathrm{Fin}L,(\mathrm{coeff}i{)}^4)+5/2\ast ((m:\mathbb{R}){)}^3\ast (\alpha {)}^2)\ast (\Vert \mathrm{lift}\psi \Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.actual_sector_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.

Definition 1.11 (completedClaim).

$$(\mathrm{completedClaim}:\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{completedRayleigh}(2\ast m)\psi (\mathrm{canonicalTensor}c)\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/CompletedCorrelationalBound.completedClaim (✓ 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 (completed_result).

$$\mathrm{completedClaim}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.completed_result (✓ 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 (countableBLinear).

$$\forall (\mathrm{coeff}:\mathbb{N}\to \mathbb{R})(\mathrm{hq}:\mathrm{Summable}\mathrm{fun}(i:\mathbb{N})\mapsto (\mathrm{coeff}i{)}^2)(m:\mathbb{N}),(\mathrm{countableBLinear}(\mathrm{coeff})(\mathrm{hq})(m):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m\})\mapsto \mathbb{C})2){\to }_l[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=2\ast m-2\})\mapsto \mathbb{C})2))=(\{\mathrm{toFun}:=\mathrm{countableB}\mathrm{coeff}m,{\mathrm{map}}_{\mathrm{ad}{\mathrm{d}}^{\prime }}:=\dots ,{\mathrm{map}}_{\mathrm{smu}{\mathrm{l}}^{\prime }}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.countableBLinear (✓ 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.14 (countable_finite_corrected_bound).

$$\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))(L:\mathbb{N}),(\Vert \mathrm{countableBL}c.\mathrm{coeff}mL\psi \Vert {)}^2\le ((m:\mathbb{R})-(m:\mathbb{R})\ast ((m:\mathbb{R})-1)\ast (\sum i\in \mathrm{Finset}.\mathrm{range}L,(c.\mathrm{coeff}i{)}^4)+5/2\ast ((m:\mathbb{R}){)}^3\ast (\alpha {)}^2)\ast (\Vert \psi \Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.countable_finite_corrected_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.

Definition 1.15 (finiteEmbed).

$$\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{finiteEmbed}(\psi ):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))=((\mathrm{coordinateRename}\{\mathrm{toFun}:=\mathrm{finiteOccupation},\mathrm{in}{\mathrm{j}}^{\prime }:=\dots \}:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))((({\mathrm{lpPiLp}}_{li}(\mathrm{fun}{(}_{:}\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})\mapsto \mathbb{C})\mathbb{C}).\mathrm{symm}:(\mathrm{PiLp}2\mathrm{fun}{(}_{:}\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})\mapsto \mathbb{C})\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})\mapsto \mathbb{C})2))\psi ))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed (✓ 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.16 (finiteEmbed_apply).

$$\forall \{dN:\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\})(x:\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\}),((\mathrm{finiteEmbed}\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{finiteOccupation}x)=\psi .\mathrm{ofLp}x$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_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.

Theorem 1.17 (finiteEmbed_norm).

$$\forall \{dN:\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\}),\Vert \mathrm{finiteEmbed}\psi \Vert =\Vert \psi \Vert$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_norm (✓ 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 (finiteEmbed_outside).

$$\forall \{dN:\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\})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),\neg \mathrm{modesBelow}dS\to ((\mathrm{finiteEmbed}\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)S=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_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 (finiteEmbedding_dense).

$$\forall (N:\mathbb{N})(\psi :\mathrm{lp}({\mathrm{fun}}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}\mapsto \mathbb{C})2),\mathrm{Filter}.\mathrm{Tendsto}(\mathrm{fun}(d:\mathbb{N})\mapsto \mathrm{finiteEmbed}(d:=d)(N:=N)(\mathrm{finiteRestrict}(d:=d)(N:=N)\psi ))\mathrm{Filter}.\mathrm{atTop}(\mathrm{nhds}\psi )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbedding_dense (✓ 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.20 (finiteOccupation).

$$\forall (d:\mathbb{N})(N:\mathbb{N})(x:\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\}),(\mathrm{finiteOccupation}(x):\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})=(⟨\mathrm{occupationSet}(x:\mathrm{Fin}d\to \mathrm{Bool}),\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteOccupation (✓ 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.21 (finiteOccupation_sectorOfCountable).

$$\forall (dN:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})(\mathrm{hS}:\mathrm{modesBelow}dS),\mathrm{finiteOccupation}(\mathrm{sectorOfCountable}dNS\mathrm{hS})=S$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteOccupation_sectorOfCountable (✓ 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 (finiteRestrict).

$$\forall (d:\mathbb{N})(N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2)),(\mathrm{finiteRestrict}(\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{WithLp}.\mathrm{toLp}2\mathrm{fun}(x:\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})\mapsto (\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{finiteOccupation}x))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteRestrict (✓ 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 (finite_pair_coordinate).

$$\forall \{LsN:\mathbb{N}\}(i:\mathrm{Fin}L)(\psi :\mathrm{EuclideanSpace}\mathbb{C}\{s_1:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}{s}_1=N\})(x:\{s_1:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}{s}_1=N-2\}),\mathrm{pairCoordinate}(\mathrm{finiteEmbed}\psi )(2\ast (i:\mathbb{N}))(2\ast (i:\mathbb{N})+1)((\mathrm{finiteOccupation}x):\mathrm{Finset}\mathbb{N})=(((\mathrm{Matrix}.\mathrm{toEuclideanLin}:\mathrm{Matrix}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\mathbb{C}\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}){\to }_l[\mathbb{C}]\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(D5.S3.\mathrm{Quantum}.\mathrm{SpinChains}.\mathrm{SupersymmetricFermion}.\mathrm{JordanWigner}.\mathrm{fullC}(\mathrm{downMode}i)\ast D5.S3.\mathrm{Quantum}.\mathrm{SpinChains}.\mathrm{SupersymmetricFermion}.\mathrm{JordanWigner}.\mathrm{fullC}(\mathrm{upMode}i)):\mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})\to \mathrm{EuclideanSpace}\mathbb{C}(\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool}))(\mathrm{lift}\psi )).\mathrm{ofLp}(x:\mathrm{Fin}(2\ast L+s)\to \mathrm{Bool})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finite_pair_coordinate (✓ 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 (modesBelow).

$$\forall (N:\mathbb{N})(d:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),(\mathrm{modesBelow}(d)(S):\mathrm{Prop})=(\forall n\in (S:\mathrm{Finset}\mathbb{N}),n<d)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.modesBelow (✓ 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 (occupationOfSet).

$$\forall (d:\mathbb{N})(S:\mathrm{Finset}\mathbb{N})(\mathrm{aAnon}:\mathrm{Fin}d),(\mathrm{occupationOfSet}(d)(S)(\mathrm{aAnon}):\mathrm{Bool})=(\mathrm{decide}((\mathrm{aAnon}:\mathbb{N})\in S))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupationOfSet (✓ 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.26 (occupationSet).

$$\forall (d:\mathbb{N})(x:\mathrm{Fin}d\to \mathrm{Bool}),(\mathrm{occupationSet}(x):\mathrm{Finset}\mathbb{N})=(\mathrm{Finset}.\mathrm{map}\{\mathrm{toFun}:=\mathrm{Fin}.\mathrm{val},\mathrm{in}{\mathrm{j}}^{\prime }:=\dots \}(\mathrm{occupiedModes}x))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupationSet (✓ 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.27 (sectorOfCountable).

$$\forall (d:\mathbb{N})(N:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})(\mathrm{hS}:\mathrm{modesBelow}dS),(\mathrm{sectorOfCountable}(d)(N)(S)(\mathrm{hS}):\{s:\mathrm{Fin}d\to \mathrm{Bool}//D5.S3.\mathrm{Quantum}.\mathrm{FockSpace}.\mathrm{ForbiddenNeighbourDeterminant}.\mathrm{occupationCount}s=N\})=(⟨\mathrm{occupationOfSet}d(S:\mathrm{Finset}\mathbb{N}),\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.sectorOfCountable (✓ 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.

References

• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.actual_sector_bound
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.completedClaim
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.completed_result
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.countableBLinear
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.countable_finite_corrected_bound
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.doublePairs_sector
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_apply
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_norm
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbed_outside
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteEmbedding_dense
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteOccupation
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteOccupation_sectorOfCountable
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finiteRestrict
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.finite_pair_coordinate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.modesBelow
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupationOfSet
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupationSet
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.occupiedModes
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realB
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_nonneg
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_row
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.realK_symm
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.sectorOfCountable
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.standardB_sector_support
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound.standardK_real
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/CanonicalRdmAndPadding