Actual pure-qubit upper family

Abstract

Normalized positive effect matrices and pure-state arcs give a matching upper family.

J is an arbitrary finite outcome index set and Jm is Fin m. All scalars and radius parameters are real. PSD means positive semidefinite, the qubit identity is the two-by-two identity matrix, and P(R) denotes the set of subsets of the real line. The following moment notation is used with the outcome set of each statement; eR is shorthand after the function t has been chosen.

$μ_{3} = \sum_{j} \frac{d _{j}^{3}}{p _{j}^{2}}, μ_{4} = \sum_{j} \frac{d _{j}^{4}}{p _{j}^{3}}, α = - 2 μ_{3}, e_{R} = t (R)^{2}$

root, effect, radiusMap, extendedCost and IsProgram are exactly the functions and full program predicate in ActualPureQubitGeometry. In particular IsProgram includes the canonical density-state realization, positive exact complex Born probabilities, and equality to the spectral cost at zero. The vector written as the square root of B times d is the function taking j to that scalar multiple of d at j. Both limits below are through all positive real radii tending to zero.

Theorem 1.1 (Normalized positive effect family).

$\forall J finite, p, d : J \to R, B \in R, (\forall j \in J, 0 < p_{j}) \land j \in J \sum p_{j} = 1 \land j \in J \sum d_{j} = 0 \land j \in J \sum \frac{d _{j}^{2}}{p _{j}} = 1 \land 0 < B ⟶ \exists w, t : R \to R, w (0) = 1 \land t (0) = 0 \land R \to 0^{+} lim \frac{extendedCost ( B , α , w ) ( t ( R ) ^{2} ) - B}{R ^{2}} = \frac{B ^{2}}{4} (μ_{4} - 1 - μ_{3}^{2}) \land \exists δ > 0, \forall R \in R, 0 < R < δ ⟶ (0 < R \land 0 < t (R) \land t (R) < 1 \land 0 < w (e_{R}) \land j \in J \sum root (p_{j}, d_{j}, α, e_{R}, w (e_{R})) = 1 \land (\forall j \in J, PSD (effect (p_{j}, d_{j}, α, e_{R}, w (e_{R})))) \land j \in J \sum effect (p_{j}, d_{j}, α, e_{R}, w (e_{R})) = 1_{2} \land radiusMap (B, α, w) (t (R)) = R \land (\forall j \in J, 0 < p_{j} - α e_{R} w (e_{R}) d_{j} \land 0 < (p_{j} - α e_{R} w (e_{R}) d_{j})^{2} - 4 e_{R} (1 - e_{R}) w (e_{R})^{2} d_{j}^{2}) \land (\forall j \in J, R (1 + t (R)) ∣ B d_{j} ∣ < p_{j}))$

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

Source. Repository-derived.

Commentary.

The same functions w and t satisfy the initial values, the moment limit, normalization of the small roots and effects, the radius equation, and every strict margin in the displayed conjunction.

Theorem 1.2 (Matching family of actual programs).

$\forall m \in N, p, d : J_{m} \to R, B \in R, (\forall j \in J_{m}, 0 < p_{j}) \land j \in J_{m} \sum p_{j} = 1 \land j \in J_{m} \sum d_{j} = 0 \land j \in J_{m} \sum \frac{d _{j}^{2}}{p _{j}} = 1 \land 0 < B ⟶ \exists N : R \to (J_{m} \to C^{2 \times 2}), ρ : R \to (R \to C^{2 \times 2}), I : R \to P (R), Q : R \to R, R \to 0^{+} lim \frac{Q ( R ) - B}{R ^{2}} = \frac{B ^{2}}{4} (μ_{4} - 1 - μ_{3}^{2}) \land (\exists δ > 0, \forall R \in R, 0 < R < δ ⟶ IsProgram (p, B d, R, N (R), ρ (R), I (R), Q (R)))$

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

Source. Repository-derived.

Commentary.

The functions N, rho, I and Q give actual programs simultaneously for every sufficiently small positive radius, with direction equal to the square root of B times d and the displayed cost limit.

References

Truth anchor: D5/S3/Quantum/Information/ActualPureQubitUpperFamily.actual_effect_family
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitUpperFamily.actual_upper_family
Dependency: D5/S3/Quantum/Information/ActualPureQubitGeometry

Keyboard shortcuts

trureturing — Discovering truth

Actual pure-qubit upper family

Abstract

References