Residual Control of Visible Compression

Abstract

Orthogonal residual norms control visible compression defects.

Definition 1.1 (Centered density coordinate).

$$\begin{gathered} \forall d,\rho :\mathrm{Matrix}\left(d,d,\mathbb{C}\right), \\ \mathrm{Density}\left(\rho \right)\Rightarrow \mathrm{densityCoordinate}\left(\rho \right)=\rho -\frac{1}{d}I\in \mathrm{HermitianTraceZero}\left(d\right). \end{gathered}$$

Formalization. D5/S3/Quantum/Tomography/ResidualControlsNaturality.densityCoordinate (✓ std3).

Source. Repository-derived.

Commentary.

A positive semidefinite trace-one matrix is centered at the maximally mixed matrix. Hermiticity and trace normalization place the result in the canonical real trace-zero Hermitian carrier.

Definition 1.2 (Visible compressed dynamics).

$$\begin{gathered} \forall d,S:\mathrm{Submodule}\left(\mathbb{R},\mathrm{HermitianTraceZero}\left(d\right)\right), \\ F:\mathrm{HermitianTraceZero}\left(d\right)\to \mathrm{HermitianTraceZero}\left(d\right),X:\mathrm{HermitianTraceZero}\left(d\right), \\ \mathrm{visibleDynamics}\left(S,F\right)(X)=P_S(F(X)). \end{gathered}$$

Formalization. D5/S3/Quantum/Tomography/ResidualControlsNaturality.visibleDynamics (✓ std3).

Source. Repository-derived.

Commentary.

The visible dynamics is constructed from the ambient map and the named orthogonal projection: apply the ambient dynamics, then project its output back to the visible subspace.

Theorem 1.3 (Orthogonal residual controls the visible compression defect).

$$\begin{array}{c}\forall d,\rho :\mathrm{Matrix}\left(d,d,\mathbb{C}\right),\\ S:\mathrm{Submodule}\left(\mathbb{R},\mathrm{HermitianTraceZero}\left(d\right)\right),F:\mathrm{HermitianTraceZero}\left(d\right)\to \mathrm{HermitianTraceZero}\left(d\right),\\ L:\mathrm{NNReal},X:\mathrm{HermitianTraceZero}\left(d\right),\\ \mathrm{Density}\left(\rho \right)\wedge \mathrm{IsClosed}\left(S\right)\wedge \mathrm{LipschitzWith}\left(L,F\right)\Rightarrow \\ \mathrm{naturalityDefect}\left(P_S,P_S,F,\mathrm{visibleDynamics}\left(S,F\right),X\right)\le L\Vert P_{S^{\perp }}(X)\Vert \wedge \\ \mathrm{naturalityDefect}\left(P_S,P_S,F,\mathrm{visibleDynamics}\left(S,F\right),\mathrm{densityCoordinate}\left(\rho \right)\right)\le L\sqrt{\mathrm{residualMass}\left(S,\mathrm{densityCoordinate}\left(\rho \right)\right)}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/ResidualControlsNaturality.residual_controls_naturality (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let S be a closed subspace of the real trace-zero Hermitian carrier, let F be L-Lipschitz, and let its visible dynamics be the orthogonal compression constructed above.

The public statement contains both source clauses. For every named coordinate X, the compression defect is at most L times the norm of its orthogonal residual. For the centered density coordinate, the same defect is at most L times the square root of the canonical residual mass.

Mathlib’s exact nonexpansiveness theorem for orthogonal projection is composed with the Lipschitz bound for F. Its orthogonal-complement identity identifies the input distance, and the real square-root identity converts the squared residual mass back to its norm.

References

• Truth anchor: D5/S3/Quantum/Tomography/ResidualControlsNaturality.densityCoordinate
• Truth anchor: D5/S3/Quantum/Tomography/ResidualControlsNaturality.residual_controls_naturality
• Truth anchor: D5/S3/Quantum/Tomography/ResidualControlsNaturality.visibleDynamics
• Dependency: D5/S0/Diagonal/Naturality/NaturalityDefectComposition
• Dependency: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence
• Dependency: D5/S3/Quantum/Tomography/ComplementaryContextProbabilityPythagoras