PhysicalContractionRdmBridge

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 (AdaptedChart).

$$\mathrm{AdaptedChart}.\mathrm{mk}:\{H:\mathrm{Type}\}\to [\mathrm{NormedAddCommGroup}H]\to [\mathrm{InnerProductSpace}\mathbb{C}H]\to \{\iota :\mathrm{Type}\}\to \{e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N}\}\to \{v:\iota \times \mathrm{Fin}2\to H\}\to (\mathrm{index}:\mathrm{Set}H)\to (\mathrm{basis}:\mathrm{HilbertBasis}(\mathrm{index}:\mathrm{Type})\mathbb{C}H)\to (\mathrm{label}:\mathrm{Function}.\mathrm{Embedding}(\mathrm{index}:\mathrm{Type})\mathbb{N})\to (\mathrm{pairs}:\iota \times \mathrm{Fin}2\to (\mathrm{index}:\mathrm{Type}))\to (\forall (p:\iota \times \mathrm{Fin}2),(\mathrm{basis}:(\mathrm{index}:\mathrm{Type})\to H)(\mathrm{pairs}p)=vp)\to (\forall (i:\iota ),(\mathrm{label}:(\mathrm{index}:\mathrm{Type})\to \mathbb{N})(\mathrm{pairs}(i,0))=4\ast (e:\iota \to \mathbb{N})i)\to (\forall (i:\iota ),(\mathrm{label}:(\mathrm{index}:\mathrm{Type})\to \mathbb{N})(\mathrm{pairs}(i,1))=4\ast (e:\iota \to \mathbb{N})i+1)\to \mathrm{AdaptedChart}ev$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.AdaptedChart (✓ 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.2 (single_pair_composition).

$$\forall (nij:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+2\})\mapsto \mathbb{C})2)),(\mathrm{countableAnnihilate}nj:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))((\mathrm{countableAnnihilate}(n+1)i:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1+1\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2))\psi )=(\mathrm{pairContract}(n+2)ij:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+2\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+2-2\})\mapsto \mathbb{C})2))\psi$$

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

