Positivity propagates one reveal back

theorem CommutingRepetition.TracialStrategy.re_pairing_pos_of_revealB {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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (H : S.M.A) (hH : IsPosElem H) (R₀ : Finset (Fin n)) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) (c : Fin n) (hc : c ∉ R₀) (y : Y) (hμc : 0 < μ (x₀ c) y) (hpos : 0 < (S.M.τ (star S.σ * (H * S.σ * S.setEffectB D (insert c R₀) μ x₀ (Function.update y₀ c y) zB))).re) : 0 < (S.M.τ (star S.σ * (H * S.σ * S.setEffectB D R₀ μ x₀ y₀ zB))).re

If the pairing against the effect revealed at one more coordinate c (pinned at a value of positive conditional weight) is positive, so is the pairing against the less revealed effect (Bob side).

theorem CommutingRepetition.TracialStrategy.re_pairing_pos_of_revealA {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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (K : S.M.A) (hK : IsPosElem K) (R₀ : Finset (Fin n)) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) (c : Fin n) (hc : c ∉ R₀) (x : X) (hμc : 0 < μ x (y₀ c)) (hpos : 0 < (S.M.τ (star S.σ * (S.setEffectA D (insert c R₀) μ (Function.update x₀ c x) y₀ zA * S.σ * K))).re) : 0 < (S.M.τ (star S.σ * (S.setEffectA D R₀ μ x₀ y₀ zA * S.σ * K))).re

Alice-side mirror of re_pairing_pos_of_revealB.

The bar branches are nonzero on the support

theorem CommutingRepetition.TracialStrategy.barB_branch_ne_zero {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 μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (r : RevealDatum n D) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) (hμi : 0 < μ (xw r.i) (yw r.i)) (hb : R.branch S.σ (aLabel D (insert r.i r.CX) xw yw zA) (bLabel D (insert r.i r.CY) xw yw zB) ≠ 0) : R.branch S.σ (aLabel D (insert r.i r.CX) xw yw zA) (bLabel D r.CY xw yw zB) ≠ 0

The bar Bob branch (Bob's live coordinate unrevealed) is nonzero wherever the full branch is nonzero and the live question pair has positive weight.

theorem CommutingRepetition.TracialStrategy.barA_branch_ne_zero {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 μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (r : RevealDatum n D) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) (hμi : 0 < μ (xw r.i) (yw r.i)) (hb : R.branch S.σ (aLabel D (insert r.i r.CX) xw yw zA) (bLabel D (insert r.i r.CY) xw yw zB) ≠ 0) : R.branch S.σ (aLabel D r.CX xw yw zA) (bLabel D (insert r.i r.CY) xw yw zB) ≠ 0

The bar Alice branch is nonzero wherever the full branch is nonzero and the live question pair has positive weight.

The alignment defect

noncomputable def CommutingRepetition.TracialStrategy.alignTerm {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 μ)) (u : PostTuple n X Y A B D × X × Y) : ℝ

The summand of the package's alignment defect at a flattened tuple.

Equations

• S.alignTerm μ R u = ‖S.uVec μ R (u.1, u.2.1) (u.1, u.2.2) - S.xVec μ R (u.1, u.2.1)‖ ^ 2 + ‖S.uVec μ R (u.1, u.2.1) (u.1, u.2.2) - S.yVec μ R (u.1, u.2.2)‖ ^ 2

theorem CommutingRepetition.TracialStrategy.posteriorQ_mul_alignTerm {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 μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (t : PostTuple n X Y A B D) : S.posteriorQ R D μ w p t * S.alignTerm μ R (flattenPost t) = S.posteriorQ R D μ w p t * (‖R.candidate S.σ (aLabel D (insert t.1.i t.1.CX) t.2.1 t.2.2.1 t.2.2.2.1) (bLabel D (insert t.1.i t.1.CY) t.2.1 t.2.2.1 t.2.2.2.2) - R.candidate S.σ (aLabel D (insert t.1.i t.1.CX) t.2.1 t.2.2.1 t.2.2.2.1) (bLabel D t.1.CY t.2.1 t.2.2.1 t.2.2.2.2)‖ ^ 2 + ‖R.candidate S.σ (aLabel D (insert t.1.i t.1.CX) t.2.1 t.2.2.1 t.2.2.2.1) (bLabel D (insert t.1.i t.1.CY) t.2.1 t.2.2.1 t.2.2.2.2) - R.candidate S.σ (aLabel D t.1.CX t.2.1 t.2.2.1 t.2.2.2.1) (bLabel D (insert t.1.i t.1.CY) t.2.1 t.2.2.1 t.2.2.2.2)‖ ^ 2)

On the support of the posterior law the package vectors are the arena's candidates, so the alignment summand is the candidate distance.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_alignTerm_le {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 μ)) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (hcol : R.ColEntropyBudget) (hrow : R.RowEntropyBudget) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (hw1 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), w xw yw zA zB ≤ 1) (hwD : ∀ (xw xw' : Fin n → X) (yw yw' : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), agreesOn D xw xw' → agreesOn D yw yw' → w xw yw zA zB = w xw' yw' zA zB) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) (hm : D.card < n) : ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D μ w p u * S.alignTerm μ R u ≤ 16 * (Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / (↑n - ↑D.card)

The alignment defect of the package Δ ≤ 16 (t₀ + s₀)/m (05_prerounding.tex, eqs two-alignment-bounds with prior-alignment-costs).