Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Centered Kraus trace norm on finite references

Abstract

A variance budget controls the actual centered Kraus output in ordinary trace norm at every finite reference size.

Theorem 1.1 (The actual rectangular centered family).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/UniformVarianceTraceBound.hermitian_centered_kraus_trace_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let E and F be arbitrary finite-dimensional complex Hilbert spaces, J any finite type, V a complex linear isometric inclusion of E into F, and h(j) Hermitian endomorphisms of the whole ambient F. Suppose delta is nonnegative and the sum of squared ambient variances is at most delta for every unit vector of E. Choose e in E with norm one whenever E admits a unit vector. Set c(j)=Re(inner(Ve,h(j)Ve)) and L(j)=h(j)V-c(j)V. No component of L(j) in the ambient space is discarded.

For each natural reference size n, amplify each same L(j) coordinatewise on the Hilbert L2 sum of n copies. Let v and w be the standard orthonormal bases chosen by stdOrthonormalBasis for these amplified input and output spaces, and M(j) the rectangular matrix of that amplified map. Every complex input matrix X satisfies traceNorm(sum(j) M(j) X M(j) adjoint) at most 5 delta traceNorm(X). The norm is Re Tr sqrt(X adjoint X), with ordinary trace and no factor of one half. Inputs may be non-Hermitian and reference coordinates may be coupled. The empty Kraus family, zero-dimensional spaces, and n=0 are included.

The simultaneous block-centering theorem supplies the 4 delta expectation displacement and 5 delta ambient energy estimates through the coefficient direction and an equal superposition of extremal eigenvectors. Its actual amplified Kraus adjoint has operator norm at most 5 delta times the test operator norm. Unitary trace-norm duality and a singular-value expansion transfer that inequality to the actual matrix Kraus output. Orthonormal coordinates preserve the operator norm; no dimension comparison of matrix norms is used.

Ltwo(Fin(n),E) denotes the Hilbert L2 sum, stdBasis denotes stdOrthonormalBasis, and Ref(n,L) is the complex linear map satisfying Ref(n,L)(x)(r)=L(x(r)). MatrixOf(v,w,R) is LinearMap.toMatrix in the indicated orthonormal bases. FiniteRank is the complex dimension. The anchor condition is vacuous in the zero input space. This result proves the complete-reference trace-norm bridge for one actual centered rectangular family. The conditional global center-pinched map and its defect identity are constructed by hermitian_unital_direct_sum_defect_trace_bound. Obtaining the variance premise from the same S/H selected branches and unreferenced normalized return error, and proving the full local and whole-family bounds of original Theorem 86.1 remain separate obligations.

Theorem 1.2 (The actual defect of a unital Hermitian factor family).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/UniformVarianceTraceBound.hermitian_unital_kraus_defect_trace_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let E be an arbitrary finite-dimensional complex Hilbert space and h(j) Hermitian endomorphisms with sum(j) h(j) composed with h(j) equal to the identity. Assume the same all-unit-vector variance budget delta and anchor condition as above. For every reference size n, H(j) is the matrix of the coordinatewise amplification of the same h(j). With c(j)=Re(inner(e,h(j)e)), M(j)=H(j)-c(j)I and Q=sum(j) M(j) adjoint M(j), the displayed centered defect identity holds for every complex input X.

The identity follows by expanding the actual M(j): the scalar linear terms and quadratic scalar terms cancel in the anticommutator minus the Kraus output. Unitality replaces sum(j) H(j) squared by I. The centered Gram norm is at most 5 delta. Testing the exact defect against a maximizing unitary bounds its two anticommutator terms by 5 delta traceNorm(X) each and its centered Kraus term by 5 delta traceNorm(X); the factor one half gives the stated 10 delta bound. No state restriction, reference dimension, rank factor, or least eigenvalue occurs.

This statement concerns a full matrix factor and includes zero E, empty J whenever its unitality premise holds, and n=0. It does not construct the source CP-TNI selected family or infer the variance premise from beta. Center-dependent scalars in a direct sum require the actual center pinching and its transfer terms; those are outside this factor statement.

Theorem 1.3 (The same globally pinched family on every finite reference).

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/UniformVarianceTraceBound.hermitian_unital_direct_sum_defect_trace_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let H be the actual Hilbert direct sum of an arbitrary finite family of finite-dimensional complex spaces E(i). The same arbitrary Hermitian ambient family h(j) satisfies sum(j) h(j) squared equals I. Assume a nonnegative delta and the ambient variance bound for every unit vector within each input block; no variance premise on vectors mixing centers is imposed. The block anchors are unit whenever their block is nonzero. The theorem quantifies over every natural reference size n, including zero, and every complex input X commuting with all actual amplified center projections P(i). This is exactly the amplified original direct-sum algebra, with arbitrary off-diagonal reference entries.

At each reference, H(j) is the matrix of Ref(h(j)), M(j) the matrix of the same Ref(ell(j)), and C(Y)=sum(i) P(i)Y P(i). The center-dependent c(j) and ell(j)=h(j)-c(j) are those of the centering theorem. Set Q=C(sum(j) M(j) squared), A(j,i,k)=P(k)H(j)P(i), B(j,i,k)=P(k)M(j)P(i), Phi(X)=C(sum(j) H(j)XH(j)), and K(X)=C(sum(j) M(j)XM(j)). These are actual formulas, not assumed conclusions or fields of an auxiliary model.

The conclusions are Q at most 5 delta I in matrix order; sum A adjoint A equals I; sum B adjoint B equals Q; ordinary trace preservation of C on every ambient matrix, and commutation of C(Y) with every P(i). Thus the actual pinching has its range in the original direct-sum algebra. For every legal X, K(X)=sum B X B adjoint, Phi(X)=sum A X A adjoint, X-Phi(X)={Q,X}/2-K(X), and traceNorm(X-Phi(X)) at most min(2,10 delta) traceNorm(X). The ordinary trace of Phi(X) equals that of X, and positivity of X implies positivity of both Phi(X) and K(X) at every reference. For every ambient test Y, Tr(K(X)Y)=Tr(X sum B adjoint Y B). Thus this actual adjoint sends I to Q, and the same Kraus witnesses provide complete positivity and trace preservation of Phi at every reference. No state or Hermiticity restriction is placed on X or Y.

The ambient matrix trace is the ordinary unnormalized trace; center pinching preserves it, giving the sum trace on the embedded direct-sum algebra. The proof never compares that norm to a dimension-weighted surrogate. The live blockwise ambient energy estimate bounds Q and the same K. The central scalars commute with legal X and are scalar at each projection edge; expansion cancels exactly their linear and quadratic cross terms after center pinching. The anticommutator and K give 10 delta on arbitrary complex inputs through trace-norm duality. The actual unital Hermitian family and complete pinching give the independent channel contraction used for the cap 2. Transfers between distinct centers remain in both Q and K.

This proves the conditional global inference in original C109 equations 86.3 through 86.5 and its complete-reference min(2,10 delta) estimate. The source is AURIC_COMPOSITE_COMPARISON_FINITE_WITNESSES_COMMON_QUANTUM_SCALE_V96, Theorem 86.1 proof. The same actual S/H family, support and pseudoinverse normalization, Hermitian Kraus construction, Hilbert-Schmidt spectral bridge and variance premise with delta=beta, and final actual filter and whole-family normalization remain separate open obligations. The original full Theorem 86.1 is not claimed complete. No independent mathematical novelty is assigned to the pinching, trace duality or central cancellation helpers.

References