Word-Probability Trace Representation
Abstract
A finite instrument word has matching operational, Schrödinger-trace, and Heisenberg-effect probabilities.
Theorem 1.1 (Word probability has Schrödinger and Heisenberg trace forms).
Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/WordProbabilityTraceRepresentation.word_probability_trace_representation (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a finite word of completely positive instrument branches, the operational probability is evaluated recursively on the current subnormalized branch state. It equals the trace after the full Schrödinger fold.
A supplied trace-duality law pulls each branch back in reverse order. The resulting effect is the imported canonical sequential word effect, obtained by applying the Heisenberg branches to the identity effect.
The formula displays the canonical conversion from the raw Hermitian word effect to the C-star matrix carrier used by the branch maps. This is a data-preserving matrix equivalence, not an implicit change of carrier.
References
- Truth anchor:
D5/S3/Quantum/Measurement/WordProbabilityTraceRepresentation.word_probability_trace_representation - Dependency: D5/S3/Quantum/Completion/SequentialWordObservationResidual
- Dependency: D5/S3/Quantum/Divergence/QuantumRelativeEntropyDefectComposition
- Dependency: D5/S3/Quantum/Fibers/OperatorSystemTowerStability