Section 7 hypercube graph: trace-form foundations

This file provides the abstract theorem statements and trace-form identities used to formalize the local and global variance rewrites in Section 7 of the LDT paper. The concrete matrix-realization statements are proved first; the public-facing statements in MIPStarRE.LDT.ExpansionHypercubeGraph.Theorems.Results then specialize these identities to arbitrary finite-dimensional operator families.

References

• references/ldt-paper/expansion.tex, especially lem:local-rewrite and lem:global-rewrite
• blueprint/src/chapter/ch05_expansion.tex

Statement structures and matrix realization

structure MIPStarRE.LDT.ExpansionHypercubeGraph.LocalRewriteStatement {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Prop

Paper origin: references/ldt-paper/expansion.tex:145-178 (\label{lem:local-rewrite}).

Conclusion statement for lem:local-rewrite: the local variance is rewritten as a trace-form expectation in the operator family A.

• traceFormula : localVariance params A ψ = localVarianceTraceForm params A ψ

  The local variance agrees with the trace form built from the Laplacian.

structure MIPStarRE.LDT.ExpansionHypercubeGraph.GlobalRewriteStatement {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : Prop

Paper origin: references/ldt-paper/expansion.tex:179-269 (\label{lem:global-rewrite}).

Conclusion statement for lem:global-rewrite: the global variance is rewritten as a trace-form expectation along the eigenbasis of the hypercube graph Laplacian.

• decomposition : ∃ (decomp : GlobalVarianceDecomposition params A), globalVariance params A ψ = globalVarianceTraceForm params A ψ decomp

  A Fourier-mode decomposition whose trace form recovers the global variance.

def MIPStarRE.LDT.ExpansionHypercubeGraph.abstractMatrixModel {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) [Nonempty ι] : MatrixOperatorFamilyRealization params

Reinterpret an abstract operator family and quantum state as the concrete matrix realization used by the trace-form proof of Section 7.

Equations

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

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.localVariance_eq_zero_of_isEmpty {ι : Type u} [Fintype ι] [DecidableEq ι] (hι : ¬Nonempty ι) (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : localVariance params A ψ = 0

If the ambient outcome type is empty, the abstract local variance is zero.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.globalVariance_eq_zero_of_isEmpty {ι : Type u} [Fintype ι] [DecidableEq ι] (hι : ¬Nonempty ι) (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : globalVariance params A ψ = 0

If the ambient outcome type is empty, the abstract global variance is zero.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.localVarianceTraceForm_eq_zero_of_isEmpty {ι : Type u} [Fintype ι] [DecidableEq ι] (hι : ¬Nonempty ι) (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) : localVarianceTraceForm params A ψ = 0

If the ambient outcome type is empty, the local trace formula vanishes.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.globalVarianceTraceForm_eq_zero_of_isEmpty {ι : Type u} [Fintype ι] [DecidableEq ι] (hι : ¬Nonempty ι) (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) (decomp : GlobalVarianceDecomposition params A) : globalVarianceTraceForm params A ψ decomp = 0

If the ambient outcome type is empty, the global trace formula vanishes.

Finite-sum helper lemmas

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.sum_sum_mul_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [CommSemiring γ] (c : γ) (f : α → β → γ) : ∑ a : α, ∑ b : β, c * f a b = c * ∑ a : α, ∑ b : β, f a b

Factor a common scalar out of a doubly indexed finite sum.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.sum_sum_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid γ] (f g : α → β → γ) : ∑ a : α, ∑ b : β, (f a b + g a b) = ∑ a : α, ∑ b : β, f a b + ∑ a : α, ∑ b : β, g a b

Distribute a doubly indexed sum across pointwise addition.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.sum_sum_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [AddCommGroup γ] (f g : α → β → γ) : ∑ a : α, ∑ b : β, (f a b - g a b) = ∑ a : α, ∑ b : β, f a b - ∑ a : α, ∑ b : β, g a b

Distribute a doubly indexed sum across pointwise subtraction.

Trace witness closed forms

def MIPStarRE.LDT.ExpansionHypercubeGraph.matrixModelState {params : Parameters} (model : MatrixOperatorFamilyRealization params) : QuantumState model.space.carrier

Turn a matrix realization state into the corresponding abstract quantum state.

Equations

• MIPStarRE.LDT.ExpansionHypercubeGraph.matrixModelState model = { density := model.state.matrix, density_psd := ⋯ }

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.normalizedTrace_combined_tensor_eq (params : Parameters) (model : MatrixOperatorFamilyRealization params) (P : MakingMeasurementsProjective.MatrixOperator (pointHilbertSpace params)) : Quantum.normalizedTrace (Matrix.conjTranspose (matrixCombinedOperator params model) * (matrixTensorOperator P model.state.matrix * matrixCombinedOperator params model)) = ∑ u : (pointHilbertSpace params).carrier, ∑ v : (pointHilbertSpace params).carrier, P u v * MakingMeasurementsProjective.matrixExpectation model.state (Matrix.conjTranspose (model.family v) * model.family u)

Expand the normalized trace of the combined tensor witness into its explicit double-sum form.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.globalVarianceTraceForm_eq_orthogonalClosedForm {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) (decomp : GlobalVarianceDecomposition params A) : globalVarianceTraceForm params A ψ decomp = (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ev ψ (Matrix.conjTranspose (decomp.orthogonalComponent u) * decomp.orthogonalComponent u)

Closed form of globalVarianceTraceForm as the average squared norm of the orthogonal residual family carried by the decomposition.

theorem MIPStarRE.LDT.ExpansionHypercubeGraph.globalVarianceTraceForm_eq_closedForm {ι : Type u} [Fintype ι] [DecidableEq ι] (params : Parameters) (A : Point params → Quantum.Op ι) (ψ : QuantumState ι) (decomp : GlobalVarianceDecomposition params A) : globalVarianceTraceForm params A ψ decomp = (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ev ψ (Matrix.conjTranspose (A u) * A u) - (↑(hypercubeVertexCount params))⁻¹ * (↑(hypercubeVertexCount params))⁻¹ * ∑ u : Point params, ∑ v : Point params, ev ψ (Matrix.conjTranspose (A v) * A u)

Closed form of globalVarianceTraceForm in the same centered-correlation coordinates as matrixGlobalVariance_eq_closedForm.