Root Fidelity and Binary Preparation

Abstract

Matrix root-fidelity identities and binary preparation estimates used by commuting midpoint contraction.

These matrix identities and preparation estimates are the foundation of commuting qubit midpoint contraction. The weighted-root norm identity has arbitrary finite decidable indices and no trace normalization. The qubit quotient allows singular density inputs; only its reference is positive definite. The half-order estimate needs no trace normalization on its second PSD matrix.

Definition 1.1 (Root fidelity).

$$\forall (n:Type)[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)](S,T:\mathrm{Matrix}\left(n,n,\mathbb{C}\right)),U\left(S,T\right)=\Re (\mathrm{tr}\left(\sqrt{\sqrt{S}T\sqrt{S}}\right))$$

Formalization. D5/S3/Quantum/CommutingMidpoint/Fidelity.rootFidelity (✓ std3).

Citation. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For matrices on any finite decidable index type, U(S,T) is the real trace of sqrt(sqrt(S) T sqrt(S)). This is root fidelity, without a final square.

Theorem 1.2 (The weighted-root norm identity).

$$\forall (n:Type)[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)](S,V,T:\mathrm{Matrix}\left(n,n,\mathbb{C}\right)),\mathrm{PSD}\left(S\right)\wedge \mathrm{PSD}\left(V\right)\wedge \mathrm{PD}\left(T\right)\Rightarrow B\left(T,S,V\right)=\Vert \mathrm{inv}\left(\sqrt{T}\right)(\sqrt{\sqrt{T}S\sqrt{T}}-\sqrt{\sqrt{T}V\sqrt{T}}){\Vert }^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint/Fidelity.bures_eq_weighted_root_norm_sq (✓ std3). ∎

Citation. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For every finite decidable index type, PSD S,V and PD T, B(T,S,V) equals the squared Frobenius norm displayed above. No trace normalization is required. Expand the norm using the Frobenius trace identity. The diagonal terms are tr(S), tr(V); the two cross terms have equal real parts because they are conjugate traces. This proves nonnegativity even for singular S or V.

Theorem 1.3 (The actual qubit quotient).

$$\forall (S:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(V:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(T:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),\mathrm{PSD}\left(S\right)\wedge \mathrm{tr}\left(S\right)=1\wedge \mathrm{PSD}\left(V\right)\wedge \mathrm{tr}\left(V\right)=1\wedge \mathrm{PD}\left(T\right)\wedge \mathrm{tr}\left(T\right)=1\Rightarrow 0<U\left(T,S\right)\wedge 0<U\left(T,V\right)\wedge \Re (F\left(T,S,V\right))=\frac{U{\left(T,S\right)}^2+U{\left(T,V\right)}^2+U{\left(S,V\right)}^2-1}{2U\left(T,S\right)U\left(T,V\right)}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint/Fidelity.qubit_root_fidelity_quotient (✓ std3). ∎

Citation. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Put a=U(T,S), b=U(T,V), c=U(S,V). For every pair of qubit density matrices and every trace-one PD reference T, a and b are strictly positive and the real ordered fidelity is the stated quotient. The proof uses the two-dimensional trace recurrence for actual matrix square roots and determinants, including singular S,V.

Definition 1.4 (Binary root fidelity).

$$\forall (p:\mathbb{R})(q:\mathbb{R}),H\left(p,q\right)=\sqrt{pq}+\sqrt{(1-p)(1-q)}$$

Formalization. D5/S3/Quantum/CommutingMidpoint/Fidelity.binaryFidelity (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

H(p,q)=sqrt(pq)+sqrt((1-p)(1-q)); its probabilistic uses have p,q in [0,1].

Theorem 1.5 (A half-order lower bound).

$$\forall (S:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(T:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),\mathrm{PSD}\left(S\right)\wedge \mathrm{tr}\left(S\right)=1\wedge \mathrm{PSD}\left(T\right)\wedge \mathrm{PSD}\left(T-\frac{1}{2}S\right)\Rightarrow \frac{1}{2}\le U{\left(T,S\right)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint/Fidelity.fidelity_sq_lower_bound_from_half_order (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For every density S and PSD T with T-S/2 PSD, U(T,S) squared is at least one half. Congruence by sqrt(S), operator monotonicity of sqrt, and positivity of trace give U(S,T)>=sqrt(1/2). The actual qubit formula proves symmetry U(S,T)=U(T,S). There is no invertibility assumption on S and no trace-one requirement on T.

Theorem 1.6 (Classical binary preparation).

$$\forall (p:\mathbb{R})(q:\mathbb{R})(x:\mathbb{R})(y:\mathbb{R}),0\le p\le 1\wedge 0\le q\le 1\wedge 0\le x\le 1\wedge 0\le y\le 1\Rightarrow H\left(p,q\right)\le H\left(px+(1-p)y,qx+(1-q)y\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint/Fidelity.classical_binary_preparation_fidelity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For all p,q,x,y in the closed unit interval, preparing binary probabilities x,y with mixing probabilities p,q cannot decrease H. Apply Cauchy-Schwarz to each coordinate and add the two inequalities. Zero probabilities are included.

References

• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.binaryFidelity
• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.bures_eq_weighted_root_norm_sq
• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.classical_binary_preparation_fidelity
• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.fidelity_sq_lower_bound_from_half_order
• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.qubit_root_fidelity_quotient
• Truth anchor: D5/S3/Quantum/CommutingMidpoint/Fidelity.rootFidelity
• Dependency: D5/S0/Observation/MatrixTracePowerSum
• Dependency: D5/S3/Quantum/GNSMatrix
• Dependency: D5/S3/Quantum/GeneralizedFidelity
• Dependency: D5/S3/Quantum/Information/ActualQubitChordObstruction