Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite causal schedules as executable quantum relation graphs

Abstract

Finite causal schedules as executable quantum relation graphs

Theorem 1.1 (Finite adaptive programs have a unique normalized static relation solution).

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/FiniteCausalScheduleProtocol.program_graph_correspondence (✓ 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 program is a finite tree of actual normalized Kraus instruments. A child is selected by the observed outcome alone. Independently assigned prefix matrices satisfying only the local equations are uniquely reconstructed from the root, and terminal trace equals the root trace on every input matrix. Positive input gives positive terminal matrices by rectangular Kraus conjugation and finite positive sums.

Theorem 1.2 (Finite causal schedules as executable quantum relation graphs).

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/FiniteCausalScheduleProtocol.causal_schedule_realization (✓ 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 compiler reads a finite legal event schedule. At each step it constructs the actual normalized instrument from the graph Kraus data, branches on its finite observed outcome, extends only the observed record, and recursively compiles the remaining positive event occurrences. Hidden Kraus labels are summed and never control feedback. The resulting Program has concrete finite interfaces and a structurally finite termination bound equal to the schedule length. Every terminal record has this length, and the finite history clock theorem identifies it with the cardinality of the added event occurrences.

Independently assign matrices to all observed-prefix vertices of this executable tree. The graph law contains only neighboring CP equations. Recursion constructs a solution from any input boundary, and induction gives uniqueness. Terminal total trace equals input trace by the canonical CPTP supplier at each node. Early termination is admitted by the stop instruction. A fixed actual record selects an existing compiled terminal whose history is precisely the scheduled observed outcomes and whose full matrix is the original path composite.

For different legal topological schedules compare event-indexed records, rather than their differently ordered output strings. Derived disjoint-port interchange gives the same complete final matrix for every record and therefore the same joint probabilities and reference-boundary readouts. Conversely these local normalized instructions constitute a legal finite adaptive quantum protocol. FiniteInstrumentRelationGraph gives the corresponding construction directly for the canonical protocol Tree, including outcome-dependent dimensions, reference factors, independent ancillary densities, retained returning environments and early leaves.

A finite deterministic causal DAG can be executed in a topological order, as in Chiribella, D’Ariano and Perinotti, Theoretical framework for quantum networks (arXiv:0904.4483v2), Section II.C.1. Finite actual-outcome feedback unrolls it into a finite tree of real instruments; this is a fixed relation graph with a variable at every actual prefix. Finite Kraus representation is the existing quantum-foundation input for CP nodes, while unused external systems remain spectator coordinates and a returning environment remains an active port. All distributions are the prescribed instrument Born probabilities. Static representation does not derive the Born law, permit an infinite output interface, discard a returning environment, or erase positive occurrences.

References