SupportPerspectiveTransport

Abstract

Signed support transport and ambient unitalization for the supported transformer.

Theorem 1.1 (Domination preserves an enclosing support).

Lean statement: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.support_of_nonneg_le_smul

Proof. Machine-checked in Lean as D5/S3/Quantum/Lieb/SupportPerspectiveTransport.support_of_nonneg_le_smul (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite decidable coordinate type n, let C,D,P be complex n by n matrices with P*=P, P C=C and D PSD. For any real r, if D is at most r C in Loewner order, then P D=D and D P=D. Idempotence of P, strict positivity of r, and complete positivity of a map are not hypotheses.

Theorem 1.2 (Normalize the actual spectral square root).

Lean statement: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.spectral_sqrt_normalization

Proof. Machine-checked in Lean as D5/S3/Quantum/Lieb/SupportPerspectiveTransport.spectral_sqrt_normalization (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite decidable carrier n and PSD Q in M_n(C), let R=sqrt(Q), W=spectralInverseSqrt(Q), and P=spectralSupport(Q). Then R*=R, W*=W, P*=P, P P=P, P R=R, R P=R, P Q=Q, and W Q W=P. These are consumed specializations of the existing singleton square-root Kraus support and normalization results. The empty carrier and Q=0 are included.

Theorem 1.3 (Positive maps preserve support of signed sandwiches).

$$\forall u:\mathrm{Level}(),v:\mathrm{Level}(),n:\mathrm{Type}(u),[\mathrm{Fintype}(n)],[\mathrm{DecidableEq}(n)],m:\mathrm{Type}(v),[\mathrm{Fintype}(m)],[\mathrm{DecidableEq}(m)],Phi:\mathrm{PositiveLinearMap}(\mathbb{C},\mathrm{Matrix}(n,n,\mathbb{C}),\mathrm{Matrix}(m,m,\mathbb{C})),B:\mathrm{Matrix}(n,n,\mathbb{C}),Z:\mathrm{Matrix}(n,n,\mathbb{C}),q:\mathrm{Matrix}(m,m,\mathbb{C}),S:\mathrm{Matrix}(m,m,\mathbb{C}),\mathrm{PSD}(B),\mathrm{Hermitian}(Z),q=\mathrm{spectralSupport}(\mathrm{Phi}(B)),S=\mathrm{Phi}(\mathrm{sqrt}(B)Z\mathrm{sqrt}(B))⟹qS=S=Sq$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Lieb/SupportPerspectiveTransport.positive_map_sandwich_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an arbitrary finite positive complex-linear map Phi, PSD B, and Hermitian Z, put S=Phi(sqrt(B) Z sqrt(B)) and q=spectralSupport(Phi(B)). Then q S = S = S q. Hermitian norm bounds give -norm(Z) Phi(B) <= S <= norm(Z) Phi(B); positivity and zero Gram matrices force support. This argument does not require Z, f(Z), or f(0) to be nonnegative. The support facts are supplied by the existing spectralSupport and spectralInverseSqrt definitions and singleton-sqrt Kraus specializations of SpectralTransposeRecovery.

Theorem 1.4 (Localize CFC through a supported sandwich).

$$\forall u:\mathrm{Level}(),n:\mathrm{Type}(u),[\mathrm{Fintype}(n)],[\mathrm{DecidableEq}(n)],q:\mathrm{Matrix}(n,n,\mathbb{C}),Y:\mathrm{Matrix}(n,n,\mathbb{C}),R:\mathrm{Matrix}(n,n,\mathbb{C}),t:\mathbb{R},f:\mathbb{R}\to \mathbb{R},\mathrm{Hermitian}(q),qq=q,\mathrm{Hermitian}(Y),qY=Y,qR=R,Rq=R⟹R\mathrm{cfc}(f,Y+t(1-q))R=R\mathrm{cfc}(f,Y)R$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Lieb/SupportPerspectiveTransport.cfc_supported_localization (✓ std3). ∎

Source. Repository-derived.

Commentary.

For Hermitian projection q, Hermitian Y with qY=Y, and R satisfying qR=R=Rq, every real t and every real function f satisfy R cfc(f,Y+t(I-q)) R = R cfc(f,Y) R. The proof uses the rectangular intertwining theorem with intertwiner q. No independent block functional-calculus premise is assumed.

Theorem 1.5 (Apply Jensen to an explicit ambient unitalization).

$$\forall u:\mathrm{Level}(),n:\mathrm{Type}(u),[\mathrm{Fintype}(n)],[\mathrm{DecidableEq}(n)],m:\mathrm{Type}(u),[\mathrm{Fintype}(m)],[\mathrm{DecidableEq}(m)],f:\mathbb{R}\to \mathbb{R},Phi:\mathrm{PositiveLinearMap}(\mathbb{C},\mathrm{Matrix}(n,n,\mathbb{C}),\mathrm{Matrix}(m,m,\mathbb{C})),B:\mathrm{Matrix}(n,n,\mathbb{C}),i:n,X:\mathrm{Matrix}(n,n,\mathbb{C}),\mathrm{OperatorConvexOnAll}(u,\mathrm{Ici}(0),f),\mathrm{ContinuousOn}(f,\mathrm{Ici}(0)),\mathrm{PSD}(B),\mathrm{PSD}(X)⟹\mathrm{cfc}(f,\mathrm{ambientUnitalization}(Phi,B,i,X))\le \mathrm{ambientUnitalization}(Phi,B,i,\mathrm{cfc}(f,X))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Lieb/SupportPerspectiveTransport.ambient_unitalized_jensen (✓ std3). ∎

Source. Repository-derived.

Commentary.

For PSD B and any positive complex-linear Phi, define N(Z)=Phi(B)^{+1/2} Phi(sqrt(B) Z sqrt(B)) Phi(B)^{+1/2}. The plus exponent denotes the existing spectral inverse square root, zero on the kernel, not an algebraic inverse. The singleton Kraus normalization gives N(I)=q, with q=spectralSupport(Phi(B)). Choose an input coordinate i and set Theta(Z)=N(Z)+Z_ii (I-q). Coordinate evaluation is a positive unital complex-linear state, so Theta is positive unital, even when Phi(B)=0. The new positive-map Jensen bridge gives cfc(f,Theta(X)) <= Theta(cfc(f,X)) for PSD X, the full all-Hilbert operator-convex supplier and continuity. This is a concrete construction, not a unitality assumption on Phi.

SupportPerspectiveTransformer consumes these interfaces and supplies the exact kernel-inclusion reconstruction, mixed spectral products and final congruence cancellations. The Jensen and transport modules supply positive-map inequalities without a complete positivity hypothesis. Identity regularization and trace data processing remain outside this source endpoint.

References

• Truth anchor: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.ambient_unitalized_jensen
• Truth anchor: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.cfc_supported_localization
• Truth anchor: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.positive_map_sandwich_support
• Truth anchor: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.spectral_sqrt_normalization
• Truth anchor: D5/S3/Quantum/Lieb/SupportPerspectiveTransport.support_of_nonneg_le_smul
• Dependency: D5/S3/Quantum/Lieb/PositiveMapJensen
• Dependency: D5/S3/Quantum/Recovery/SpectralTransposeRecovery