Role-register tensor algebra for the low individual degree test

Role-register operators and strategy symmetrization infrastructure extracted from MIPStarRE.LDT.Test.Strategy.

Role-register tensor algebra

theorem MIPStarRE.LDT.sum_role_eq_add {α : Type u_1} [AddCommMonoid α] (f : Role → α) : ∑ r : Role, f r = f Role.A + f Role.B

def MIPStarRE.LDT.roleProj (r : Role) : Quantum.Op Role

Basis projector onto the role sector r.

Equations

• MIPStarRE.LDT.roleProj r = Matrix.single r r 1

theorem MIPStarRE.LDT.roleProj_nonneg (r : Role) : 0 ≤ roleProj r

The basis projector onto a role sector is positive semidefinite.

@[simp]

theorem MIPStarRE.LDT.roleProj_mul_self (r : Role) : roleProj r * roleProj r = roleProj r

@[simp]

theorem MIPStarRE.LDT.roleProj_A_mul_B : roleProj Role.A * roleProj Role.B = 0

@[simp]

theorem MIPStarRE.LDT.roleProj_B_mul_A : roleProj Role.B * roleProj Role.A = 0

noncomputable def MIPStarRE.LDT.roleCond {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : Role) (X : Quantum.Op ι) : Quantum.Op (Role × ι)

Tensor an operator with the role projector selecting the r block.

Equations

• MIPStarRE.LDT.roleCond r X = MIPStarRE.LDT.opTensor (MIPStarRE.LDT.roleProj r) X

noncomputable def MIPStarRE.LDT.roleBlock {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : Role) (Y : Quantum.Op (Role × ι)) : Quantum.Op ι

Principal role block of an operator on the role-register local space.

Equations

• MIPStarRE.LDT.roleBlock r Y = Matrix.submatrix Y (fun (i : ι) => (r, i)) fun (i : ι) => (r, i)

theorem MIPStarRE.LDT.roleCond_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : Role) {X : Quantum.Op ι} (hX : 0 ≤ X) : 0 ≤ roleCond r X

@[simp]

theorem MIPStarRE.LDT.roleCond_mul_same {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : Role) (X Y : Quantum.Op ι) : roleCond r X * roleCond r Y = roleCond r (X * Y)

@[simp]

theorem MIPStarRE.LDT.roleCond_A_mul_B {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X Y : Quantum.Op ι) : roleCond Role.A X * roleCond Role.B Y = 0

@[simp]

theorem MIPStarRE.LDT.roleCond_B_mul_A {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X Y : Quantum.Op ι) : roleCond Role.B X * roleCond Role.A Y = 0

theorem MIPStarRE.LDT.roleCond_finset_sum {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (r : Role) (s : Finset α) (f : α → Quantum.Op ι) : ∑ a ∈ s, roleCond r (f a) = roleCond r (s.sum f)

@[simp]

theorem MIPStarRE.LDT.roleCond_one_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] : roleCond Role.A 1 + roleCond Role.B 1 = 1

def MIPStarRE.LDT.roleRegisterPairLocalEquiv (ι : Type u_1) : (Role × Role) × ι × ι ≃ (Role × ι) × Role × ι

Reassociate the role and local-space indices for the role-register symmetrization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.rolePairProj (rL rR : Role) : Quantum.Op (Role × Role)

Basis projector onto a pair of role sectors.

Equations

• MIPStarRE.LDT.rolePairProj rL rR = MIPStarRE.LDT.opTensor (MIPStarRE.LDT.roleProj rL) (MIPStarRE.LDT.roleProj rR)

theorem MIPStarRE.LDT.rolePairProj_mul_eq_zero_of_ne (rL rR sL sR : Role) (h : (rL, rR) ≠ (sL, sR)) : rolePairProj rL rR * rolePairProj sL sR = 0

Distinct role-pair sectors have zero product.

@[simp]

theorem MIPStarRE.LDT.rolePairProj_AB_mul_BA : rolePairProj Role.A Role.B * rolePairProj Role.B Role.A = 0

Orthogonal role-pair sectors AB and BA have zero product.

