Quantum states and tensor placement for the low individual degree test

Core quantum-state definitions together with tensor-placement operators.

structure MIPStarRE.LDT.QuantumState (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type u_1

A PSD density matrix indexed by ι.

There is intentionally no global Inhabited instance: the zero matrix is PSD but not a physical state of unit trace, so an ambient default would silently trivialize later statements. Use IsNormalized to additionally require τ(ρ) = 1.

This remains the ambient state space for the current LDT development: strategy packages in LDT/Test/StrategyCore.lean, the SWAP-symmetry API PermInvState, and the expectation-value lemmas in LDT/Basic/OperatorExpectations.lean are all stated for arbitrary density matrices, not only pure states.

• density : Quantum.Op ι
• density_psd : 0 ≤ self.density

def MIPStarRE.LDT.QuantumState.IsNormalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) : Prop

Unit normalized trace for the concrete matrix carried by a state.

Equations

• ψ.IsNormalized = (MIPStarRE.Quantum.normalizedTrace ψ.density = 1)

theorem MIPStarRE.LDT.QuantumState.IsNormalized.nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ψ : QuantumState ι} (hψ : ψ.IsNormalized) : Nonempty ι

A normalized state has a nonempty carrier: if the carrier were empty, the trace would vanish and normalizedTrace = 0 / 0 = 0, contradicting = 1.

noncomputable def MIPStarRE.LDT.pureDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : ι → ℂ) : Quantum.Op ι

The scaled rank-one density matrix attached to a state vector.

Because this development uses the normalized trace τ(A) = tr(A) / dim, the quantum state represented by a unit vector ψ is dim · |ψ⟩⟨ψ| rather than the raw projector |ψ⟩⟨ψ|. This scaling makes τ(ρ) = 1 and keeps ev aligned with the paper's bra-ket expectations.

Equations

• MIPStarRE.LDT.pureDensity ψ = ↑(Fintype.card ι) • Matrix.vecMulVec ψ (star ψ)

def MIPStarRE.LDT.swapVector {ι : Type u_1} (ψ : ι × ι → ℂ) : ι × ι → ℂ

Swap the two tensor coordinates of a bipartite state vector.

Equations

• MIPStarRE.LDT.swapVector ψ ij = ψ (ij.2, ij.1)

structure MIPStarRE.LDT.PureState (ι : Type u_1) [Fintype ι] [DecidableEq ι] [Nonempty ι] : Type u_1

A pure-state witness as a unit vector in the ambient finite Hilbert space.

The associated density matrix is pureDensity ψ.vector = dim · |ψ⟩⟨ψ|, so that coercing to QuantumState preserves the paper's scalar ⟨ψ|X|ψ⟩ formulas despite our use of the normalized trace.

• vector : ι → ℂ
• unit : star self.vector ⬝ᵥ self.vector = 1