$$\forall (n:\mathbb{N})(i:\mathbb{N}),(\mathrm{countableAnnihilate}(n)(i):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2){\to }_L[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))=(\mathrm{partialPullCLM}(\mathrm{fun}(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \neg (i\in R.\mathrm{val}))(\mathrm{fun}(R:\{R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\}//\neg (i\in R.\mathrm{val})\})\mapsto (⟨\mathrm{insert}iR.\mathrm{val}.\mathrm{val},\dots ⟩:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\}))\dots (\mathrm{fun}(R:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto ((-1:\mathbb{C}){)}^{R.\mathrm{val}.\mathrm{filter}(\mathrm{fun}(k:\mathbb{N})\mapsto k<i).\mathrm{card}})\dots )$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.countableAnnihilate (✓ 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.4 (tensorSlice_apply).

$$\forall (ni:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2))(t:\mathrm{Fin}n\to \mathbb{N}),(((\mathrm{tensorSlice}ni:(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathbb{C})2))\psi ):(i:\mathrm{Fin}n\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathbb{C})i)t=(\psi :(i:\mathrm{Fin}(n+1)\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})i)(\mathrm{Fin}.\mathrm{cons}it)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice_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.5 (tensorSlice_antisymmetric).

$$\forall (ni:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2)),\mathrm{IsAntisymmetric}(n+1)\psi \to \mathrm{IsAntisymmetric}n((\mathrm{tensorSlice}ni:(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathbb{C})2))\psi )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice_antisymmetric (✓ 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 (tensorSlice).

$$\forall (n:\mathbb{N})(i:\mathbb{N}),(\mathrm{tensorSlice}(n)(i):(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2){\to }_L[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathbb{C})2))=(\mathrm{partialPullCLM}(\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathrm{True})(\mathrm{fun}(t:{\{}_{:}\mathrm{Fin}n\to \mathbb{N}//\mathrm{True}\})\mapsto \mathrm{Fin}.\mathrm{cons}i(t:\mathrm{Fin}n\to \mathbb{N}))\dots (\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto 1)\dots )$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice (✓ 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.7 (slaterBasis_apply).

$$\forall (n:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\}),(\mathrm{slaterHilbertBasis}n:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\}\to (\mathrm{antisymmetricSubmodule}n))S=\mathrm{slaterAntiVector}nS$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.slaterBasis_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.8 (antiHead_intertwining).

$$\forall (ni:\mathbb{N})(\psi :(\mathrm{antisymmetricSubmodule}(n+1))),((\mathrm{slaterHilbertBasis}n).\mathrm{repr}:(\mathrm{antisymmetricSubmodule}n)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))((\mathrm{antiHead}ni:(\mathrm{antisymmetricSubmodule}(n+1))\to (\mathrm{antisymmetricSubmodule}n))\psi )=(\mathrm{countableAnnihilate}ni:(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))(((\mathrm{slaterHilbertBasis}(n+1)).\mathrm{repr}:(\mathrm{antisymmetricSubmodule}(n+1))\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2))\psi )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.antiHead_intertwining (✓ 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.9 (antiHead).

$$\forall (n:\mathbb{N})(i:\mathbb{N}),(\mathrm{antiHead}(n)(i):(\mathrm{antisymmetricSubmodule}(n+1)){\to }_L[\mathbb{C}](\mathrm{antisymmetricSubmodule}n))=(\mathrm{let}{x}_{x_{\mathrm{LinearMap}}}:=\{\mathrm{toFun}:=\mathrm{fun}(\psi :(\mathrm{antisymmetricSubmodule}(n+1)))\mapsto ⟨(\mathrm{Real}.\mathrm{sqrt}((n:\mathbb{R})+1):\mathbb{C})\cdot (\mathrm{tensorSlice}ni:(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}n\to \mathbb{N})\mapsto \mathbb{C})2))(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2)),\dots ⟩,{\mathrm{map}}_{\mathrm{ad}{\mathrm{d}}^{\prime }}:=\dots ,{\mathrm{map}}_{\mathrm{smu}{\mathrm{l}}^{\prime }}:=\dots \};\{\mathrm{toLinearMap}:=x_{x_{\mathrm{LinearMap}}},\mathrm{cont}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.antiHead (✓ 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.10 (adaptedChart).

$$\forall (H:\mathrm{Type})[\mathrm{NormedAddCommGroup}H][\mathrm{InnerProductSpace}\mathbb{C}H][\mathrm{CompleteSpace}H][\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}H](\iota :\mathrm{Type})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(v:\iota \times \mathrm{Fin}2\to H)(\mathrm{hv}:\mathrm{Orthonormal}\mathbb{C}v)(h:\mathrm{Nonempty}(\mathrm{AdaptedChart}ev)),(\mathrm{adaptedChart}(e)(v)(\mathrm{hv}):\mathrm{AdaptedChart}ev)=(\mathrm{Classical}.\mathrm{choice}h)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.adaptedChart (✓ 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.11 (canonicalPair_countable).

$$\forall \{H:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}H][\mathrm{InnerProductSpace}\mathbb{C}H][\mathrm{CompleteSpace}H][\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}H]\{\iota :\mathrm{Type}\}(v:\iota \times \mathrm{Fin}2\to H),\mathrm{Orthonormal}\mathbb{C}v\to \mathrm{Countable}\iota$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.canonicalPair_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.12 (particleAntiEmbedding).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(N:\mathbb{N}),(\mathrm{particleAntiEmbedding}(X)(b)(e)(N):(\mathrm{particleExterior}XbeN){\to }_{li}[\mathbb{C}](\mathrm{antisymmetricSubmodule}N))=(\{\mathrm{toFun}:=\mathrm{fun}(\psi :(\mathrm{particleExterior}XbeN))\mapsto ⟨(\mathrm{particleCoordinates}XbeN:(\mathrm{particleObject}XN).\mathrm{carrier}\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2))(\psi :(\mathrm{particleObject}XN).\mathrm{carrier}),\dots ⟩,{\mathrm{map}}_{\mathrm{ad}{\mathrm{d}}^{\prime }}:=\dots ,{\mathrm{map}}_{\mathrm{smu}{\mathrm{l}}^{\prime }}:=\dots ,{\mathrm{norm}}_{\mathrm{ma}{\mathrm{p}}^{\prime }}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleAntiEmbedding (✓ 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.13 (particleBasis).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier}),\mathrm{particleBasis}Xb0=\mathrm{HilbertBasis}.\mathrm{ofRepr}(\mathrm{coordinateEquiv}(\mathrm{Equiv}.\mathrm{ofUnique}(\mathrm{Fin}0\to X.\mathrm{carrier})(\mathrm{Fin}0\to \iota )))\wedge (\forall (n:\mathbb{N}),\mathrm{particleBasis}Xb(n+1)=\mathrm{tensorTowerTupleBasis}Xbn)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleBasis (✓ 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 (particleCoordinates).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N}),\mathrm{particleCoordinates}Xbe0=(\mathrm{coordinateRename}(\mathrm{Function}.\mathrm{Embedding}.\mathrm{arrowCongrRight}(\gamma :=\mathrm{Fin}0)e)).\mathrm{comp}(\mathrm{particleBasis}Xb0).\mathrm{repr}.\mathrm{toLinearIsometry}\wedge (\forall (n:\mathbb{N}),\mathrm{particleCoordinates}Xbe(n+1)=\mathrm{sourceTensorCoordinates}Xben)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleCoordinates (✓ 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 zero branch gives vacuum coordinates; the positive branch uses sourceTensorCoordinates.

Definition 1.15 (particleExterior).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N}),\mathrm{particleExterior}Xbe0=\mathrm{top}\wedge (\forall (n:\mathbb{N}),\mathrm{particleExterior}Xbe(n+1)=\mathrm{sourceExterior}Xben)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleExterior (✓ 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 zero-particle sector is the scalar vacuum. Every positive-particle sector uses the literal physical exterior definition sourceExterior.

Definition 1.16 (particleHead).

$$\forall (X:\mathrm{HilbertObject})(f:X.\mathrm{carrier})(n:\mathbb{N}),(\mathrm{particleHead}(X)(f)(n):(\mathrm{particleObject}X(n+1)).\mathrm{carrier}{\to }_L[\mathbb{C}](\mathrm{particleObject}Xn).\mathrm{carrier})=(\mathrm{match}n\mathrm{with}|0\mapsto (\mathrm{lp}.\mathrm{singleContinuousLinearMap}\mathbb{C}(\mathrm{fun}{(}_{:}\mathrm{Fin}0\to X.\mathrm{carrier})\mapsto \mathbb{C})2\mathrm{fun}(k:\mathrm{Fin}0)\mapsto k.elim0){\circ }_{\mathrm{SL}}(\mathrm{innerSL}\mathbb{C}:(\mathrm{particleObject}X(0+1)).\mathrm{carrier}\to (\mathrm{particleObject}X(0+1)).\mathrm{carrier}{\to }_L[\mathbb{C}]\mathbb{C})f|n.\mathrm{succ}\mapsto \mathrm{tensorHead}f)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleHead (✓ 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.17 (particleObject).

$$\forall (X:\mathrm{HilbertObject}),\mathrm{particleObject}X0=\mathrm{vacuumObject}X\wedge (\forall (n:\mathbb{N}),\mathrm{particleObject}X(n+1)=\mathrm{tensorTower}Xn)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleObject (✓ 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.18 (particleOccupation).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(N:\mathbb{N}),(\mathrm{particleOccupation}(X)(b)(e)(N):(\mathrm{particleExterior}XbeN){\to }_{li}[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})\mapsto \mathbb{C})2))=((\mathrm{slaterHilbertBasis}N).\mathrm{repr}.\mathrm{toLinearIsometry}.\mathrm{comp}(\mathrm{particleAntiEmbedding}XbeN))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleOccupation (✓ 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.19 (sourceAnnihilate).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(f:X.\mathrm{carrier}),(\mathrm{sourceAnnihilate}(X)(b)(e)(n)(f):(\mathrm{particleExterior}Xbe(n+1)){\to }_L[\mathbb{C}](\mathrm{particleExterior}Xben))=(\mathrm{let}{x}_{x_{\mathrm{LinearMap}}}:=\{\mathrm{toFun}:=\mathrm{fun}(\psi :(\mathrm{particleExterior}Xbe(n+1)))\mapsto ⟨(\mathrm{Real}.\mathrm{sqrt}((n:\mathbb{R})+1):\mathbb{C})\cdot (\mathrm{particleHead}Xfn:(\mathrm{particleObject}X(n+1)).\mathrm{carrier}\to (\mathrm{particleObject}Xn).\mathrm{carrier})(\psi :(\mathrm{particleObject}X(n+1)).\mathrm{carrier}),\dots ⟩,{\mathrm{map}}_{\mathrm{ad}{\mathrm{d}}^{\prime }}:=\dots ,{\mathrm{map}}_{\mathrm{smu}{\mathrm{l}}^{\prime }}:=\dots \};\{\mathrm{toLinearMap}:=x_{x_{\mathrm{LinearMap}}},\mathrm{cont}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceAnnihilate (✓ 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 fermionic annihilator at an arbitrary one-particle vector f contracts the first tensor factor against f, with the physical square-root particle-number normalization.

Definition 1.20 (sourceCreate).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(f:X.\mathrm{carrier}),(\mathrm{sourceCreate}(X)(b)(e)(n)(f):(\mathrm{particleExterior}Xben){\to }_L[\mathbb{C}](\mathrm{particleExterior}Xbe(n+1)))=((\mathrm{ContinuousLinearMap}.\mathrm{adjoint}:((\mathrm{particleExterior}Xbe(n+1)){\to }_L[\mathbb{C}](\mathrm{particleExterior}Xben))\to (\mathrm{particleExterior}Xben){\to }_L[\mathbb{C}](\mathrm{particleExterior}Xbe(n+1)))(\mathrm{sourceAnnihilate}Xbenf))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceCreate (✓ 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 fermionic creation operator at f is the Hilbert adjoint of sourceAnnihilate at f.

Definition 1.21 (sourceGamma).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(\psi :(\mathrm{particleExterior}Xbe(n+2)))(h:\exists \Gamma :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}){\to }_L[\mathbb{C}]\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}),\forall (f_1{f}_2{g}_1{g}_2:X.\mathrm{carrier}),\mathrm{inner}\mathbb{C}((\mathrm{TensorProduct}.\mathrm{tmul}\mathbb{C}{f}_1{f}_2:\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))(\Gamma ((\mathrm{TensorProduct}.\mathrm{tmul}\mathbb{C}{g}_1{g}_2:\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})))=\mathrm{inner}\mathbb{C}\psi (\mathrm{sourceCreate}Xbe(n+1)g_1(\mathrm{sourceCreate}Xben{g}_2(\mathrm{sourceAnnihilate}Xben{f}_2(\mathrm{sourceAnnihilate}Xbe(n+1)f_1\psi ))))),(\mathrm{sourceGamma}(X)(b)(e)(n)(\psi ):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}){\to }_L[\mathbb{C}]\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))=(\mathrm{Classical}.\mathrm{choose}h)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceGamma (✓ std3).

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