@[simp]

theorem MIPStarRE.LDT.rolePairProj_BA_mul_AB : rolePairProj Role.B Role.A * rolePairProj Role.A Role.B = 0

Orthogonal role-pair sectors BA and AB have zero product.

noncomputable def MIPStarRE.LDT.rolePairCond {ι : Type u_1} [Fintype ι] [DecidableEq ι] (rL rR : Role) (X : Quantum.Op (ι × ι)) : Quantum.Op ((Role × ι) × Role × ι)

Reindex a bipartite local-space operator into the (Role × ι) local spaces and restrict it to the selected role sector.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.rolePairProj_nonneg (rL rR : Role) : 0 ≤ rolePairProj rL rR

The projection onto a pair of role sectors is positive semidefinite.

theorem MIPStarRE.LDT.swapDensity_pureDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : ι × ι → ℂ) : swapDensity (pureDensity ψ) = pureDensity (swapVector ψ)

Swapping the density of a rank-one pure state swaps the underlying state vector.

noncomputable def MIPStarRE.LDT.classicalRoleSymmState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) : QuantumState ((Role × ι) × Role × ι)

Classical role-register symmetrization of a bipartite state.

The A/B sector carries the original state, while the B/A sector carries the swapped state. The scalar 2 on each occupied role sector compensates for the normalized-trace convention on the enlarged ambient space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.classicalRoleSymmState_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) : swapDensity (classicalRoleSymmState ψ).density = (classicalRoleSymmState ψ).density

theorem MIPStarRE.LDT.normalizedTrace_rolePairProj (rL rR : Role) : Quantum.normalizedTrace (rolePairProj rL rR) = 1 / 4

The normalized trace of a two-role sector projection is 1 / 4.

theorem MIPStarRE.LDT.normalizedTrace_two_smul_rolePairCond {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (rL rR : Role) (X : Quantum.Op (ι × ι)) : Quantum.normalizedTrace (2 • rolePairCond rL rR X) = 1 / 2 * Quantum.normalizedTrace X

theorem MIPStarRE.LDT.normalizedTrace_re_two_smul_rolePairCond {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (rL rR : Role) (X : Quantum.Op (ι × ι)) : (Quantum.normalizedTrace (2 • rolePairCond rL rR X)).re = 2⁻¹ * (Quantum.normalizedTrace X).re

theorem MIPStarRE.LDT.permInvState_of_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hfix : swapDensity ψ.density = ψ.density) : PermInvState ψ

theorem MIPStarRE.LDT.PureState.isSwapInvariant_density_fixed {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState (ι × ι)) (hψ : ψ.IsSwapInvariant) : swapDensity ψ.toQuantumState.density = ψ.toQuantumState.density

A vector-level SWAP-invariant pure state induces the mixed-state symmetry API used throughout the current development.

theorem MIPStarRE.LDT.PureState.isSwapInvariant_permInvState {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : PureState (ι × ι)) (hψ : ψ.IsSwapInvariant) : PermInvState ψ.toQuantumState

A vector-level SWAP-invariant pure state automatically satisfies PermInvState. This is the intended bridge from the paper's pure-state symmetry assumption to the density-matrix API used in Lean.

theorem MIPStarRE.LDT.classicalRoleSymmState_permInvState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) : PermInvState (classicalRoleSymmState ψ)

The classical role-register symmetrized state is permutation-invariant.

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

The classical role-register symmetrized state preserves normalization.

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) : ev (classicalRoleSymmState ψ) 1 = ev ψ 1

The role-register symmetrized state has the same total expectation as the original state.

noncomputable def MIPStarRE.LDT.swapQuantumState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) : QuantumState (ι × ι)

Equations

• MIPStarRE.LDT.swapQuantumState ψ = { density := MIPStarRE.LDT.swapDensity ψ.density, density_psd := ⋯ }

theorem MIPStarRE.LDT.ev_swapQuantumState {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (Z : Quantum.Op (ι × ι)) : ev (swapQuantumState ψ) Z = ev ψ (swapDensity Z)