CompletedTensorSlaterGeometry

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

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

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

Definition 1.2 (HilbertObject).

$$\mathrm{HilbertObject}.\mathrm{mk}:(\mathrm{carrier}:\mathrm{Type})\to \mathrm{NormedAddCommGroup}\mathrm{carrier}\to \mathrm{InnerProductSpace}\mathbb{C}\mathrm{carrier}\to \mathrm{CompleteSpace}\mathrm{carrier}\to \mathrm{HilbertObject}$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.HilbertObject (✓ 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.3 (IsAntisymmetric).

$$\forall (N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2)),(\mathrm{IsAntisymmetric}(N)(\psi ):\mathrm{Prop})=(\forall (t:\mathrm{Fin}N\to \mathbb{N})(\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}N)),(\psi :(i:\mathrm{Fin}N\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})i)(t\circ (\sigma :\mathrm{Fin}N\to \mathrm{Fin}N))=\mathrm{permutationPhase}N\sigma \ast (\psi :(i:\mathrm{Fin}N\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})i)t)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.IsAntisymmetric (✓ 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.4 (TensorTowerIndex).

$$\forall (\iota :\mathrm{Type}),\mathrm{TensorTowerIndex}\iota 0=\iota \wedge (\forall (n:\mathbb{N}),\mathrm{TensorTowerIndex}\iota (n+1)=\iota \times \mathrm{TensorTowerIndex}\iota n)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.TensorTowerIndex (✓ 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.5 (antisymmetricComplete).

$$\forall (N:\mathbb{N}),\mathrm{CompleteSpace}(\mathrm{antisymmetricSubmodule}N)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricComplete (✓ 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.6 (antisymmetricSubmodule).

$$\forall (N:\mathbb{N}),(\mathrm{antisymmetricSubmodule}(N):\mathrm{Submodule}\mathbb{C}(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2))=(\{\mathrm{carrier}:=\{\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2)|\mathrm{IsAntisymmetric}N\psi \},{\mathrm{add}}_{\mathrm{me}{\mathrm{m}}^{\prime }}:=\dots ,{\mathrm{zero}}_{\mathrm{me}{\mathrm{m}}^{\prime }}:=\dots ,{\mathrm{smul}}_{\mathrm{me}{\mathrm{m}}^{\prime }}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricSubmodule (✓ 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 (antisymmetricSubmodule_closed).

$$\forall (N:\mathbb{N}),\mathrm{IsClosed}((\mathrm{antisymmetricSubmodule}N):\mathrm{Set}(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricSubmodule_closed (✓ 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 (antisymmetric_orthogonal_slaters_zero).

$$\forall (N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2)),\mathrm{IsAntisymmetric}N\psi \to (\forall (S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),\mathrm{inner}\mathbb{C}(\mathrm{slaterVector}NS)\psi =0)\to \psi =0$$

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

$$\forall (N:\mathbb{N})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2)),\mathrm{IsAntisymmetric}N\psi \to \forall (t:\mathrm{Fin}N\to \mathbb{N}),\neg \mathrm{Function}.\mathrm{Injective}t\to (\psi :(i:\mathrm{Fin}N\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})i)t=0$$

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

$$\forall (A:\mathrm{Type})(B:\mathrm{Type})(e:A\equiv B),(\mathrm{coordinateEquiv}(e):(\mathrm{lp}(\mathrm{fun}{(}_{:}A)\mapsto \mathbb{C})2){\equiv }_{li}[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}B)\mapsto \mathbb{C})2))=(\mathrm{LinearIsometryEquiv}.\mathrm{ofSurjective}(\mathrm{coordinateRename}e.\mathrm{toEmbedding})\dots )$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.coordinateEquiv (✓ 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 (extendedCoeff_moment).

$$\forall \{\iota :\mathrm{Type}\}(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(c:\mathrm{CanonicalFamily}\iota )(k:\mathbb{N}),0<k\to \sum ^{\prime }(j:\mathbb{N}),(\mathrm{Function}.\mathrm{extend}(e:\iota \to \mathbb{N})c.\mathrm{coeff}(\mathrm{fun}{(}_{:}\mathbb{N})\mapsto 0)j{)}^k=\sum ^{\prime }(i:\iota ),(c.\mathrm{coeff}i{)}^k$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.extendedCoeff_moment (✓ 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 (familyCoefficients).

$$\forall (\iota :\mathrm{Type})(c:\mathrm{CanonicalFamily}\iota ),(\mathrm{familyCoefficients}(c):(\mathrm{lp}(\mathrm{fun}{(}_{:}\iota )\mapsto \mathbb{C})2))=(⟨\mathrm{fun}(i:\iota )\mapsto ((c.\mathrm{coeff}i):\mathbb{C}),\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familyCoefficients (✓ 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 (familySequence).

$$\forall (\iota :\mathrm{Type})(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(c:\mathrm{CanonicalFamily}\iota ),(\mathrm{familySequence}(e)(c):\mathrm{CanonicalSequence})=(\{\mathrm{coeff}:=\mathrm{Function}.\mathrm{extend}(e:\iota \to \mathbb{N})c.\mathrm{coeff}\mathrm{fun}{(}_{:}\mathbb{N})\mapsto 0,\mathrm{nonneg}:=\dots ,{\mathrm{summable}}_{\mathrm{sq}}:=\dots ,\mathrm{mass}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familySequence (✓ 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 (familySequence_cap).

$$\forall \{\iota :\mathrm{Type}\}(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(c:\mathrm{CanonicalFamily}\iota )(\alpha :\mathbb{R}),0\le \alpha \to (\forall (i:\iota ),(c.\mathrm{coeff}i{)}^2\le \alpha )\to \forall (j:\mathbb{N}),((\mathrm{familySequence}ec).\mathrm{coeff}j{)}^2\le \alpha$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familySequence_cap (✓ 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 (occupationTuple).

$$\forall (N:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})(\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}N))(\mathrm{aAnon}:\mathrm{Fin}N),(\mathrm{occupationTuple}(N)(S)(\sigma )(\mathrm{aAnon}):\mathbb{N})=(((S:\mathrm{Finset}\mathbb{N}).\mathrm{orderEmbOfFin}\dots :\mathrm{Fin}N\to \mathbb{N})((\sigma :\mathrm{Fin}N\to \mathrm{Fin}N)\mathrm{aAnon}))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.occupationTuple (✓ 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 (permutationPhase).

$$\forall (N:\mathbb{N})(\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}N)),(\mathrm{permutationPhase}(N)(\sigma ):\mathbb{C})=(((((\mathrm{Equiv}.\mathrm{Perm}.\mathrm{sign}:\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}N)\to \mathrm{Units}\mathbb{Z})\sigma ):\mathbb{Z}):\mathbb{C}))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.permutationPhase (✓ 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 (slaterAntiVector).

$$\forall (N:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),(\mathrm{slaterAntiVector}(N)(S):(\mathrm{antisymmetricSubmodule}N))=(⟨\mathrm{slaterVector}NS,\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterAntiVector (✓ 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.18 (slaterAntiVector_dense).

$$\forall (N:\mathbb{N}),(\mathrm{Submodule}.\mathrm{span}\mathbb{C}(\mathrm{Set}.\mathrm{range}(\mathrm{slaterAntiVector}N)))\perp =\mathrm{bot}$$

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

Theorem 1.19 (slaterAntiVector_orthonormal).

$$\forall (N:\mathbb{N}),\mathrm{Orthonormal}\mathbb{C}(\mathrm{slaterAntiVector}N)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterAntiVector_orthonormal (✓ 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 (slaterHilbertBasis).

$$\forall (N:\mathbb{N})(h:\mathrm{Orthonormal}\mathbb{C}(\mathrm{slaterAntiVector}N))(g:(\mathrm{Submodule}.\mathrm{span}\mathbb{C}(\mathrm{Set}.\mathrm{range}(\mathrm{slaterAntiVector}N)))\perp =\mathrm{bot}),(\mathrm{slaterHilbertBasis}(N):\mathrm{HilbertBasis}\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}\mathbb{C}(\mathrm{antisymmetricSubmodule}N))=(\mathrm{HilbertBasis}.\mathrm{mkOfOrthogonalEqBot}hg)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterHilbertBasis (✓ 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.21 (slaterVector).

$$\forall (N:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\}),(\mathrm{slaterVector}(N)(S):(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2))=(⟨(((\mathrm{Real}.\mathrm{sqrt}(N.\mathrm{factorial}:\mathbb{R}):\mathbb{C}){)}^{-1})\cdot \mathrm{MultilinearMap}.\mathrm{alternatization}(\mathrm{MultilinearMap}.\mathrm{piFamily}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathrm{MultilinearMap}.\mathrm{mkPiAlgebra}\mathbb{C}(\mathrm{Fin}N)\mathbb{C}))(\mathrm{fun}(i:\mathrm{Fin}N)\mapsto \mathrm{Pi}.\mathrm{single}(S.\mathrm{val}.\mathrm{orderEmbOfFin}S.\mathrm{property}i)(1:\mathbb{C})),\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterVector (✓ 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.22 (slater_inner_antisymmetric).

$$\forall (N:\mathbb{N})(S:\{s:\mathrm{Finset}\mathbb{N}//s.\mathrm{card}=N\})(\psi :(\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})2)),\mathrm{IsAntisymmetric}N\psi \to \mathrm{inner}\mathbb{C}(\mathrm{slaterVector}NS)\psi =(\mathrm{Real}.\mathrm{sqrt}(N.\mathrm{factorial}:\mathbb{R}):\mathbb{C})\ast (\psi :(i:\mathrm{Fin}N\to \mathbb{N})\to (\mathrm{fun}{(}_{:}\mathrm{Fin}N\to \mathbb{N})\mapsto \mathbb{C})i)(\mathrm{occupationTuple}NS1)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slater_inner_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.23 (sourceCanonicalFamily).

$$\forall (\iota :\mathrm{Type})(E:\mathrm{Type})[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{CompleteSpace}E][\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}E](e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(v:\iota \times \mathrm{Fin}2\to E)(\mathrm{hv}:\mathrm{Orthonormal}\mathbb{C}v)(c:\mathrm{CanonicalFamily}\iota )(h:\mathrm{Orthonormal}\mathbb{C}(\mathrm{sourcePairWedge}v)),(\mathrm{sourceCanonicalFamily}(e)(v)(\mathrm{hv})(c):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EE))=(h.\mathrm{orthogonalFamily}.\mathrm{linearIsometry}(\mathrm{familyCoefficients}c))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily (✓ 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 (sourceCanonicalFamily_coordinates).

$$\forall \{\iota :\mathrm{Type}\}\{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{CompleteSpace}E][\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}E]\{\kappa :\mathrm{Type}\}(e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(v:\iota \times \mathrm{Fin}2\to E)(\mathrm{hv}:\mathrm{Orthonormal}\mathbb{C}v)(c:\mathrm{CanonicalFamily}\iota )(b:\mathrm{HilbertBasis}\kappa \mathbb{C}E)(\mathrm{label}:\mathrm{Function}.\mathrm{Embedding}\kappa \mathbb{N})(r:\iota \times \mathrm{Fin}2\to \kappa ),(\forall (p:\iota \times \mathrm{Fin}2),(b:\kappa \to E)(rp)=vp)\to (\forall (i:\iota ),(\mathrm{label}:\kappa \to \mathbb{N})(r(i,0))=4\ast (e:\iota \to \mathbb{N})i)\to (\forall (i:\iota ),(\mathrm{label}:\kappa \to \mathbb{N})(r(i,1))=4\ast (e:\iota \to \mathbb{N})i+1)\to (\mathrm{tensorCoordinateEmbedding}b\mathrm{label}:\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EE)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathbb{N}\times \mathbb{N})\mapsto \mathbb{C})2))(\mathrm{sourceCanonicalFamily}ev\mathrm{hv}c)=\mathrm{canonicalTensor}(\mathrm{padCanonicalSequence}(\mathrm{familySequence}ec))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily_coordinates (✓ 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 (sourceCanonicalFamily_series).

$$\forall \{\iota :\mathrm{Type}\}\{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{CompleteSpace}E][\mathrm{TopologicalSpace}.\mathrm{SeparableSpace}E](e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(v:\iota \times \mathrm{Fin}2\to E)(\mathrm{hv}:\mathrm{Orthonormal}\mathbb{C}v)(c:\mathrm{CanonicalFamily}\iota ),\mathrm{sourceCanonicalFamily}ev\mathrm{hv}c=\sum ^{\prime }(i:\iota ),((c.\mathrm{coeff}i):\mathbb{C})\cdot \mathrm{sourcePairWedge}vi$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily_series (✓ 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 (sourceExterior).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(x_e:\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})(n:\mathbb{N}),(\mathrm{sourceExterior}(X)(b)(x_e)(n):\mathrm{Submodule}\mathbb{C}(\mathrm{tensorTower}Xn).\mathrm{carrier})=(\{\mathrm{carrier}:=\{\psi |\forall (\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}(n+1))),\mathrm{tensorPermutation}Xbn\sigma \psi =\mathrm{permutationPhase}(n+1)\sigma \cdot \psi \},\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceExterior (✓ 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 exterior sector is the physical permutation-antisymmetric part of the actual completed tensor power: each permutation acts by its sign. The coordinate characterization is private and is used by the physical contraction proof.

Definition 1.27 (sourceHilbertObject).

$$\forall (E:\mathrm{Type})[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{CompleteSpace}E],(\mathrm{sourceHilbertObject}(E):\mathrm{HilbertObject})=(\{\mathrm{carrier}:=E,\mathrm{normed}:=\mathrm{inferInstance},\mathrm{innerProduct}:=\mathrm{inferInstance},\mathrm{complete}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceHilbertObject (✓ 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.28 (sourceTensorCoordinates).

$$\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{sourceTensorCoordinates}(X)(b)(e)(n):(\mathrm{tensorTower}Xn).\mathrm{carrier}{\to }_{li}[\mathbb{C}](\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2))=((\mathrm{coordinateRename}e.\mathrm{arrowCongrRight}).\mathrm{comp}(\mathrm{tensorTowerTupleBasis}Xbn).\mathrm{repr}.\mathrm{toLinearIsometry})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceTensorCoordinates (✓ 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.29 (sourceTensorCoordinates_antisymmetric).

$$\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{tensorTower}Xn).\mathrm{carrier}),\mathrm{IsAntisymmetric}(n+1)((\mathrm{sourceTensorCoordinates}Xben:(\mathrm{tensorTower}Xn).\mathrm{carrier}\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \mathbb{N})\mapsto \mathbb{C})2))\psi )⟺\psi \in \mathrm{sourceExterior}Xben$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceTensorCoordinates_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.30 (tensorHead).

$$\forall (E:\mathrm{Type})(F:\mathrm{Type})[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F][\mathrm{CompleteSpace}F](f:E),(\mathrm{tensorHead}(f):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF){\to }_L[\mathbb{C}]F)=(((((\mathrm{TensorProduct}.\mathrm{lidIsometry}\mathbb{C}F):\mathrm{TensorProduct}\mathbb{CC}F{\equiv }_L[\mathbb{C}]F):\mathrm{TensorProduct}\mathbb{CC}F{\to }_L[\mathbb{C}]F){\circ }_{\mathrm{SL}}\mathrm{ContinuousLinearMap}.\mathrm{rTensor}F((\mathrm{innerSL}\mathbb{C}:E\to E{\to }_L[\mathbb{C}]\mathbb{C})f)).\mathrm{extend}\mathrm{UniformSpace}.\mathrm{Completion}.\mathrm{toComplL})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead (✓ 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.31 (tensorHead_adjoint).

$$\forall \{E:\mathrm{Type}\}\{F:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F][\mathrm{CompleteSpace}F]\{\iota :\mathrm{Type}\}\{\kappa :\mathrm{Type}\}{(}_{:}\mathrm{HilbertBasis}\iota \mathbb{C}E){(}_{:}\mathrm{HilbertBasis}\kappa \mathbb{C}F)(f:E),\mathrm{tensorHead}f=(\mathrm{ContinuousLinearMap}.\mathrm{adjoint}:(F{\to }_L[\mathbb{C}]\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF))\to \mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF){\to }_L[\mathbb{C}]F)(\mathrm{UniformSpace}.\mathrm{Completion}.\mathrm{toComplL}{\circ }_{\mathrm{SL}}(\mathrm{TensorProduct}.\mathrm{mkL}\mathbb{C}EF:E\to F{\to }_L[\mathbb{C}]\mathrm{TensorProduct}\mathbb{C}EF)f)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead_adjoint (✓ 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.32 (tensorHead_basis_coordinates).

$$\forall \{E:\mathrm{Type}\}\{F:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{InnerProductSpace}\mathbb{C}E][\mathrm{NormedAddCommGroup}F][\mathrm{InnerProductSpace}\mathbb{C}F][\mathrm{CompleteSpace}F]\{\iota :\mathrm{Type}\}\{\kappa :\mathrm{Type}\}(b:\mathrm{HilbertBasis}\iota \mathbb{C}E)(c:\mathrm{HilbertBasis}\kappa \mathbb{C}F)(i:\iota )(\psi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF))(j:\kappa ),(((c.\mathrm{repr}:F\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\kappa )\mapsto \mathbb{C})2))((\mathrm{tensorHead}((b:\iota \to E)i):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF)\to F)\psi )):(i:\kappa )\to (\mathrm{fun}{(}_{:}\kappa )\mapsto \mathbb{C})i)j=((((\mathrm{tensorHilbertBasis}bc).\mathrm{repr}:\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}EF)\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\iota \times \kappa )\mapsto \mathbb{C})2))\psi ):(i:\iota \times \kappa )\to (\mathrm{fun}{(}_{:}\iota \times \kappa )\mapsto \mathbb{C})i)(i,j)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead_basis_coordinates (✓ 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.33 (tensorHilbertObject).

$$\forall (X:\mathrm{HilbertObject})(Y:\mathrm{HilbertObject}),(\mathrm{tensorHilbertObject}(X)(Y):\mathrm{HilbertObject})=(\{\mathrm{carrier}:=\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}Y.\mathrm{carrier}),\mathrm{normed}:=\mathrm{inferInstance},\mathrm{innerProduct}:=\mathrm{inferInstance},\mathrm{complete}:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHilbertObject (✓ 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 (tensorPermutation).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(n:\mathbb{N})(\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}(n+1))),(\mathrm{tensorPermutation}(X)(b)(n)(\sigma ):(\mathrm{tensorTower}Xn).\mathrm{carrier}{\equiv }_{li}[\mathbb{C}](\mathrm{tensorTower}Xn).\mathrm{carrier})=((\mathrm{tensorTowerTupleBasis}Xbn).\mathrm{repr}.\mathrm{trans}((\mathrm{coordinateEquiv}(\mathrm{Equiv}.\mathrm{arrowCongr}\sigma (\mathrm{Equiv}.\mathrm{refl}\iota ))).\mathrm{trans}(\mathrm{tensorTowerTupleBasis}Xbn).\mathrm{repr}.\mathrm{symm}))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPermutation (✓ 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.35 (tensorPermutation_product).

$$\forall \{\iota :\mathrm{Type}\}(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(n:\mathbb{N})(\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}(n+1)))(x:\mathrm{Fin}(n+1)\to X.\mathrm{carrier}),(\mathrm{tensorPermutation}Xbn\sigma :(\mathrm{tensorTower}Xn).\mathrm{carrier}\to (\mathrm{tensorTower}Xn).\mathrm{carrier})(\mathrm{tensorPure}Xnx)=\mathrm{tensorPure}Xn(x\circ ((\mathrm{Equiv}.\mathrm{symm}\sigma ):\mathrm{Fin}(n+1)\to \mathrm{Fin}(n+1)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPermutation_product (✓ 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 bounded tensor permutation acts on an actual pure completed tensor by permuting its physical one-particle factors. This identifies the coordinate construction with physical tensor antisymmetry.

Definition 1.36 (tensorPure).

$$\forall (X:\mathrm{HilbertObject}),(\forall (x:\mathrm{Fin}1\to X.\mathrm{carrier}),\mathrm{tensorPure}X0x=x0)\wedge (\forall (n:\mathbb{N})(x:\mathrm{Fin}(n+2)\to X.\mathrm{carrier}),\mathrm{tensorPure}X(n+1)x=(\mathrm{TensorProduct}.\mathrm{tmul}\mathbb{C}(x0)(\mathrm{tensorPure}Xn(\mathrm{Fin}.\mathrm{tail}x)):\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}X.\mathrm{carrier}(\mathrm{tensorTower}Xn).\mathrm{carrier})))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPure (✓ 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.37 (tensorTower).

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

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTower (✓ 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 (tensorTowerBasis).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier}),\mathrm{tensorTowerBasis}Xb0=b\wedge (\forall (n:\mathbb{N}),\mathrm{tensorTowerBasis}Xb(n+1)=\mathrm{tensorHilbertBasis}b(\mathrm{tensorTowerBasis}Xbn))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerBasis (✓ 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.39 (tensorTowerTupleBasis).

$$\forall (\iota :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(n:\mathbb{N}),(\mathrm{tensorTowerTupleBasis}(X)(b)(n):\mathrm{HilbertBasis}(\mathrm{Fin}(n+1)\to \iota )\mathbb{C}(\mathrm{tensorTower}Xn).\mathrm{carrier})=(\{\mathrm{repr}:=(\mathrm{tensorTowerBasis}Xbn).\mathrm{repr}.\mathrm{trans}(\mathrm{coordinateEquiv}(\mathrm{tensorTowerTupleEquiv}\iota n))\})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerTupleBasis (✓ 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.40 (tensorTowerTupleEquiv).

$$\forall (\iota :\mathrm{Type}),\mathrm{tensorTowerTupleEquiv}\iota 0=(\mathrm{Equiv}.\mathrm{funUnique}(\mathrm{Fin}1)\iota ).\mathrm{symm}\wedge (\forall (n:\mathbb{N}),\mathrm{tensorTowerTupleEquiv}\iota (n+1)=(\mathrm{Equiv}.\mathrm{prodCongr}(\mathrm{Equiv}.\mathrm{refl}\iota )(\mathrm{tensorTowerTupleEquiv}\iota n)).\mathrm{trans}(\mathrm{Fin}.\mathrm{consEquiv}({\mathrm{fun}}_{:}\mathrm{Fin}(n+2)\mapsto \iota )))$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerTupleEquiv (✓ 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.41 (tupleBasis_repr).

$$\forall \{\iota :\mathrm{Type}\}(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\iota \mathbb{C}X.\mathrm{carrier})(n:\mathbb{N})(\psi :(\mathrm{tensorTower}Xn).\mathrm{carrier})(t:\mathrm{Fin}(n+1)\to \iota ),((((\mathrm{tensorTowerTupleBasis}Xbn).\mathrm{repr}:(\mathrm{tensorTower}Xn).\mathrm{carrier}\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \iota )\mapsto \mathbb{C})2))\psi ):(i:\mathrm{Fin}(n+1)\to \iota )\to (\mathrm{fun}{(}_{:}\mathrm{Fin}(n+1)\to \iota )\mapsto \mathbb{C})i)t=((((\mathrm{tensorTowerBasis}Xbn).\mathrm{repr}:(\mathrm{tensorTower}Xn).\mathrm{carrier}\to (\mathrm{lp}(\mathrm{fun}{(}_{:}\mathrm{TensorTowerIndex}\iota n)\mapsto \mathbb{C})2))\psi ):(i:\mathrm{TensorTowerIndex}\iota n)\to (\mathrm{fun}{(}_{:}\mathrm{TensorTowerIndex}\iota n)\mapsto \mathbb{C})i)(((\mathrm{tensorTowerTupleEquiv}\iota n).\mathrm{symm}:(\mathrm{Fin}(n+1)\to \iota )\to \mathrm{TensorTowerIndex}\iota n)t)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tupleBasis_repr (✓ 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/CompletedTensorSlaterGeometry.CanonicalFamily
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.HilbertObject
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.IsAntisymmetric
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.TensorTowerIndex
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricComplete
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricSubmodule
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetricSubmodule_closed
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetric_orthogonal_slaters_zero
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.antisymmetric_repeated_zero
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.coordinateEquiv
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.extendedCoeff_moment
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familyCoefficients
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familySequence
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.familySequence_cap
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.occupationTuple
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.permutationPhase
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterAntiVector
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterAntiVector_dense
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterAntiVector_orthonormal
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterHilbertBasis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slaterVector
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.slater_inner_antisymmetric
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily_coordinates
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceCanonicalFamily_series
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceExterior
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceHilbertObject
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceTensorCoordinates
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.sourceTensorCoordinates_antisymmetric
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead_adjoint
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHead_basis_coordinates
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorHilbertObject
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPermutation
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPermutation_product
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorPure
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTower
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerBasis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerTupleBasis
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tensorTowerTupleEquiv
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/CompletedTensorSlaterGeometry.tupleBasis_repr
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/CanonicalRdmAndPadding