The two-factor joint register: tensor states, partial operators, and the Born marginal

Category: 1-Mathlib (CSD-free).

The product-index register EuclideanSpace ℂ (ι₁ × ι₂) over arbitrary finite factors, with the four pieces every two-register algorithm argument consumes:

• tensorState φ ψ — the product state, coordinate φ c * ψ y, with bilinearity (tensorState_smul_left/right, tensorState_sum_left/right) and |c⟩ ⊗ |y⟩ = |(c,y)⟩ (tensorState_basis).
• matrixLeft M Φ — a matrix kernel acting on the first factor only (the shape of "the inverse QFT on the counting register"), linear (matrixLeft_smul/matrixLeft_sum), with the key reduction ★ matrixLeft_tensorState: on a product state it acts on the first factor and leaves the second alone.
• sliceLeft Φ c — the second-register slice at first-register outcome c, the vector whose norm² is the marginal weight.
• probLeft Φ c — the Born marginal on the first register, ∑_y ‖Φ (c, y)‖²; on a product state it is the product law (probLeft_tensorState), and — the load-bearing fact — ★★ probLeft_sum_tensor_orthogonal: for a sum of product states whose second factors are pairwise orthogonal, the marginal is the mixture of the branch marginals, with every cross-term dead. This is the lemma that turns a multi-branch kickback state into a classical mixture of single-phase distributions.

Extracted 2026-08-29 (plan specs/amplitude-amplification-plan.md, AA-5b step 1) from the Fin T × ZMod N-typed originals in Empirical/QM/Algorithms/ShorCore.lean (tensorCN, qftInvCount, probCount), which are now the instances; the second consumer is the amplitude -estimation kickback marginal (AA-5b), whose two branches have orthogonal eigenvector companions. The mixture lemma is new here — Shor's file never needed the general form, and the 8/π² assembly does.

The tensor state

