Pure-qubit affine geometry

Abstract

A rank-two affine measurement of a pure qubit curve has a strict arc parametrization.

Throughout, Jm denotes the finite index set Fin m; a subscript j denotes evaluation at j. Matrices are complex, PSD means positive semidefinite, and 1n is the identity on the indicated finite index set. C1(I) means continuously differentiable on I over the reals. Preconnected means that I cannot be separated into two nonempty relatively open sets; it does not require I to be nonempty. D2 is the canonical space of positive trace-one qubit density states, and mat recovers the underlying matrix. All unspecified scalar arguments in the definitions below are real. In radiusMap and extendedCost, w is a function from the reals to the reals; in root, upperDiag and effect it is a real scalar. Division by zero and the real square root use their total real conventions: a zero denominator gives zero and the square root of a negative number is zero.

For spectralQFI, U is the eigenvector unitary chosen for the Hermitian matrix, and the lambda entries are its eigenvalues. The positivity proof is shown after a semicolon when its quantification matters. A prime denotes the real derivative. In the rank-two statement, the orthonormal basis is indexed by Fin 3 and its coordinate isometry is denoted O with subscript B.

Definition 1.1 (Spectral SLD information).

$\forall n finite, ρ, D \in C^{n \times n}, h : PSD (ρ), U = U_{h}, M = U^{*} D U, spectralQFI (ρ, D; h) = i \in n \sum j \in n \sum \frac{2∣ M _{ij} ∣ ^{2}}{λ _{i} + λ _{j}}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.spectralQFI (✓ std3).

Source. Repository-derived.

Commentary.

The spectral expression uses the chosen Hermitian eigenbasis and assigns zero to terms with zero denominator.

Definition 1.2 (Guarded real infimum).

