Actual pure-qubit cost infimum

Abstract

The full finite affine-readout pure-qubit cost infimum has quadratic coefficient one quarter of the weighted score-square projection residual.

Let Jm be Fin m. For positive probabilities p summing to one and a centered nonzero real direction v, define the scores, their second moment B, and their third moment M3 by

$s_j=\frac{v_j}{p_j},B={\sum }_{j\in J_m}{p}_j{s}_j^2={\sum }_{j\in J_m}\frac{v_j^2}{p_j},M_3={\sum }_{j\in J_m}{p}_j{s}_j^3.$

The weighted squared residual after projecting the score square onto the span of the constant function and the score is

$V={\sum }_{j\in J_m}{p}_j{\left(s_j^2-B-\frac{M_3}{B}{s}_j\right)}^2={\sum }_{j\in J_m}{p}_j{s}_j^4-B^2-\frac{M_3^2}{B}.$

Here costs and C2 are the attainable cost set and its guarded real infimum from ActualPureQubitGeometry, with the full IsProgram predicate there. BddBelow(S) means that S has a real lower bound. IsGLB(S,c) means that c is a lower bound and every real lower bound is at most c:

$\mathrm{BddBelow}(S)\iff \exists b\in \mathbb{R},\forall q\in S,b\le q,\mathrm{IsGLB}(S,c)\iff (\forall q\in S,c\le q)\wedge (\forall b\in \mathbb{R},(\forall q\in S,b\le q)\Rightarrow b\le c).$

All radii in the statement are real. The right limit is through every positive real radius tending to zero, and the three eventual properties hold together on one positive interval.

Theorem 1.1 (Exact quadratic infimum coefficient).

$$\begin{array}{rl}& \forall m\in \mathbb{N},p,v:J_m\to \mathbb{R},\\ & (\forall j\in J_m,0<p_j)\wedge \sum _{j\in J_m}{p}_j=1\wedge \sum _{j\in J_m}{v}_j=0\wedge v\ne 0\\ & \wedge (\exists i,j,k\in J_m,s_i\ne s_j\wedge s_i\ne s_k\wedge s_j\ne s_k)\\ & ⟶0<V\\ & \wedge (\exists \delta >0,\forall R\in \mathbb{R},0<R<\delta ⟶\\ & \mathrm{costs}(p,v,R)\ne \varnothing \wedge \mathrm{BddBelow}(\mathrm{costs}(p,v,R))\wedge \mathrm{IsGLB}(\mathrm{costs}(p,v,R),C_2(p,v,R)))\\ & \wedge \underset{R\to 0^{+}}{\lim }\frac{C_2(p,v,R)-B}{R^2}=\frac{V}{4}\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/ActualPureQubitCostInfimum.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary finite positive probability data, a nonzero centered direction, and at least three distinct scores, the residual is positive and the normalized infimum excess tends to one quarter of that residual as real positive radii tend to zero. Repeated and zero individual scores are allowed. Cubic approximate minimizers suffice; no optimum is assumed attained. This result makes no two-score attainment or unrestricted CPTP processor equivalence claim.

The lower bound uses the joint limit of feasible rank-two coefficients: positivity, normalization, and the spectral cost equation exclude a positive limiting transverse parameter when three scores are distinct. The remaining diagonal coefficients converge to the normalized weighted score squares. An exact matching inequality then gives the quadratic lower coefficient. The rank-one branch has a fixed positive cost gap, and a smooth family of actual programs supplies the matching upper bound.

References

• Truth anchor: D5/S3/Quantum/Information/ActualPureQubitCostInfimum.result
• Dependency: D5/S3/Quantum/Information/ActualPureQubitFisherRank
• Dependency: D5/S3/Quantum/Information/ActualPureQubitUpperFamily