A fixed unit vector and normalization with fallback

theorem CommutingRepetition.StdTracialAlgebra.norm_ι_one (N : StdTracialAlgebra) : ‖N.ι 1‖ = 1

noncomputable def CommutingRepetition.StdTracialAlgebra.unitOr (N : StdTracialAlgebra) (v : N.H) : N.H

Normalize a vector, falling back to the fixed unit vector ι 1 at zero.

Equations

• N.unitOr v = if v = 0 then N.ι 1 else ↑‖v‖⁻¹ • v

theorem CommutingRepetition.StdTracialAlgebra.unitOr_norm (N : StdTracialAlgebra) (v : N.H) : ‖N.unitOr v‖ = 1

theorem CommutingRepetition.StdTracialAlgebra.unitOr_of_ne (N : StdTracialAlgebra) (v : N.H) (hv : v ≠ 0) : N.unitOr v = ↑‖v‖⁻¹ • v

theorem CommutingRepetition.ResolverArena.unitOr_branch {M : StdTracialAlgebra} {I J Af Bf : Type} [Fintype I] [Fintype J] [Fintype Af] [Fintype Bf] {F : I → Af → M.A} {G : J → Bf → M.A} (R : ResolverArena M F G) (σ : M.A) (i : I) (j : J) (hb : R.branch σ i j ≠ 0) : R.N.unitOr (R.branch σ i j) = R.candidate σ i j

theorem CommutingRepetition.RevealDatum.mem_CY_of_ne {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) {j : Fin n} (hj : j ≠ r.i) (hCX : j ∉ r.CX) : j ∈ r.CY

theorem CommutingRepetition.RevealDatum.mem_CX_of_ne {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) {j : Fin n} (hj : j ≠ r.i) (hCY : j ∉ r.CY) : j ∈ r.CX

The labels of a history

noncomputable def CommutingRepetition.TracialStrategy.labelA {n : ℕ} {X Y A B : Type} [Nonempty X] [Nonempty Y] [Nonempty A] (D : Finset (Fin n)) (h : PostTuple n X Y A B D) (x : X) : ALabel n X Y A

The Alice label s = (i, r, x): canonical at {i} ∪ C_X with the live question inserted.

Equations

• CommutingRepetition.TracialStrategy.labelA D h x = CommutingRepetition.aLabel D (insert h.1.i h.1.CX) (Function.update h.2.1 h.1.i x) h.2.2.1 h.2.2.2.1

noncomputable def CommutingRepetition.TracialStrategy.labelB {n : ℕ} {X Y A B : Type} [Nonempty X] [Nonempty Y] [Nonempty B] (D : Finset (Fin n)) (h : PostTuple n X Y A B D) (y : Y) : BLabel n X Y B

The Bob label t = (i, r, y).

Equations

• CommutingRepetition.TracialStrategy.labelB D h y = CommutingRepetition.bLabel D (insert h.1.i h.1.CY) h.2.1 (Function.update h.2.2.1 h.1.i y) h.2.2.2.2

noncomputable def CommutingRepetition.TracialStrategy.barLabelA {n : ℕ} {X Y A B : Type} [Nonempty X] [Nonempty Y] [Nonempty A] (D : Finset (Fin n)) (h : PostTuple n X Y A B D) (y : Y) : ALabel n X Y A

The bar Alice label (eq bar-HK, H̄_{r,y}): canonical at C_X, the live Bob question inserted on the weight side.

Equations

• CommutingRepetition.TracialStrategy.barLabelA D h y = CommutingRepetition.aLabel D h.1.CX h.2.1 (Function.update h.2.2.1 h.1.i y) h.2.2.2.1

noncomputable def CommutingRepetition.TracialStrategy.barLabelB {n : ℕ} {X Y A B : Type} [Nonempty X] [Nonempty Y] [Nonempty B] (D : Finset (Fin n)) (h : PostTuple n X Y A B D) (x : X) : BLabel n X Y B

The bar Bob label (K̄_{r,x}).

Equations

• CommutingRepetition.TracialStrategy.barLabelB D h x = CommutingRepetition.bLabel D h.1.CY (Function.update h.2.1 h.1.i x) h.2.2.1 h.2.2.2.2

theorem CommutingRepetition.TracialStrategy.labelA_histCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] {D : Finset (Fin n)} (t : PostTuple n X Y A B D) : labelA D (histCore t) (t.2.1 t.1.i) = aLabel D (insert t.1.i t.1.CX) t.2.1 t.2.2.1 t.2.2.2.1

The label of the flattened tuple is the posterior's canonical label.

theorem CommutingRepetition.TracialStrategy.labelB_histCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] {D : Finset (Fin n)} (t : PostTuple n X Y A B D) : labelB D (histCore t) (t.2.2.1 t.1.i) = bLabel D (insert t.1.i t.1.CY) t.2.1 t.2.2.1 t.2.2.2.2

