Complete Context Collision Conservation

Abstract

Complete complementary rank-one measurements conserve collisions at operator and scalar level.

Theorem 1.1 (Complete context collision conservation).

$$\begin{gathered} \forall n:Nat,C:\mathrm{Fin}(n+2)\to \mathrm{RankOneContext}(n+1),\rho :\mathrm{Matrix}(\mathrm{Fin}(n+1),\mathrm{Fin}(n+1),\mathbb{C}), \\ (\forall l:\mathrm{Fin}(n+2),\mathrm{IsRecordMeasurement}(\mathrm{projector}(C_l)))\wedge \\ (\forall l,k:\mathrm{Fin}(n+2),j,r:\mathrm{Fin}(n+1), \\ \mathrm{Tr}(\mathrm{projector}(C_l,j)\cdot \mathrm{projector}(C_k,r))=\mathrm{if}(l=k,\mathrm{if}(j=r,1,0),\frac{1}{n+1}))\wedge \\ \mathrm{PosSemidefinite}(\rho )\wedge \mathrm{Tr}(\rho )=1\Rightarrow \\ (\sum _l\sum _j\mathrm{Kronecker}(\mathrm{projector}(C_l,j),\mathrm{projector}(C_l,j))=I_{\mathrm{Matrix}((\mathrm{Fin}(n+1)\times \mathrm{Fin}(n+1)),(\mathrm{Fin}(n+1)\times \mathrm{Fin}(n+1)),\mathbb{C})}+\mathrm{PermMatrix}(\mathrm{prodComm}(\mathrm{Fin}(n+1),\mathrm{Fin}(n+1))))\wedge \\ (\sum _l\sum _j\mathrm{basisProbability}(\rho ,C_l,j{)}^2=1+\mathrm{ReTr}({\rho }^2)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CompleteContextCollisionConservation.complete_context_collision_conservation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take n+2 complete rank-one record measurements in dimension n+1. Their public trace-overlap equation states orthogonality within each context and inverse-dimension overlap between contexts.

The frozen complete-context tomography theorem separates matrices by their projector traces. Applying that separator to the induced frame map and then evaluating on matrix units gives the operator identity with the canonical coordinate-swap permutation matrix.

The scalar collision clause is the frozen complete-context purity identity applied to the same context family and density matrix. Prime-dimensional Weyl context families are instances of these public complete-context hypotheses.

References

• Truth anchor: D5/S3/Quantum/Measurements/CompleteContextCollisionConservation.complete_context_collision_conservation
• Dependency: D5/S3/Quantum/Measurements/CompleteContextPurityIdentities