Five-mode local density fibres
Abstract
Full-rank five-mode density fibres and their affine coordinates.
Theorem 1.1 (The full-rank mean fibre has 21 real local dimensions).
Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/FiveModeDensityFiber.full_rank_local_fibre (✓ std3). ∎
Source. Repository-derived.
Commentary.
The ordered modes are empty, one, two, three, and thirteen. The three means, ordered X,Z,Y, are rho(1,1)+rho(4,4), rho(2,2), and rho(3,3)+rho(4,4), with real parts understood. Trace-zero Hermitian five-by-five matrices have real dimension 24, by BipartiteSectorDecomposition.trace_zero_hermitian_finrank. Explicit diagonal trace-zero matrices independently realize the three means, so the kernel has dimension 21.
For any positive-definite trace-one rho, every Hermitian matrix with trace one and the same means is uniquely rho+h with h in that kernel. Positive semidefiniteness is still a restriction on these affine coordinates. The real spectrum of rho has a strictly positive lower bound epsilon. A self-adjoint perturbation h satisfies minus its C-star operator norm times the identity <= h. Consequently every kernel perturbation with operator norm below epsilon remains positive definite, with unchanged trace and means. This gives an open 21-dimensional neighbourhood within the affine fibre at each full-rank point. The scalar identity divided by five is one such point. The conclusion does not impose the same dimension on lower-rank boundary fibres.
Writing kappa=rho(4,4), the diagonal probabilities are 1-X-Z-Y+kappa, X-kappa, Z, Y-kappa, and kappa. The single diagonal direction kappa is independent of the ten complex off-diagonal Hermitian coordinates, which supply twenty real directions. Positivity constrains both sets of coordinates jointly.
The pure states generated by (mode-one+mode-three)/sqrt(2) and (mode-one-mode-three)/sqrt(2) have X=Y=1/2, Z=kappa=0. They give expectations +1 and -1 for the self-adjoint observable C13=|one><three|+|three><one|. Thus three means do not determine this coherent readout. C13 is an observable with signed expectation; it is not a positive quantum effect. The empty mode is a nonzero basis vector. The probability-coordinate equalities and both positive trace-one coherence matrices are exact finite-matrix applications, rather than separately retained theorem wrappers.
The full reference star at arbitrary rank
The arbitrary-rank star certificate of Theorem 11.11 in AURIC FIB-ATOM: observation graphs, purity certification and stable future response - continuation is an application to the same ordered five-mode matrix carrier. Fin 5 indices 0,1,2,3,4 denote source modes 0,1,2,3,13. Let rho be any complex positive semidefinite matrix of trace one. Its diagonal is real; write Z=Re rho(2,2)>0, so rho(2,2)=Z. Set Cij=rho(j,i). All four reference coherences Ci2, i different from 2, and every quantity below belong to this single rho. No fixed means or rank assumption enters this application.
Define v_i=rho(i,2)/sqrt(Z), V=vv*, R=rho-V, and epsilon=1-Z-Z^(-1) sum_(i different from 2) |Ci2|^2. Here the vector norm is Euclidean, and the star on a vector denotes its conjugate transpose in an outer product. Hermiticity gives v_i=conj(Ci2)/sqrt(Z), including v_2=sqrt(Z). Thus the reference star and Z determine this actual vector, rather than an independently chosen completion.
Matrix.PosDef.fromBlocks₁₁ supplies residual positivity. Its scalar positive block is the one-by-one diagonal matrix Z, its row block is B_j=rho(2,j), and its remaining block is rho. The whole block matrix is a positive semidefinite submatrix of rho with reference index 2 repeated: use the map from Unit plus Fin 5 that sends Unit to 2 and Fin 5 identically to itself. The Schur residual rho-B* Z^(-1) B is exactly R. This use of the generic Schur result requires invertibility only of the positive scalar Z. Entrywise normalization also gives R(i,2)=0.
UniversalReplacementCapacityGrowth.pure_trace identifies tr(V) with the squared Euclidean norm of v. Separating reference coordinate 2 in the finite sum gives ||v||^2=Z+Z^(-1) sum_(i different from 2) |Ci2|^2 =1-epsilon and tr(R)=epsilon. Positivity of R and nonnegativity of the sum yield 0<=epsilon<=1-Z<1 and ||v||^2>=Z>0. Define psiHat=v/||v|| and P=|psiHat><psiHat|. The vector psiHat has norm one; FiniteDiamondDistance.pureState gives precisely the density matrix P.
Purity here has the concrete meaning FiniteDiamondDistance.IsPure: rho is an outer product uu*. If epsilon=0, the positive matrix R has trace zero, so Matrix.PosSemidef.trace_eq_zero_iff gives R=0 and rho=vv*. Conversely, for rho=uu*, the identity u_2 conj(u_2)=Z makes vv*=rho by the same reference-column normalization. Hence R=0 and epsilon=0. Both directions apply to every positive semidefinite trace-one rho with positive reference probability.
Only when epsilon>0 define sigma=epsilon^(-1) R. Positive scalar multiplication and tr(R)=epsilon make this actual sigma a density matrix. Normalization of v gives V=(1-epsilon)P and therefore rho=(1-epsilon)P+epsilon sigma. For the halved trace-norm distance of FiniteTraceDistance.traceDistance, scalar homogeneity gives D(rho,P)=epsilon D(sigma,P)<=epsilon. The suppliers are ConicalDesignConcurrenceComparability.traceNorm_smul_nonneg and FiniteTraceDistance.traceDistance_le_one; their trace norm and density carriers are used without changing normalization. At epsilon=0 no normalized-residual sigma is required. Z=1, arbitrary rank, and zero nonreference coherences or amplitudes are included; only Z=0 is excluded.
The full reference star is {02,12,32,(13)2}. Reversing an edge conjugates Cij, so the signed reported pair (2 Re Cij,2 Im Cij) becomes (2 Re Cij,-2 Im Cij). The source native graph is {01,02,03,1–13,3–13}; it shares only 02 with the star, and their union has eight complex edges. These source labels do not identify the separately labelled ReadoutInstrument windows or supply acquisition of the additional star edges. This is a deterministic consequence of exact entries mutually consistent with one density matrix. It supplies no acquisition, noise, finite-shot confidence or transport assertion.