Commentary.

Christiansen, Section 1, p. 1, equation (1.1): “Given a normalized state Ψ ∈ ⋀ᴺ𝔥 we define the 2-body operator associated to Ψ, γ₂^Ψ : 𝔥 ⊗ 𝔥 → 𝔥 ⊗ 𝔥, by ⟨φ₁ ⊗ φ₂, γ₂^Ψ(ψ₁ ⊗ ψ₂)⟩ = ⟨Ψ, c*(ψ₁)c*(ψ₂)c(φ₂)c(φ₁)Ψ⟩ for any φ₁, φ₂, ψ₁, ψ₂ ∈ 𝔥, where c*(·) and c(·) denote the fermionic creation and annihilation operators.” The bounded operator is selected from the operators satisfying this arbitrary-vector kernel equation. The private Gram construction proves existence and uniqueness and transports this operator on the result’s live Rayleigh path. Annihilation is defined at every one-particle vector; creation is its Hilbert adjoint. Source tensor and particle carriers are actual completed Hilbert tensor powers, and the basis trace normalization is proved in sourceGamma_trace.

Theorem 1.22 (sourceGamma_trace).

$$\forall \{\iota :\mathrm{Type}\}(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(\psi :(\mathrm{particleExterior}Xbe(n+2))),\sum ^{\prime }(p:\iota \times \iota ),(\mathrm{inner}\mathbb{C}((\mathrm{tensorHilbertBasis}bb:\iota \times \iota \to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))p)((\mathrm{sourceGamma}Xben\psi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})\to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))((\mathrm{tensorHilbertBasis}bb:\iota \times \iota \to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))p))).\mathrm{re}=(((n+2)\ast (n+1)):\mathbb{R})\ast (\Vert \psi \Vert {)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceGamma_trace (✓ 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 physical two-body Gram operator has trace N(N−1) for a unit vector, with N = n+2. The displayed basis trace is an absolutely summable series, rather than a formal finite-dimensional trace.

Definition 1.23 (sourceRayleigh).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(\psi :(\mathrm{particleExterior}Xbe(n+2)))(\phi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})),(\mathrm{sourceRayleigh}(X)(b)(e)(n)(\psi )(\phi ):\mathbb{R})=((\mathrm{inner}\mathbb{C}\phi ((\mathrm{sourceGamma}Xben\psi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})\to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier}))\phi )).\mathrm{re})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceRayleigh (✓ 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.24 (sourceRayleigh_transport).

$$\forall \{\iota :\mathrm{Type}\}(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(\psi :(\mathrm{particleExterior}Xbe(n+2)))(\phi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})),\mathrm{sourceRayleigh}Xben\psi \phi =\mathrm{completedRayleigh}(n+2)((\mathrm{particleOccupation}Xbe(n+2):(\mathrm{particleExterior}Xbe(n+2))\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+2\})\mapsto \mathbb{C})2))\psi )((\mathrm{tensorCoordinateEmbedding}be:\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}X.\mathrm{carrier})\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathbb{N}\times \mathbb{N})\mapsto \mathbb{C})2))\phi )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceRayleigh_transport (✓ 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.25 (source_single_intertwining).

$$\forall \{\iota :\mathrm{Type}\}(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N})(i:\iota )(\psi :(\mathrm{particleExterior}Xbe(n+1))),(\mathrm{particleOccupation}Xben:(\mathrm{particleExterior}Xben)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))((\mathrm{sourceAnnihilate}Xben((b:\iota \to X.\mathrm{carrier})i):(\mathrm{particleExterior}Xbe(n+1))\to (\mathrm{particleExterior}Xben))\psi )=(\mathrm{countableAnnihilate}n((e:\iota \to \mathbb{N})i):(\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n\})\mapsto \mathbb{C})2))((\mathrm{particleOccupation}Xbe(n+1):(\mathrm{particleExterior}Xbe(n+1))\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=n+1\})\mapsto \mathbb{C})2))\psi )$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.source_single_intertwining (✓ 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.26 (vacuumObject).

$$\forall (X:\mathrm{HilbertObject}),(\mathrm{vacuumObject}(X):\mathrm{HilbertObject})=(\{\mathrm{carrier}:=(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}0\to X.\mathrm{carrier})\mapsto \mathbb{C})2),\mathrm{normed}:=\mathrm{inferInstance},\mathrm{innerProduct}:=\mathrm{inferInstance},\mathrm{complete}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.vacuumObject (✓ 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/PhysicalContractionRdmBridge.AdaptedChart
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.adaptedChart
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.antiHead
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.antiHead_intertwining
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.canonicalPair_countable
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.countableAnnihilate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleAntiEmbedding
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleBasis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleCoordinates
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleExterior
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleHead
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleObject
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.particleOccupation
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.single_pair_composition
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.slaterBasis_apply
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceAnnihilate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceCreate
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceGamma
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceGamma_trace
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceRayleigh
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.sourceRayleigh_transport
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.source_single_intertwining
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice_antisymmetric
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.tensorSlice_apply
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge.vacuumObject
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry