Manuscript I@2 · I.tex · theorem · 85631fa7

Theorem: Born probabilities

Born laws and destructive projective residuals › Whole-register records precede marginalization · lines 1717–1760 · proof included or linked

I@2#thm:born

Assume diagonal anchoring, $(C)^{⋆}$ , and the readout instances of $(R)^{⋆}$ . Then, for every finite configuration and $S \subseteq L$ ,

P^{S}_{ψ} (κ) = M^{S}_{κ} ψ^{2} .

Proof. First let $S = L$ . The source

t_{L, *} = let x = Enter (q_{L}) in ⟨ *, x ⟩

is well typed because no complementary quantum names remain.

Write $ψ = \sum_{j} a_{j} ∣ j ⟩_{L}$ . Before record readout, the deferred program has vector

Ψ^{'} = j \sum a_{j} ∣ j ⟩_{L} ∣ j ⟩_{R} .

Its record reduction is

ρ_{R} = j \sum ∣ a_{j} ∣^{2} ∣ j ⟩ ⟨ j ∣ .

Diagonal anchoring gives record law $∣ a_{j} ∣^{2}$ . The readout record equation identifies this with $P^{L}_{ψ} (j)$ .

For a proper subset, composability gives

P^{S}_{ψ} (κ) = λ \in {0, 1}^{L ∖ S} \sum P^{L}_{ψ} (κ, λ) = λ \sum ∣ a_{κλ} ∣^{2} = M^{S}_{κ} ψ^{2} .

No partial-register record test with omitted spectators is used.

Displayed formulas in this passage

unlabeled · line 1722
$P^{S}_{ψ} (κ) = M^{S}_{κ} ψ^{2} .$
unlabeled · line 1730
$t_{L, *} = let x = Enter (q_{L}) in ⟨ *, x ⟩$
unlabeled · line 1738
$Ψ^{'} = j \sum a_{j} ∣ j ⟩_{L} ∣ j ⟩_{R} .$
unlabeled · line 1742
$ρ_{R} = j \sum ∣ a_{j} ∣^{2} ∣ j ⟩ ⟨ j ∣ .$
unlabeled · line 1750
$P^{S}_{ψ} (κ) = λ \in {0, 1}^{L ∖ S} \sum P^{L}_{ψ} (κ, λ) = λ \sum ∣ a_{κλ} ∣^{2} = M^{S}_{κ} ψ^{2} .$