Universal Replacement Capacity Growth

Abstract

Universal replacement extracts an orthonormal purification family and forces inner capacity growth.

Definition 1.1 (Universal single-step replacement).

$$\begin{array}{r}\forall A,B,R:Type,\\ \mathrm{Fintype}\left(A\right),\mathrm{DecidableEq}\left(A\right),\mathrm{Fintype}\left(B\right),\mathrm{Fintype}\left(R\right),\mathrm{DecidableEq}\left(R\right),\\ \forall W:\mathrm{Matrix}\left(B\times R,A,\mathbb{C}\right),tau:\mathrm{DensityState}\left(R\right),\\ \mathrm{UniversalReplacement}\left(W,tau\right):=(\forall rho\in \mathrm{DensityState}\left(A\right),\mathrm{partialTraceFirst}\left(((W\cdot CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right))\cdot \mathrm{conjTranspose}\left(W\right))\right)=CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(tau\right)\right)).\end{array}$$

Formalization. D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth.UniversalReplacement (✓ std3).

Citation. Samuel L. Braunstein and Arun K. Pati (2007). Quantum Information Cannot Be Completely Hidden in Correlations: Implications for the Black-Hole Information Paradox. DOI: 10.1103/PhysRevLett.98.080502.

Commentary.

A, B, and R index the previous inner space, next inner space, and emitted space. The product B times R is the finite coordinate realization of their tensor product. DensityState is the existing positive trace-one CStarMatrix subtype. The displayed CStarMatrix.ofMatrix.symm(val(rho)) is exactly CStarMatrix.ofMatrix.symm rho.val, and conjTranspose is the adjoint. This is equation 55.2: the quantifier ranges over every density input, including coherent superpositions, not only the input basis states.

Theorem 1.2 (Orthonormal extraction and inner capacity).

$$\begin{array}{r}\forall A,B,R:Type,\\ \mathrm{Fintype}\left(A\right),\mathrm{DecidableEq}\left(A\right),\mathrm{Fintype}\left(B\right),\mathrm{Fintype}\left(R\right),\mathrm{DecidableEq}\left(R\right),\\ \forall W:\mathrm{Matrix}\left(B\times R,A,\mathbb{C}\right),tau:\mathrm{DensityState}\left(R\right),\\ \mathrm{UniversalReplacement}\left(W,tau\right)⟹\\ \mathrm{let}M:=CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(tau\right)\right),\\ \mathrm{let}E:=\mathrm{eigenvectorBasis}\left(M\right),lam:=\mathrm{eigenvalues}\left(M\right),\\ \mathrm{let}S:=\{a:R\mid lam\left(a\right)\ne 0\},\\ \mathrm{let}v:A\times S\to \mathrm{EuclideanSpace}\left(\mathbb{C},B\right):=\\ ia\mapsto \mathrm{smul}\left(\mathrm{inv}\left(\mathrm{ofReal}\left(\mathrm{sqrt}\left(lam\left(\mathrm{val}\left(\mathrm{snd}\left(ia\right)\right)\right)\right)\right)\right),\mathrm{toLp}\left(2,b\mapsto \sum _{r\in R}\mathrm{star}\left(E\left(\mathrm{val}\left(\mathrm{snd}\left(ia\right)\right),r\right)\right)\cdot W\left((b,r),\mathrm{fst}\left(ia\right)\right)\right)\right),\\ (\mathrm{Orthonormal}\left(\mathbb{C},v\right))\wedge (\mathrm{card}\left(A\right)\cdot \mathrm{rank}\left(M\right)\le \mathrm{card}\left(B\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth.universal_replacement_capacity_growth (✓ std3). ∎

Citation. Samuel L. Braunstein and Arun K. Pati (2007). Quantum Information Cannot Be Completely Hidden in Correlations: Implications for the Black-Hole Information Paradox. DOI: 10.1103/PhysRevLett.98.080502.

Commentary.

M and S abbreviate the underlying matrix of tau and its nonzero spectral support. The Lean let hPos transports tau.property.1 through CStarMatrix.ofMatrixStarAlgEquiv.symm and Matrix.nonneg_iff_posSemidef.mp. E and lam are exactly hPos.isHermitian.eigenvectorBasis and eigenvalues. Positivity makes every nonzero eigenvalue positive. No spectral or orthogonality hypothesis is added.

In v, fst and snd are the product projections, val removes the support subtype, ofReal casts Real.sqrt into Complex, inv is complex inverse, and smul is complex scalar multiplication. toLp(2, f) is WithLp.toLp 2 f, giving the EuclideanSpace vector. The sum is over all r in R. Thus v is exactly the inverse-square-root normalized contraction of a column of W against the corresponding emitted eigenvector.

Universal replacement on normalized pure inputs first determines the diagonal contraction pairing. Complex polarization, including imaginary-phase superpositions, then gives the cross-input Gram identity. Orthonormality is derived from this identity. The final count binds Mathlib’s orthonormal linear independence and finite dimension bound; matrix rank is the number of nonzero eigenvalues.

The theorem is the exact finite-dimensional no-hiding capacity bound of quantum-reality Theorem 55.2, together with its explicit witness. Equation 55.2 alone is sufficient, so no redundant isometry premise is assumed. This does not assert a result about approximate replacement, small corrections, or arbitrary black-hole models.

References

• Truth anchor: D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth.UniversalReplacement
• Truth anchor: D5/S3/Quantum/Entanglement/UniversalReplacementCapacityGrowth.universal_replacement_capacity_growth
• Dependency: D5/S3/Quantum/Entanglement/LocalObservationPartialTraceEquivalence
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel