Disjoint quantum ports and topological-order independence

Abstract

Disjoint quantum ports and topological-order independence

Theorem 1.1 (Actual disjoint Kraus ports interchange on correlated matrices).

$$(\forall I:\mathrm{Type}\left(\right),(\forall J:\mathrm{Type}\left(\right),(\forall O:\mathrm{Type}\left(\right),(\forall P:\mathrm{Type}\left(\right),(\forall M:\mathrm{Type}\left(\right),(\forall N:\mathrm{Type}\left(\right),[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)][\mathrm{Fintype}\left(J\right)][\mathrm{DecidableEq}\left(J\right)][\mathrm{Fintype}\left(O\right)][\mathrm{DecidableEq}\left(O\right)][\mathrm{Fintype}\left(P\right)][\mathrm{DecidableEq}\left(P\right)][\mathrm{Fintype}\left(M\right)][\mathrm{Fintype}\left(N\right)](\forall A:\mathrm{KrausFamily}\left(M,O,I\right),(\forall B:\mathrm{KrausFamily}\left(N,P,J\right),(\forall rho:\mathrm{State}\left(\mathrm{Product}\left(I,J\right)\right),(\mathrm{rightBranch}\left(B,\mathrm{leftBranch}\left(A,rho\right)\right)=\mathrm{leftBranch}\left(A,\mathrm{rightBranch}\left(B,rho\right)\right)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/FiniteCausalPortGraph.disjoint_port_interchange (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Giulio Chiribella; Giacomo M. D’Ariano; Paolo Perinotti (2009). Theoretical framework for quantum networks. DOI: 10.1103/PhysRevA.80.022339. URL: https://arxiv.org/abs/0904.4483v2.

Commentary.

The two branches act as A tensor identity and identity tensor B on the full joint matrix. Rectangular Kronecker multiplication identifies either composed Kraus operator with A tensor B. Interchanging the finite hidden-label sums then proves the equality without requiring a product input or assuming commutation.

Theorem 1.2 (Disjoint quantum ports and topological-order independence).

$$(\forall E:\mathrm{Type}\left(\right),[\mathrm{PartialOrder}\left(E\right)](\forall G:\mathrm{QuantumPortGraph}\left(E\right),(\forall h:\mathrm{Records}\left(\mathrm{Outcomes}\left(G\right)\right),(\forall K:\mathrm{Set}\left(E\right),(\forall L:\mathrm{Set}\left(E\right),(\forall l:\mathrm{List}\left(E\right),(\forall m:\mathrm{List}\left(E\right),(\forall X:\mathrm{State}\left(\mathrm{Cut}\left(G,K\right)\right),(((((\mathrm{IsLowerSet}\left(K\right)\wedge \mathrm{IsLowerSet}\left(L\right))\wedge \mathrm{Finite}\left(L\right))\wedge \mathrm{Exec}\left(K,l,L\right))\wedge \mathrm{Exec}\left(K,m,L\right))⟹(\mathrm{pathMap}\left(\mathrm{Readout}\left(G,h\right),l,X\right)=\mathrm{pathMap}\left(\mathrm{Readout}\left(G,h\right),m,X\right)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/FiniteCausalPortGraph.quantum_schedule_independence (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Giulio Chiribella; Giacomo M. D’Ariano; Paolo Perinotti (2009). Theoretical framework for quantum networks. DOI: 10.1103/PhysRevA.80.022339. URL: https://arxiv.org/abs/0904.4483v2.

Commentary.

Every cut has a finite complex matrix interface. A local instrument has finitely many actual outcomes and hidden Kraus labels, rectangular Kraus matrices, and sum over outcomes and hidden labels of K-adjoint K equal to identity. Its combined channel is the canonical FiniteKrausChannel supplier. Branch matrices are actual sums K X K-adjoint, not abstract state-transforming functions. Cut matrices include joint correlations, reference systems, observers, memories and every environment that can interact again.

Acting on one tensor port uses K tensor identity on the complete joint matrix. Rectangular Kronecker multiplication and exchanging the two finite hidden sums show that two disjoint local operations commute on every matrix, including entangled inputs. PortSquare certifies the individual four edge maps as the two corresponding spectator lifts in explicit tensor coordinates. It supplies neither a diamond equation nor a whole-path interchange law. The diamond is derived from these actual quantum interfaces.

An event chooses its Kraus instrument only from the already available record and its own actual outcome. The derived local diamonds and ConfigurationPathTransport finite-endpoint path theorem imply equality of the complete cut matrix for any two legal topological schedules and a fixed event-indexed actual record. Projecting to a subsystem or an effect preserves that equality. The literal occurrence history is not deleted or identified with the output matrix.

References

• Truth anchor: D5/S3/Quantum/Dynamics/FiniteCausalPortGraph.disjoint_port_interchange
• Truth anchor: D5/S3/Quantum/Dynamics/FiniteCausalPortGraph.quantum_schedule_independence
• Dependency: D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport
• Dependency: D5/S3/ConceptDynamics/PartialIdentification/EnabledPathSwapConnectivity
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel