SourceCorrelationalBound

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

$$\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{hv}:\mathrm{Orthonormal}\mathbb{C}v)(h:\exists f:\iota \to \mathbb{N},\mathrm{Function}.\mathrm{Injective}f),(\mathrm{canonicalIndex}(v)(\mathrm{hv}):\mathrm{Function}.\mathrm{Embedding}\iota \mathbb{N})=(\{\mathrm{toFun}:=\mathrm{Classical}.\mathrm{choose}h,\mathrm{in}{\mathrm{j}}^{\prime }:=\dots \})$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.canonicalIndex (✓ 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.2 (claim).

$$(\mathrm{claim}:\mathrm{Prop})=(\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{hv}:\mathrm{Orthonormal}\mathbb{C}v)(c:\mathrm{CanonicalFamily}\iota )(\varphi :\mathrm{UniformSpace}.\mathrm{Completion}(\mathrm{TensorProduct}\mathbb{C}HH)),\mathrm{HasSum}(\mathrm{fun}(i:\iota )\mapsto ((c.\mathrm{coeff}i):\mathbb{C})\cdot \mathrm{sourcePairWedge}vi)\varphi \to \forall (m:\mathbb{N}),(2\ast (m:\mathbb{R})+2)\ast (\mathrm{lambdaMax}c{)}^2\le 1\to \mathrm{have}d:=\mathrm{adaptedChart}(\mathrm{canonicalIndex}v\mathrm{hv})v\mathrm{hv};\forall (\psi :(\mathrm{tensorTower}(\mathrm{sourceHilbertObject}H)(2\ast m+1)).\mathrm{carrier})(\mathrm{hanti}:\forall (\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}(2\ast m+2))),(\mathrm{tensorPermutation}(\mathrm{sourceHilbertObject}H)d.\mathrm{basis}(2\ast m+1)\sigma :(\mathrm{tensorTower}(\mathrm{sourceHilbertObject}H)(2\ast m+1)).\mathrm{carrier}\to (\mathrm{tensorTower}(\mathrm{sourceHilbertObject}H)(2\ast m+1)).\mathrm{carrier})\psi =\mathrm{permutationPhase}(2\ast m+2)\sigma \cdot \psi ),\Vert \psi \Vert =1\to \mathrm{sourceRayleigh}(\mathrm{sourceHilbertObject}H)d.\mathrm{basis}d.\mathrm{label}(2\ast m)(\mathrm{physicalParticle}(\mathrm{sourceHilbertObject}H)d.\mathrm{basis}d.\mathrm{label}(2\ast m+1)\psi \mathrm{hanti})\varphi \le (2\ast (m:\mathbb{R})+2)\ast (1-(m:\mathbb{R})\ast (\sum ^{\prime }(i:\iota ),(c.\mathrm{coeff}i{)}^4)+5/8\ast (((2\ast (m:\mathbb{R})+2)\ast (\mathrm{lambdaMax}c{)}^2){)}^2))$$

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

Christiansen, Section 1.1, p. 4, Conjecture 3, verbatim: “Let Φ ∈ 𝔥 ∧ 𝔥 be normalized with canonical form Φ = ∑{k=1}^{∞} λ_k u_k ∧ v_k. Then there exists a constant C > 0, independent of Φ, such that for every N ∈ 2ℕ with N λ_max² ≤ 1 sup{Ψ ∈ ⋀ᴺ𝔥, ‖Ψ‖=1} ⟨Φ, γ₂^Ψ Φ⟩ ≤ N(1 − (N−2)/2 ∑_{k=1}^{∞} λ_k⁴ + C(N λ_max²)²).”. The displayed claim fixes C = 5/8. H is an arbitrary separable complex Hilbert space; Φ has the supplied normalized canonical form, v(i,0) and v(i,1) are mutually orthonormal, and m parametrizes N = 2m + 2. The physical tensor permutation action defines fermionic antisymmetry. sourceRayleigh uses the literal creation/annihilation-kernel RDM, with trace N(N−1). lambdaMax is the attained maximum. The source supremum is encoded by quantifying every normalized ψ.

Definition 1.3 (lambdaMax).

$$\forall (\iota :\mathrm{Type})(c:\mathrm{CanonicalFamily}\iota )(h:\exists a:\mathbb{R},\mathrm{IsGreatest}(\mathrm{Set}.\mathrm{range}c.\mathrm{coeff})a),(\mathrm{lambdaMax}(c):\mathbb{R})=(\mathrm{Classical}.\mathrm{choose}h)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.lambdaMax (✓ 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 (physicalParticle).

$$\forall (\kappa :\mathrm{Type})(X:\mathrm{HilbertObject})(b:\mathrm{HilbertBasis}\kappa \mathbb{C}X.\mathrm{carrier})(\mathrm{label}:\mathrm{Function}.\mathrm{Embedding}\kappa \mathbb{N})(n:\mathbb{N})(\psi :(\mathrm{tensorTower}Xn).\mathrm{carrier})(\mathrm{h\psi }:\forall (\sigma :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}(n+1))),(\mathrm{tensorPermutation}Xbn\sigma :(\mathrm{tensorTower}Xn).\mathrm{carrier}\to (\mathrm{tensorTower}Xn).\mathrm{carrier})\psi =\mathrm{permutationPhase}(n+1)\sigma \cdot \psi ),(\mathrm{physicalParticle}(X)(b)(\mathrm{label})(n)(\psi )(\mathrm{h\psi }):(\mathrm{particleExterior}Xb\mathrm{label}(n+1)))=(⟨\psi ,\dots ⟩)$$

Formalization. D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.physicalParticle (✓ 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.5 (result).

$$\mathrm{claim}$$

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

Resolves. Problems/christiansen-2025-fermionic-correlational-bound (proved) by D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.result.

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 claim holds with C = 5/8. The weighted occupation-row estimate retains the fourth moment, spectator modes, weight one at zero coefficient, and the original unrenormalized cutoffs.

References

• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.canonicalIndex
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.claim
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.lambdaMax
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.physicalParticle
• Truth anchor: D5/S3/Quantum/FermionicCorrelationalBound/SourceCorrelationalBound.result
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/CompletedCorrelationalBound
• Dependency: D5/S3/Quantum/FermionicCorrelationalBound/PhysicalContractionRdmBridge