noncomputable def QuantumInfo.tensorState {ι₁ : Type u_1} {ι₂ : Type u_2} (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : EuclideanSpace ℂ (ι₁ × ι₂)

The tensor product of two register states, as a vector on the product index: coordinate (tensorState φ ψ) (c, y) = φ c * ψ y.

Equations

• QuantumInfo.tensorState φ ψ = (WithLp.equiv 2 (ι₁ × ι₂ → ℂ)).symm fun (p : ι₁ × ι₂) => φ.ofLp p.1 * ψ.ofLp p.2

@[simp]

theorem QuantumInfo.tensorState_apply {ι₁ : Type u_1} {ι₂ : Type u_2} (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) (c : ι₁) (y : ι₂) : (tensorState φ ψ).ofLp (c, y) = φ.ofLp c * ψ.ofLp y

theorem QuantumInfo.tensorState_smul_left {ι₁ : Type u_1} {ι₂ : Type u_2} (k : ℂ) (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : tensorState (k • φ) ψ = k • tensorState φ ψ

The tensor is linear in the first factor.

theorem QuantumInfo.tensorState_sum_left {ι₁ : Type u_1} {ι₂ : Type u_2} {κ : Type u_3} (s : Finset κ) (f : κ → EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : tensorState (∑ k ∈ s, f k) ψ = ∑ k ∈ s, tensorState (f k) ψ

The tensor commutes with finite sums in the first factor.

theorem QuantumInfo.tensorState_smul_right {ι₁ : Type u_1} {ι₂ : Type u_2} (k : ℂ) (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : tensorState φ (k • ψ) = k • tensorState φ ψ

The tensor is linear in the second factor.

theorem QuantumInfo.tensorState_sum_right {ι₁ : Type u_1} {ι₂ : Type u_2} {κ : Type u_3} (φ : EuclideanSpace ℂ ι₁) (s : Finset κ) (f : κ → EuclideanSpace ℂ ι₂) : tensorState φ (∑ k ∈ s, f k) = ∑ k ∈ s, tensorState φ (f k)

The tensor commutes with finite sums in the second factor.

@[simp]

theorem QuantumInfo.tensorState_basis {ι₁ : Type u_1} {ι₂ : Type u_2} [DecidableEq ι₁] [DecidableEq ι₂] (c : ι₁) (y : ι₂) : tensorState (basisState c) (basisState y) = basisState (c, y)

On basis states the tensor is the joint basis state: |c⟩ ⊗ |y⟩ = |(c, y)⟩.

theorem QuantumInfo.tensorState_add_right {ι₁ : Type u_1} {ι₂ : Type u_2} (φ : EuclideanSpace ℂ ι₁) (ψ χ : EuclideanSpace ℂ ι₂) : tensorState φ (ψ + χ) = tensorState φ ψ + tensorState φ χ

The tensor is additive in the second factor.

A matrix kernel on the first factor

noncomputable def QuantumInfo.matrixLeft {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] (M : Matrix ι₁ ι₁ ℂ) (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) : EuclideanSpace ℂ (ι₁ × ι₂)

A matrix kernel acting on the first factor only: coordinate (matrixLeft M Φ) (c, y) = ∑_x M c x · Φ (x, y). This is the shape of "apply the inverse QFT to the counting register of a joint state".

Equations

• QuantumInfo.matrixLeft M Φ = (WithLp.equiv 2 (ι₁ × ι₂ → ℂ)).symm fun (p : ι₁ × ι₂) => ∑ x : ι₁, M p.1 x * Φ.ofLp (x, p.2)

@[simp]

theorem QuantumInfo.matrixLeft_apply {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] (M : Matrix ι₁ ι₁ ℂ) (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) (y : ι₂) : (matrixLeft M Φ).ofLp (c, y) = ∑ x : ι₁, M c x * Φ.ofLp (x, y)

theorem QuantumInfo.matrixLeft_smul {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] (M : Matrix ι₁ ι₁ ℂ) (k : ℂ) (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) : matrixLeft M (k • Φ) = k • matrixLeft M Φ

The partial matrix action is homogeneous.

theorem QuantumInfo.matrixLeft_sum {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] {κ : Type u_3} (M : Matrix ι₁ ι₁ ℂ) (s : Finset κ) (f : κ → EuclideanSpace ℂ (ι₁ × ι₂)) : matrixLeft M (∑ k ∈ s, f k) = ∑ k ∈ s, matrixLeft M (f k)

The partial matrix action commutes with finite sums.

theorem QuantumInfo.toEuclideanLin_coord {ι₁ : Type u_1} [Fintype ι₁] [DecidableEq ι₁] (M : Matrix ι₁ ι₁ ℂ) (φ : EuclideanSpace ℂ ι₁) (c : ι₁) : ((Matrix.toEuclideanLin M) φ).ofLp c = ∑ x : ι₁, M c x * φ.ofLp x

The coordinate of the Euclidean matrix action: (M ψ) c = ∑_x M c x · ψ x.

theorem QuantumInfo.matrixLeft_tensorState {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] (M : Matrix ι₁ ι₁ ℂ) (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : matrixLeft M (tensorState φ ψ) = tensorState ((Matrix.toEuclideanLin M) φ) ψ

★ Key reduction: on a product state, a first-factor kernel acts on the first factor and leaves the second alone: matrixLeft M (φ ⊗ ψ) = (M φ) ⊗ ψ.

theorem QuantumInfo.matrixLeft_add {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] (M : Matrix ι₁ ι₁ ℂ) (Φ Ψ : EuclideanSpace ℂ (ι₁ × ι₂)) : matrixLeft M (Φ + Ψ) = matrixLeft M Φ + matrixLeft M Ψ

The partial matrix action is additive.

The second-register slice and the Born marginal on the first register

noncomputable def QuantumInfo.sliceLeft {ι₁ : Type u_1} {ι₂ : Type u_2} (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) : EuclideanSpace ℂ ι₂

The second-register slice of a joint state at first-register outcome c: the (not normalized) vector y ↦ Φ (c, y) whose norm² is the marginal weight of c.

Equations

• QuantumInfo.sliceLeft Φ c = (WithLp.equiv 2 (ι₂ → ℂ)).symm fun (y : ι₂) => Φ.ofLp (c, y)

@[simp]

theorem QuantumInfo.sliceLeft_apply {ι₁ : Type u_1} {ι₂ : Type u_2} (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) (y : ι₂) : (sliceLeft Φ c).ofLp y = Φ.ofLp (c, y)

theorem QuantumInfo.sliceLeft_sum {ι₁ : Type u_1} {ι₂ : Type u_2} {κ : Type u_3} (s : Finset κ) (f : κ → EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) : sliceLeft (∑ k ∈ s, f k) c = ∑ k ∈ s, sliceLeft (f k) c

Slicing commutes with finite sums.

theorem QuantumInfo.sliceLeft_tensorState {ι₁ : Type u_1} {ι₂ : Type u_2} (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) (c : ι₁) : sliceLeft (tensorState φ ψ) c = φ.ofLp c • ψ

The slice of a product state is the scaled second factor.

noncomputable def QuantumInfo.probLeft {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) : ℝ

The Born marginal on the first register: probLeft Φ c = ∑_y ‖Φ (c, y)‖².

Equations

• QuantumInfo.probLeft Φ c = ∑ y : ι₂, ‖Φ.ofLp (c, y)‖ ^ 2

theorem QuantumInfo.probLeft_nonneg {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) : 0 ≤ probLeft Φ c

theorem QuantumInfo.probLeft_eq_inner {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] (Φ : EuclideanSpace ℂ (ι₁ × ι₂)) (c : ι₁) : ↑(probLeft Φ c) = inner ℂ (sliceLeft Φ c) (sliceLeft Φ c)

The marginal weight is the squared norm of the slice, as an inner product.

theorem QuantumInfo.probLeft_tensorState {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) (c : ι₁) : probLeft (tensorState φ ψ) c = ‖φ.ofLp c‖ ^ 2 * ∑ y : ι₂, ‖ψ.ofLp y‖ ^ 2

The product law: the marginal of a product state is the first-factor Born weight scaled by the second factor's norm².

theorem QuantumInfo.probLeft_sum_tensor_orthogonal {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] {κ : Type u_3} (s : Finset κ) (φ : κ → EuclideanSpace ℂ ι₁) (u : κ → EuclideanSpace ℂ ι₂) (horth : ∀ k ∈ s, ∀ l ∈ s, k ≠ l → inner ℂ (u k) (u l) = 0) (c : ι₁) : probLeft (∑ k ∈ s, tensorState (φ k) (u k)) c = ∑ k ∈ s, ‖(φ k).ofLp c‖ ^ 2 * ∑ y : ι₂, ‖(u k).ofLp y‖ ^ 2

★★ The orthogonal-branch mixture law. For a sum of product states whose second factors are pairwise orthogonal, the Born marginal on the first register is the mixture of the branch marginals — every cross-term dies against the orthogonality. This is what turns a multi-branch kickback state ∑_s φ_s ⊗ u_s (orthogonal eigenvector companions u_s) into a classical mixture of single-branch counting distributions.

theorem QuantumInfo.probLeft_add_tensor_orthogonal {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₂] (φ₁ φ₂ : EuclideanSpace ℂ ι₁) (u₁ u₂ : EuclideanSpace ℂ ι₂) (h12 : inner ℂ u₁ u₂ = 0) (c : ι₁) : probLeft (tensorState φ₁ u₁ + tensorState φ₂ u₂) c = ‖φ₁.ofLp c‖ ^ 2 * ∑ y : ι₂, ‖u₁.ofLp y‖ ^ 2 + ‖φ₂.ofLp c‖ ^ 2 * ∑ y : ι₂, ‖u₂.ofLp y‖ ^ 2

★ The two-branch mixture law: for two product states with orthogonal second factors, the first-register marginal is the sum of the branch marginals — the form the two-eigenvector kickback state consumes.