noncomputable def MIPStarRE.LDT.PureState.basis {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (i : ι) : PureState ι

The coordinate-basis pure state at a distinguished basis vector.

Equations

• MIPStarRE.LDT.PureState.basis i = { vector := fun (j : ι) => if j = i then 1 else 0, unit := ⋯ }

noncomputable def MIPStarRE.LDT.PureState.density {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : Quantum.Op ι

The density matrix represented by a pure-state witness.

Equations

• ψ.density = MIPStarRE.LDT.pureDensity ψ.vector

theorem MIPStarRE.LDT.PureState.density_psd {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : 0 ≤ ψ.density

noncomputable def MIPStarRE.LDT.PureState.toQuantumState {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : QuantumState ι

Equations

• ψ.toQuantumState = { density := ψ.density, density_psd := ⋯ }

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.PureState.instCoeQuantumState {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] : Coe (PureState ι) (QuantumState ι)

Equations

• MIPStarRE.LDT.PureState.instCoeQuantumState = { coe := MIPStarRE.LDT.PureState.toQuantumState }

@[simp]

theorem MIPStarRE.LDT.PureState.coe_density {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : ψ.toQuantumState.density = ψ.density

theorem MIPStarRE.LDT.PureState.normalizedTrace_density {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : Quantum.normalizedTrace ψ.density = 1

theorem MIPStarRE.LDT.PureState.toQuantumState_isNormalized {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) : ψ.toQuantumState.IsNormalized

theorem MIPStarRE.LDT.PureState.normalizedTrace_density_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) (X : Quantum.Op ι) : Quantum.normalizedTrace (ψ.toQuantumState.density * X) = star ψ.vector ⬝ᵥ Matrix.mulVec X ψ.vector

def MIPStarRE.LDT.PureState.IsSwapInvariant {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState (ι × ι)) : Prop

Vector-level SWAP invariance for a bipartite pure-state witness.

This is stronger than density-level SWAP invariance: it records the paper's honest vector symmetry and rules out antisymmetric vectors, even though those vectors define SWAP-invariant density matrices.

Equations

• ψ.IsSwapInvariant = (MIPStarRE.LDT.swapVector ψ.vector = ψ.vector)

@[simp]

theorem MIPStarRE.LDT.swapVector_swapVector {ι : Type u_1} (ψ : ι × ι → ℂ) : swapVector (swapVector ψ) = ψ

noncomputable def MIPStarRE.LDT.ev {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (X : Quantum.Op ι) : Error

The expectation Re τ(ψ X). Dimensions match by construction.

Equations

• MIPStarRE.LDT.ev ψ X = (MIPStarRE.Quantum.normalizedTrace (ψ.density * X)).re

theorem MIPStarRE.LDT.PureState.ev_eq_re_inner {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState ι) (X : Quantum.Op ι) : ev ψ.toQuantumState X = (star ψ.vector ⬝ᵥ Matrix.mulVec X ψ.vector).re

@[reducible, inline]

abbrev MIPStarRE.LDT.opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : Quantum.Op (ι₁ × ι₂)

Tensor product of two operators via Kronecker product.

Equations

• MIPStarRE.LDT.opTensor A B = Matrix.kronecker A B

@[reducible, inline]

abbrev MIPStarRE.LDT.leftTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) : Quantum.Op (ι₁ × ι₂)

Left placement A ⊗ I on a bipartite space ι₁ × ι₂.

Equations

• MIPStarRE.LDT.leftTensor A = Matrix.kronecker A 1

@[reducible, inline]

abbrev MIPStarRE.LDT.rightTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (B : Quantum.Op ι₂) : Quantum.Op (ι₁ × ι₂)

Right placement I ⊗ B on a bipartite space ι₁ × ι₂.

Equations

• MIPStarRE.LDT.rightTensor B = Matrix.kronecker 1 B

theorem MIPStarRE.LDT.leftTensor_one {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] : leftTensor 1 = 1

Left placement of the identity is the identity on the product space.

theorem MIPStarRE.LDT.rightTensor_one {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] : rightTensor 1 = 1

Right placement of the identity is the identity on the product space.

theorem MIPStarRE.LDT.leftTensor_mul_rightTensor_eq_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : leftTensor A * rightTensor B = opTensor A B

Local tensor placements multiply to the full Kronecker product.

theorem MIPStarRE.LDT.opTensor_nonneg {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₁} {B : Quantum.Op ι₂} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ opTensor A B

Positivity is preserved by opTensor.

theorem MIPStarRE.LDT.normalizedTrace_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Nonempty ι₁] [Fintype ι₂] [DecidableEq ι₂] [Nonempty ι₂] (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : Quantum.normalizedTrace (opTensor A B) = Quantum.normalizedTrace A * Quantum.normalizedTrace B

The normalized trace of a tensor product is the product of the normalized traces.

noncomputable def MIPStarRE.LDT.QuantumState.tensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState ι₁) (φ : QuantumState ι₂) : QuantumState (ι₁ × ι₂)

Tensor product of two quantum states.

Equations

• ψ.tensor φ = { density := MIPStarRE.LDT.opTensor ψ.density φ.density, density_psd := ⋯ }

@[simp]

theorem MIPStarRE.LDT.QuantumState.tensor_density {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState ι₁) (φ : QuantumState ι₂) : (ψ.tensor φ).density = opTensor ψ.density φ.density

theorem MIPStarRE.LDT.QuantumState.tensor_isNormalized {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {ψ : QuantumState ι₁} {φ : QuantumState ι₂} (hψ : ψ.IsNormalized) (hφ : φ.IsNormalized) : (ψ.tensor φ).IsNormalized

Tensor products of normalized states are normalized.

theorem MIPStarRE.LDT.opTensor_le_leftTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₁} {B : Quantum.Op ι₂} (hA : 0 ≤ A) (hB : B ≤ 1) : opTensor A B ≤ leftTensor A

If 0 ≤ A and B ≤ 1, then A ⊗ B ≤ A ⊗ I.

theorem MIPStarRE.LDT.opTensor_mono_left {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A₁ A₂ : Quantum.Op ι₁} {B : Quantum.Op ι₂} (hA : A₁ ≤ A₂) (hB : 0 ≤ B) : opTensor A₁ B ≤ opTensor A₂ B

opTensor is monotone in the left factor against a PSD right factor.

theorem MIPStarRE.LDT.leftTensor_mono {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A₁ A₂ : Quantum.Op ι₁} (hA : A₁ ≤ A₂) : leftTensor A₁ ≤ leftTensor A₂

Left tensor placement is monotone.

theorem MIPStarRE.LDT.opTensor_mono_right {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₁} {B₁ B₂ : Quantum.Op ι₂} (hA : 0 ≤ A) (hB : B₁ ≤ B₂) : opTensor A B₁ ≤ opTensor A B₂

opTensor is monotone in the right factor against a PSD left factor.

theorem MIPStarRE.LDT.rightTensor_mono {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {B₁ B₂ : Quantum.Op ι₂} (hB : B₁ ≤ B₂) : rightTensor B₁ ≤ rightTensor B₂

Right tensor placement is monotone.

theorem MIPStarRE.LDT.rightTensor_mul_leftTensor_eq_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : rightTensor B * leftTensor A = opTensor A B

rightTensor B * leftTensor A = opTensor A B.

theorem MIPStarRE.LDT.leftTensor_mul_leftTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) : leftTensor A * leftTensor B = leftTensor (A * B)

leftTensor A * leftTensor B = leftTensor (A * B).

theorem MIPStarRE.LDT.leftTensor_mul_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) (C : Quantum.Op ι₂) : leftTensor A * opTensor B C = opTensor (A * B) C

Multiplying a left tensor into a full tensor only affects the left factor.

theorem MIPStarRE.LDT.opTensor_mul_leftTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) (C : Quantum.Op ι₂) : opTensor A C * leftTensor B = opTensor (A * B) C

Multiplying a full tensor by a left tensor only affects the left factor.

theorem MIPStarRE.LDT.leftTensor_smul {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : ℂ) (A : Quantum.Op ι₁) : c • leftTensor A = leftTensor (c • A)

Scalar multiplication commutes with left tensor placement.

theorem MIPStarRE.LDT.leftTensor_pow {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (n : ℕ) : leftTensor A ^ n = leftTensor (A ^ n)

Powers commute with left tensor placement.

theorem MIPStarRE.LDT.rightTensor_mul_rightTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₂) : rightTensor A * rightTensor B = rightTensor (A * B)

rightTensor A * rightTensor B = rightTensor (A * B).

theorem MIPStarRE.LDT.rightTensor_mul_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₂) (B : Quantum.Op ι₁) (C : Quantum.Op ι₂) : rightTensor A * opTensor B C = opTensor B (A * C)

Multiplying a right tensor into a full tensor only affects the right factor.

theorem MIPStarRE.LDT.conjTranspose_opTensor {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : Matrix.conjTranspose (opTensor A B) = opTensor (Matrix.conjTranspose A) (Matrix.conjTranspose B)

Conjugate transpose distributes over opTensor.

@[simp]

theorem MIPStarRE.LDT.leftTensor_conjTranspose {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) : Matrix.conjTranspose (leftTensor A) = leftTensor (Matrix.conjTranspose A)

Conjugate transpose commutes with left tensor placement.

@[simp]

theorem MIPStarRE.LDT.rightTensor_conjTranspose {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (B : Quantum.Op ι₂) : Matrix.conjTranspose (rightTensor B) = rightTensor (Matrix.conjTranspose B)

Conjugate transpose commutes with right tensor placement.

theorem MIPStarRE.LDT.opTensor_mul {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A₁ A₂ : Quantum.Op ι₁) (B₁ B₂ : Quantum.Op ι₂) : opTensor A₁ B₁ * opTensor A₂ B₂ = opTensor (A₁ * A₂) (B₁ * B₂)

opTensor distributes over multiplication.

theorem MIPStarRE.LDT.opTensor_sub_left {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) (C : Quantum.Op ι₂) : opTensor A C - opTensor B C = opTensor (A - B) C

opTensor is linear in the left factor: subtraction.

theorem MIPStarRE.LDT.leftTensor_sub {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) : leftTensor A - leftTensor B = leftTensor (A - B)

Left tensor placement commutes with subtraction.

theorem MIPStarRE.LDT.rightTensor_sub {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₂) : rightTensor A - rightTensor B = rightTensor (A - B)

Right tensor placement commutes with subtraction.

theorem MIPStarRE.LDT.opTensor_smul_left_error {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : opTensor (c • A) B = c • opTensor A B

opTensor is linear in the left factor: real scalar multiplication.

theorem MIPStarRE.LDT.opTensor_smul_right_error {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : opTensor A (c • B) = c • opTensor A B

opTensor is linear in the right factor: real scalar multiplication.

theorem MIPStarRE.LDT.opTensor_add_left_local {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A B : Quantum.Op ι₁) (C : Quantum.Op ι₂) : opTensor (A + B) C = opTensor A C + opTensor B C

opTensor is additive in the left factor.

theorem MIPStarRE.LDT.opTensor_add_right_local {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (B C : Quantum.Op ι₂) : opTensor A (B + C) = opTensor A B + opTensor A C

opTensor is additive in the right factor.

theorem MIPStarRE.LDT.opTensor_sum_left_finset {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (s : Finset α) (f : α → Quantum.Op ι₁) (B : Quantum.Op ι₂) : opTensor (∑ a ∈ s, f a) B = ∑ a ∈ s, opTensor (f a) B

Pull a finite sum out of the left factor of opTensor.

theorem MIPStarRE.LDT.opTensor_sum_right_finset {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (s : Finset α) (f : α → Quantum.Op ι₂) : opTensor A (∑ a ∈ s, f a) = ∑ a ∈ s, opTensor A (f a)

Pull a finite sum out of the right factor of opTensor.

theorem MIPStarRE.LDT.opTensor_sum_left_univ {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype α] [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (f : α → Quantum.Op ι₁) (B : Quantum.Op ι₂) : opTensor (∑ a : α, f a) B = ∑ a : α, opTensor (f a) B

Pull an unindexed finite-type sum out of the left factor of opTensor.

theorem MIPStarRE.LDT.opTensor_sum_right_univ {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype α] [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (A : Quantum.Op ι₁) (f : α → Quantum.Op ι₂) : opTensor A (∑ a : α, f a) = ∑ a : α, opTensor A (f a)

Pull an unindexed finite-type sum out of the right factor of opTensor.