$\forall S \subseteq R, guardedInfimum (S) = {inf S 0 S \neq = \emptyset \land BddBelow (S) otherwise$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.guardedInfimum (✓ std3).

Source. Repository-derived.

Commentary.

Real infimum with explicit nonempty and bounded-below guard.

Definition 1.3 (Canonical density-state bridge).

$\forall M \in C^{2 \times 2}, h : PSD (M), h_{t} : tr (M) = 1, densityBridge (M, h, h_{t}) \in {r \in D_{2} ∣ mat (r) = M}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.densityBridge (✓ std3).

Source. Repository-derived.

Commentary.

The bridge constructs the canonical density state represented by the given positive trace-one matrix; its subtype includes the exact recovered-matrix equality.

Definition 1.4 (Full actual program class).

$\forall m \in N, p, v : J_{m} \to R, R, Q \in R, N : J_{m} \to C^{2 \times 2}, ρ : R \to C^{2 \times 2}, I \subseteq R, IsProgram (p, v, R, N, ρ, I, Q) \Leftrightarrow Open (I) \land Preconnected (I) \land [- R, R] \subseteq I \land (\forall j \in J_{m}, PSD (N_{j})) \land j \in J_{m} \sum N_{j} = 1_{2} \land ρ \in C^{1} (I) \land (\forall u \in I, PSD (ρ (u)) \land tr (ρ (u)) = 1 \land ρ (u)^{2} = ρ (u) \land \exists r \in D_{2}, mat (r) = ρ (u)) \land (\forall u \in I, \forall j \in J_{m}, tr (N_{j} ρ (u)) = p_{j} + u v_{j} \land 0 < p_{j} + u v_{j}) \land (\forall h : PSD (ρ (0)), spectralQFI (ρ (0), ρ^{'} (0); h) = Q)$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.IsProgram (✓ std3).

Source. Repository-derived.

Commentary.

The predicate quantifies the full finite measurement and pure-curve data. The interval contains the closed radius interval, and the Born equation is an equality in the complex numbers with the real affine value embedded in them. The final clause quantifies over every proof of positivity at zero, exactly as displayed, even for arbitrary real R.

Definition 1.5 (Attainable actual costs).

$costs (p, v, R) = {Q \in R ∣ \exists N, ρ, I, IsProgram (p, v, R, N, ρ, I, Q)}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.costs (✓ std3).

Source. Repository-derived.

Commentary.

The set ranges over all actual programs in the preceding class.

Definition 1.6 (Cost infimum).

$C_{2} (p, v, R) = guardedInfimum (costs (p, v, R))$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.C2 (✓ std3).

Source. Repository-derived.

Commentary.

C2 applies the guarded infimum to the attainable cost set; when the guard fails its value is zero.

Definition 1.7 (Bloch vector).

$bloch (M) = (2 Re M_{01}, - 2 Im M_{01}, Re M_{00} - Re M_{11}) \in R^{3}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.bloch (✓ std3).

Source. Repository-derived.

Commentary.

The three real Bloch coordinates of a two by two matrix.

Definition 1.8 (Bloch matrix).

$blochMatrix (a, r) = \frac{1}{2} (a + r_{2} r_{0} + i r_{1} r_{0} - i r_{1} a - r_{2}) (a \in R, r \in R^{3})$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.blochMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The Hermitian matrix with a specified real trace and Bloch vector.

Definition 1.9 (Visible readout map).

$effectReadout (N) : R^{3} \to R^{J_{m}}, effectReadout (N) (r)_{j} = \frac{⟨ bloch ( N _{j} ) , r ⟩}{2}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.effectReadout (✓ std3).

Source. Repository-derived.

Commentary.

The linear part of the finite measurement readout sends a Bloch vector to its pairings with the effect vectors.

Definition 1.10 (Orthogonal change of Bloch coordinates).

$reframe (O, M) = blochMatrix (Re tr (M), O (bloch (M))) (O : R^{3} \equiv R^{3} orthogonal)$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.reframe (✓ std3).

Source. Repository-derived.

Commentary.

An orthogonal change of the Bloch vector preserves the trace coordinate.

Definition 1.11 (Linear Bloch map).

$blochLinear : C^{2 \times 2} \to_{R} R^{3}, blochLinear (M) = bloch (M)$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.blochLinear (✓ std3).

Source. Repository-derived.

Commentary.

The Bloch coordinates form a real linear map on complex matrices.

Definition 1.12 (Linear change of matrix coordinates).

$reframeLinear (O) : C^{2 \times 2} \to_{R} C^{2 \times 2}, reframeLinear (O) (M) = reframe (O, M)$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.reframeLinear (✓ std3).

Source. Repository-derived.

Commentary.

A fixed orthogonal Bloch frame induces a real linear map on matrices.

Definition 1.13 (Small quadratic root).

$root (p, d, α, e, w) = \frac{2 ( 1 - e ) w ^{2} d ^{2}}{p - α e w d + ( p - α e w d ) ^{2} - 4 e ( 1 - e ) w ^{2} d ^{2}}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.root (✓ std3).

Source. Repository-derived.

Commentary.

The rationalized small root gives the lower diagonal effect coefficient, including zero individual scores.

Definition 1.14 (Radius map).

$radiusMap (B, α, w) (t) = \frac{( 2 t 1 - t ^{2} - ∣ α ∣ t ^{2} ) w ( t ^{2} )}{( 1 + t ) B}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.radiusMap (✓ std3).

Source. Repository-derived.

Commentary.

This real function converts an arc parameter into a radius for the effect-family statement.

Definition 1.15 (Extended family cost).

$extendedCost (B, α, w) (e) = \frac{B}{w ( e ) ^{2}} \frac{4 ( 1 - e )}{4 ( 1 - e ) - α ^{2} e}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.extendedCost (✓ std3).

Source. Repository-derived.

Commentary.

The cost formula extends through the zero transverse parameter for the normalization branch.

Definition 1.16 (Upper diagonal coefficient).

$upperDiag (p, d, α, e, w) = \frac{p - α e w d + ( p - α e w d ) ^{2} - 4 e ( 1 - e ) w ^{2} d ^{2}}{2 ( 1 - e )}$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.upperDiag (✓ std3).

Source. Repository-derived.

Commentary.

The complementary quadratic root determines the upper diagonal effect coefficient.

Definition 1.17 (Actual effect matrix).

$effect (p, d, α, e, w) = (upperDiag (p, d, α, e, w) w d w d root (p, d, α, e, w))$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.effect (✓ std3).

Source. Repository-derived.

Commentary.

The two diagonal coefficients and the normalized direction determine each effect matrix.

Definition 1.18 (Pure-state arc).

$arc (e, x, c, u) = blochMatrix (1, (x + c u, 4 e (1 - e) - (x + c u)^{2}, 1 - 2 e))$

Formalization. D5/S3/Quantum/Information/ActualPureQubitGeometry.arc (✓ std3).

Source. Repository-derived.

Commentary.

The Bloch curve has one affine coordinate, one square-root coordinate, and one constant coordinate.

Theorem 1.19 (Actual rank-two arc and feasible coefficients).

$\forall m \in N, N : J_{m} \to C^{2 \times 2}, ρ : R \to C^{2 \times 2}, p, v : J_{m} \to R, I \subseteq R, Open (I) \land Preconnected (I) \land 0 \in I \land v \neq = 0 \land (\forall j \in J_{m}, PSD (N_{j})) \land j \in J_{m} \sum N_{j} = 1_{2} \land ρ \in C^{1} (I) \land (\forall u \in I, PSD (ρ (u)) \land tr (ρ (u)) = 1 \land ρ (u)^{2} = ρ (u)) \land (\forall u \in I, \forall j \in J_{m}, Re tr (N_{j} ρ (u)) = p_{j} + u v_{j}) \land rank_{R} (effectReadout (N)) = 2 ⟶ \exists B orthonormal basis of R^{3}, \exists x, c, ε, s \in R, \exists A, q, b : J_{m} \to R, 0 < c \land 0 < ε \land ε \leq \frac{1}{2} \land (s = 1 \lor s = - 1) \land (\forall j \in J_{m}, 0 \leq q_{j} \land 0 \leq A_{j} \land b_{j}^{2} \leq A_{j} q_{j} \land b_{j} = v_{j} / c \land A_{j} = (p_{j} - b_{j} x - ε q_{j}) / (1 - ε)) \land j \in J_{m} \sum q_{j} = 1 \land (\forall u \in I, reframe (O_{B}, ρ (u)) = blochMatrix (1, (x + c u, s 4 ε (1 - ε) - (x + c u)^{2}, 1 - 2 ε))) \land (\forall u \in I, (x + c u)^{2} < 4 ε (1 - ε)) \land (\forall R \in R, 0 \leq R \land [- R, R] \subseteq I ⟶ ∣ x ∣ + c R < 4 ε (1 - ε))$

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

Source. Repository-derived.

Commentary.

The basis supplies a fixed coordinate frame. The coefficients and the signed square-root coordinate satisfy exactly the conjunction below; the last bound holds for every nonnegative radius whose closed interval lies in I.

References

Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.C2
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.IsProgram
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.actual_rank_two_parameters
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.arc
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.bloch
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.blochLinear
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.blochMatrix
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.costs
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.densityBridge
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.effect
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.effectReadout
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.extendedCost
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.guardedInfimum
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.radiusMap
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.reframe
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.reframeLinear
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.root
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.spectralQFI
Truth anchor: D5/S3/Quantum/Information/ActualPureQubitGeometry.upperDiag
Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel

Keyboard shortcuts

trureturing — Discovering truth

Pure-qubit affine geometry

Abstract

References