theorem CommutingRepetition.TracialStrategy.barLabelA_histCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] {D : Finset (Fin n)} (t : PostTuple n X Y A B D) : barLabelA D (histCore t) (t.2.2.1 t.1.i) = aLabel D t.1.CX t.2.1 t.2.2.1 t.2.2.2.1

theorem CommutingRepetition.TracialStrategy.barLabelB_histCore {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] {D : Finset (Fin n)} (t : PostTuple n X Y A B D) : barLabelB D (histCore t) (t.2.1 t.1.i) = bLabel D t.1.CY t.2.1 t.2.2.1 t.2.2.2.2

The package data over an arena

noncomputable def CommutingRepetition.TracialStrategy.uVec {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : PostTuple n X Y A B D × X) (t : PostTuple n X Y A B D × Y) : R.N.H

u_{st}: the normalized ideal branch, fixed unit vector off the support.

Equations

• S.uVec μ R s t = R.N.unitOr (R.branch S.σ (CommutingRepetition.TracialStrategy.labelA D s.1 s.2) (CommutingRepetition.TracialStrategy.labelB D t.1 t.2))

noncomputable def CommutingRepetition.TracialStrategy.xVec {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : PostTuple n X Y A B D × X) : R.N.H

x_s: the normalized Alice-side branch (φ^A_{r,x}, Bob at the bar).

Equations

• S.xVec μ R s = R.N.unitOr (R.branch S.σ (CommutingRepetition.TracialStrategy.labelA D s.1 s.2) (CommutingRepetition.TracialStrategy.barLabelB D s.1 s.2))

noncomputable def CommutingRepetition.TracialStrategy.yVec {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (t : PostTuple n X Y A B D × Y) : R.N.H

y_t: the normalized Bob-side branch (φ^B_{r,y}, Alice at the bar).

Equations

• S.yVec μ R t = R.N.unitOr (R.branch S.σ (CommutingRepetition.TracialStrategy.barLabelA D t.1 t.2) (CommutingRepetition.TracialStrategy.labelB D t.1 t.2))

noncomputable def CommutingRepetition.TracialStrategy.Apov {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : PostTuple n X Y A B D × X) (a : A) : R.N.A

Alice's answer POVM: the fully refined arena POVM coarse-grained at the live coordinate (eq live-refinements).

Equations

• S.Apov μ R s a = ∑ as : Fin n → A, if as s.1.1.i = a then R.Ameas (CommutingRepetition.TracialStrategy.labelA D s.1 s.2) as else 0

noncomputable def CommutingRepetition.TracialStrategy.Bpov {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (t : PostTuple n X Y A B D × Y) (b : B) : R.N.A

Equations

• S.Bpov μ R t b = ∑ bs : Fin n → B, if bs t.1.1.i = b then R.Bmeas (CommutingRepetition.TracialStrategy.labelB D t.1 t.2) bs else 0

theorem CommutingRepetition.TracialStrategy.Apov_pos {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : PostTuple n X Y A B D × X) (a : A) : IsPosElem (S.Apov μ R s a)

theorem CommutingRepetition.TracialStrategy.Bpov_pos {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (t : PostTuple n X Y A B D × Y) (b : B) : IsPosElem (S.Bpov μ R t b)

theorem CommutingRepetition.TracialStrategy.Apov_sum {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : PostTuple n X Y A B D × X) : ∑ a : A, S.Apov μ R s a = 1

theorem CommutingRepetition.TracialStrategy.Bpov_sum {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (t : PostTuple n X Y A B D × Y) : ∑ b : B, S.Bpov μ R t b = 1

theorem CommutingRepetition.TracialStrategy.candidate_pairing {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (μ : X → Y → ℝ) (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)) (s : ALabel n X Y A) (t : BLabel n X Y B) (i : Fin n) (a : A) (b : B) (hb : R.branch S.σ s t ≠ 0) : (inner ℂ (R.candidate S.σ s t) ((R.N.L (∑ as : Fin n → A, if as i = a then R.Ameas s as else 0)) ((R.N.Rop (∑ bs : Fin n → B, if bs i = b then R.Bmeas t bs else 0)) (R.candidate S.σ s t)))).re = (∑ as : Fin n → A, ∑ bs : Fin n → B, if as i = a ∧ bs i = b then (S.M.τ (star S.σ * (S.refinedA D μ s as * S.σ * S.refinedB D μ t bs))).re else 0) / ‖R.branch S.σ s t‖ ^ 2

The ideal answer law (eq ideal-answer-law, coarse-grained form): on a nonzero branch, the candidate's answer pairing is the refined pairing mass at the live answers divided by the branch mass.