Word agreement

theorem CommutingRepetition.agreesOn_refl {n : ℕ} {α : Type} [DecidableEq α] (S : Finset (Fin n)) (a : Fin n → α) : agreesOn S a a

theorem CommutingRepetition.agreesOn_comm {n : ℕ} {α : Type} [DecidableEq α] {S : Finset (Fin n)} {a b : Fin n → α} : agreesOn S a b ↔ agreesOn S b a

theorem CommutingRepetition.agreesOn_univ_iff {n : ℕ} {α : Type} [DecidableEq α] {a b : Fin n → α} : agreesOn Finset.univ a b ↔ a = b

theorem CommutingRepetition.agreesOn_insert_iff {n : ℕ} {α : Type} [DecidableEq α] {S : Finset (Fin n)} {i : Fin n} {a b : Fin n → α} : agreesOn (insert i S) a b ↔ a i = b i ∧ agreesOn S a b

theorem CommutingRepetition.agreesOn_mono {n : ℕ} {α : Type} [DecidableEq α] {S T : Finset (Fin n)} (hST : S ⊆ T) {a b : Fin n → α} (h : agreesOn T a b) : agreesOn S a b

theorem CommutingRepetition.keepOn_eq_iff {n : ℕ} {α : Type} [DecidableEq α] [Nonempty α] (S : Finset (Fin n)) (a b : Fin n → α) : keepOn S a = keepOn S b ↔ agreesOn S a b

theorem CommutingRepetition.sum_agree_prod {n : ℕ} {α : Type} [DecidableEq α] [Fintype α] (S : Finset (Fin n)) (xw : Fin n → α) (f : Fin n → α → ℝ) : (∑ xw' : Fin n → α, if agreesOn S xw' xw then ∏ j : Fin n, f j (xw' j) else 0) = ∏ j : Fin n, if j ∈ S then f j (xw j) else ∑ x : α, f j x

Fiber product identity: summing a product over the words agreeing with a reference on S pins the S-factors and sums the others.

The core posterior law

@[reducible, inline]

abbrev CommutingRepetition.TracialStrategy.CoreTuple (n : ℕ) (X Y A B : Type) (D : Finset (Fin n)) : Type

The core tuple space: the two full question words and the core word (the second factor of PostTuple).

Equations

• CommutingRepetition.TracialStrategy.CoreTuple n X Y A B D = ((Fin n → X) × (Fin n → Y) × (↥D → A) × (↥D → B))

noncomputable def CommutingRepetition.TracialStrategy.corePair {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D : Finset (Fin n)) (s : CoreTuple n X Y A B D) : ℝ

The core pairing re τ(σ* E_x^{z_A} σ F_y^{z_B}).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommutingRepetition.TracialStrategy.prodPrior {n : ℕ} {X Y A B : Type} (D : Finset (Fin n)) (μ : X → Y → ℝ) (s : CoreTuple n X Y A B D) : ℝ

The full product prior on a core tuple's words.

Equations

• CommutingRepetition.TracialStrategy.prodPrior D μ s = ∏ j : Fin n, μ (s.1 j) (s.2.1 j)

noncomputable def CommutingRepetition.TracialStrategy.corePost {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D : Finset (Fin n)) (μ : X → Y → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (s : CoreTuple n X Y A B D) : ℝ

The core posterior law ℚ⁰(x, y, z) = Πμ · w · pairing / p: the posterior branch law with the reveal datum integrated out (eq posterior-branch-law at the core, i.e. the weighted core correlation normalized by p).

Equations

• S.corePost D μ w p s = CommutingRepetition.TracialStrategy.prodPrior D μ s * w s.1 s.2.1 s.2.2.1 s.2.2.2 * S.corePair D s / p

theorem CommutingRepetition.TracialStrategy.corePair_nonneg {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)) (s : CoreTuple n X Y A B D) : 0 ≤ S.corePair D s

theorem CommutingRepetition.TracialStrategy.sum_corePair {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)) (xw : Fin n → X) (yw : Fin n → Y) : ∑ zD : (↥D → A) × (↥D → B), S.corePair D (xw, yw, zD) = 1

The core pairings over all core words sum to τ(σ*σ) = 1.

theorem CommutingRepetition.TracialStrategy.corePair_le_one {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)) (s : CoreTuple n X Y A B D) : S.corePair D s ≤ 1

theorem CommutingRepetition.TracialStrategy.prodPrior_nonneg {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)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (s : CoreTuple n X Y A B D) : 0 ≤ prodPrior D μ s

theorem CommutingRepetition.TracialStrategy.corePost_nonneg {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) (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) {p : ℝ} (hppos : 0 < p) (s : CoreTuple n X Y A B D) : 0 ≤ S.corePost D μ w p s

theorem CommutingRepetition.TracialStrategy.sum_corePost {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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) {p : ℝ} (hp : p = S.coreMass D μ w) (hppos : 0 < p) : ∑ s : CoreTuple n X Y A B D, S.corePost D μ w p s = 1

The core posterior law is a probability law (the weighted core mass is p).

theorem CommutingRepetition.TracialStrategy.corePost_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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (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) {p : ℝ} (hppos : 0 < p) (s : CoreTuple n X Y A B D) : S.corePost D μ w p s ≤ p⁻¹ * prodPrior D μ s

Pointwise density bound: ℚ⁰ ≤ Πμ / p (eq question-answer-conditioning-budget, pointwise form).

theorem CommutingRepetition.TracialStrategy.sum_zD_corePost_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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (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) {p : ℝ} (hppos : 0 < p) (xw : Fin n → X) (yw : Fin n → Y) : ∑ zD : (↥D → A) × (↥D → B), S.corePost D μ w p (xw, yw, zD) ≤ p⁻¹ * ∏ j : Fin n, μ (xw j) (yw j)

The core-word sum of the core posterior is at most Πμ / p.

theorem CommutingRepetition.TracialStrategy.corePost_eq_zero_of_mu {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 → ℝ) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (s : CoreTuple n X Y A B D) (i : Fin n) (h : μ (s.1 i) (s.2.1 i) = 0) : S.corePost D μ w p s = 0

theorem CommutingRepetition.TracialStrategy.mu_pos_of_corePost_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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (s : CoreTuple n X Y A B D) (hs : 0 < S.corePost D μ w p s) (i : Fin n) : 0 < μ (s.1 i) (s.2.1 i)

Positivity of the core posterior forces positivity of every question factor.

theorem CommutingRepetition.TracialStrategy.prodPrior_pos_of_corePost_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 → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (p : ℝ) (s : CoreTuple n X Y A B D) (hs : 0 < S.corePost D μ w p s) : 0 < prodPrior D μ s

Class masses over revealed sets

noncomputable def CommutingRepetition.TracialStrategy.classMass {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {D : Finset (Fin n)} (SX SY : Finset (Fin n)) (f : CoreTuple n X Y A B D → ℝ) (s : CoreTuple n X Y A B D) : ℝ

The mass of a function of core tuples over the class of s fixing the Alice word on SX, the Bob word on SY, and the core word.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommutingRepetition.TracialStrategy.classMap {n : ℕ} {X Y A B : Type} [Nonempty X] [Nonempty Y] {D : Finset (Fin n)} (SX SY : Finset (Fin n)) (s : CoreTuple n X Y A B D) : CoreTuple n X Y A B D

The class map behind classMass.

Equations

• CommutingRepetition.TracialStrategy.classMap SX SY s = (CommutingRepetition.keepOn SX s.1, CommutingRepetition.keepOn SY s.2.1, s.2.2)

theorem CommutingRepetition.TracialStrategy.classMap_eq_iff {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)} (SX SY : Finset (Fin n)) (s s' : CoreTuple n X Y A B D) : classMap SX SY s' = classMap SX SY s ↔ agreesOn SX s'.1 s.1 ∧ agreesOn SY s'.2.1 s.2.1 ∧ s'.2.2 = s.2.2

theorem CommutingRepetition.TracialStrategy.classMass_eq_sum_ite {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)} (SX SY : Finset (Fin n)) (f : CoreTuple n X Y A B D → ℝ) (s : CoreTuple n X Y A B D) : classMass SX SY f s = ∑ s' : CoreTuple n X Y A B D, if classMap SX SY s' = classMap SX SY s then f s' else 0

classMass is the grouped mass under classMap, as an indicator sum over the whole tuple space.

theorem CommutingRepetition.TracialStrategy.classMass_nonneg {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)} (SX SY : Finset (Fin n)) (f : CoreTuple n X Y A B D → ℝ) (hf : ∀ (s : CoreTuple n X Y A B D), 0 ≤ f s) (s : CoreTuple n X Y A B D) : 0 ≤ classMass SX SY f s

theorem CommutingRepetition.TracialStrategy.le_classMass {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)} (SX SY : Finset (Fin n)) (f : CoreTuple n X Y A B D → ℝ) (hf : ∀ (s : CoreTuple n X Y A B D), 0 ≤ f s) (s : CoreTuple n X Y A B D) : f s ≤ classMass SX SY f s

theorem CommutingRepetition.TracialStrategy.classMass_mono_right {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)} (SX SY SY' : Finset (Fin n)) (hSY : SY ⊆ SY') (f : CoreTuple n X Y A B D → ℝ) (hf : ∀ (s : CoreTuple n X Y A B D), 0 ≤ f s) (s : CoreTuple n X Y A B D) : classMass SX SY' f s ≤ classMass SX SY f s

theorem CommutingRepetition.TracialStrategy.classMass_prodPrior {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)} (SX SY : Finset (Fin n)) (μ : X → Y → ℝ) (s : CoreTuple n X Y A B D) : classMass SX SY (prodPrior D μ) s = ∏ j : Fin n, if j ∈ SX then if j ∈ SY then μ (s.1 j) (s.2.1 j) else ∑ y : Y, μ (s.1 j) y else if j ∈ SY then ∑ x : X, μ x (s.2.1 j) else ∑ x : X, ∑ y : Y, μ x y

Product formula for the prior class mass: the doubly revealed coordinates are pinned, the singly revealed ones carry a marginal, the unrevealed ones the total mass.

theorem CommutingRepetition.TracialStrategy.classMass_prodPrior_univ_eq {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)} (SX SY : Finset (Fin n)) (hcov : SX ∪ SY = Finset.univ) (μ : X → Y → ℝ) (s : CoreTuple n X Y A B D) (hμX : ∀ j ∈ SX \ SY, ∑ y : Y, μ (s.1 j) y ≠ 0) : classMass SX Finset.univ (prodPrior D μ) s = classMass SX SY (prodPrior D μ) s * ∏ j ∈ SX \ SY, μ (s.1 j) (s.2.1 j) / ∑ y : Y, μ (s.1 j) y

The ratio of the prior class masses at a covering pair, the Bob set enlarged to everything: the pinned-to-marginal ratios on SX \ SY.

Canonical labels along a fiber

theorem CommutingRepetition.aLabel_congr {n : ℕ} {X Y A : Type} [Fintype X] [Fintype Y] [Fintype A] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [Nonempty X] [Nonempty Y] [Nonempty A] (D R₀ : Finset (Fin n)) {xw xw' : Fin n → X} {yw yw' : Fin n → Y} (zD : ↥D → A) (hx : ∀ j ∈ R₀, xw j = xw' j) (hy : ∀ j ∉ R₀, yw j = yw' j) : aLabel D R₀ xw yw zD = aLabel D R₀ xw' yw' zD

The canonical Alice label reads xw only on R₀ and yw only off R₀.

theorem CommutingRepetition.bLabel_congr {n : ℕ} {X Y B : Type} [Fintype X] [Fintype Y] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty B] (D R₀ : Finset (Fin n)) {xw xw' : Fin n → X} {yw yw' : Fin n → Y} (zD : ↥D → B) (hx : ∀ j ∉ R₀, xw j = xw' j) (hy : ∀ j ∈ R₀, yw j = yw' j) : bLabel D R₀ xw yw zD = bLabel D R₀ xw' yw' zD

The canonical Bob label reads xw only off R₀ and yw only on R₀.

theorem CommutingRepetition.RevealDatum.core_subset_insert_CX {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) : D ⊆ insert r.i r.CX

theorem CommutingRepetition.RevealDatum.core_subset_insert_CY {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) : D ⊆ insert r.i r.CY

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

Every coordinate is revealed to one side (eq reveal-cover).

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

theorem CommutingRepetition.RevealDatum.card_lt {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) : D.card < n

theorem CommutingRepetition.RevealDatum.revealLaw_pos {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) : 0 < r.revealLaw

theorem CommutingRepetition.groupedMass_ext_of_fibers {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (g : ι → κ) (f f' : ι → ℝ) (h : ∀ (t : ι), (∑ t' : ι, if g t' = g t then f t' else 0) = ∑ t' : ι, if g t' = g t then f' t' else 0) (u : κ) : ClassicalInformation.groupedMass g f u = ClassicalInformation.groupedMass g f' u

Grouped masses agree once every fiber sum agrees.

The fiber collapse of the posterior branch law

theorem CommutingRepetition.TracialStrategy.flattenPost_eq_iff {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 t' : PostTuple n X Y A B D) : flattenPost t' = flattenPost t ↔ t'.1 = t.1 ∧ agreesOn (insert t.1.i t.1.CX) t'.2.1 t.2.1 ∧ agreesOn (insert t.1.i t.1.CY) t'.2.2.1 t.2.2.1 ∧ t'.2.2.2 = t.2.2.2

The fibers of the flattening: same datum, same core word, and the words agree on {i} ∪ C_X resp. {i} ∪ C_Y.

theorem CommutingRepetition.TracialStrategy.sum_fiber_flattenPost {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)} (F : PostTuple n X Y A B D → ℝ) (t : PostTuple n X Y A B D) : (∑ t' : PostTuple n X Y A B D, if flattenPost t' = flattenPost t then F t' else 0) = ∑ xw' : Fin n → X, ∑ yw' : Fin n → Y, if agreesOn (insert t.1.i t.1.CX) xw' t.2.1 ∧ agreesOn (insert t.1.i t.1.CY) yw' t.2.2.1 then F (t.1, xw', yw', t.2.2.2) else 0

A fiber sum of the flattening, as a double word sum.

theorem CommutingRepetition.TracialStrategy.branch_normSq_eq {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (r : RevealDatum n D) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : ‖R.branch S.σ (aLabel D (insert r.i r.CX) xw yw zD.1) (bLabel D (insert r.i r.CY) xw yw zD.2)‖ ^ 2 = (S.M.τ (star S.σ * (S.effectiveH r μ xw yw (extendCoreA D zD.1) * S.σ * S.effectiveK r μ xw yw (extendCoreB D zD.2)))).re

Branch mass at the full canonical labels: the effective-effect pairing.

theorem CommutingRepetition.TracialStrategy.posteriorQ_fiber {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 : ℝ) (r : RevealDatum n D) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : (∑ xw' : Fin n → X, ∑ yw' : Fin n → Y, if agreesOn (insert r.i r.CX) xw' xw ∧ agreesOn (insert r.i r.CY) yw' yw then S.posteriorQ R D μ w p (r, xw', yw', zD) else 0) = r.revealLaw * classMass (insert r.i r.CX) (insert r.i r.CY) (S.corePost D μ w p) (xw, yw, zD)

The fiber collapse (eq posterior-branch-law through eqs branch-probability and prior-factorization): over a flattening fiber the posterior branch law sums to the reveal law times the core posterior class mass.

theorem CommutingRepetition.TracialStrategy.flatQ_eq {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 : ℝ) (u : PostTuple n X Y A B D × X × Y) : S.flatQ R D μ w p u = ClassicalInformation.groupedMass flattenPost (fun (t : PostTuple n X Y A B D) => t.1.revealLaw * S.corePost D μ w p t.2) u

The pushforward identity (F0): the flattened posterior is the pushforward of revealLaw ⊗ ℚ⁰ under the flattening.

theorem CommutingRepetition.TracialStrategy.flatQ_flattenPost {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 : ℝ) (t : PostTuple n X Y A B D) : S.flatQ R D μ w p (flattenPost t) = t.1.revealLaw * classMass (insert t.1.i t.1.CX) (insert t.1.i t.1.CY) (S.corePost D μ w p) t.2

(F1) The flattened posterior at a flattened tuple.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_hist {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 : ℝ) (t : PostTuple n X Y A B D) : ∑ y : Y, S.flatQ R D μ w p (histCore t, t.2.1 t.1.i, y) = t.1.revealLaw * classMass (insert t.1.i t.1.CX) t.1.CY (S.corePost D μ w p) t.2

(F2) The flattened posterior summed over the live Bob question.

theorem CommutingRepetition.TracialStrategy.sum_flatQ_live {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 : ℝ) (i₀ : Fin n) (x : X) : (∑ h : PostTuple n X Y A B D, if h.1.i = i₀ then ∑ y : Y, S.flatQ R D μ w p (h, x, y) else 0) = (∑ r : RevealDatum n D, if r.i = i₀ then r.revealLaw else 0) * ∑ s : CoreTuple n X Y A B D, if s.1 i₀ = x then S.corePost D μ w p s else 0

(F3) The flattened posterior mass of a live coordinate and live Alice question: the reveal law's fiber mass times the core marginal.

theorem CommutingRepetition.TracialStrategy.posteriorQ_nonneg {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (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) {p : ℝ} (hppos : 0 < p) (t : PostTuple n X Y A B D) : 0 ≤ S.posteriorQ R D μ w p t

theorem CommutingRepetition.TracialStrategy.flatQ_nonneg {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (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) {p : ℝ} (hppos : 0 < p) (u : PostTuple n X Y A B D × X × Y) : 0 ≤ S.flatQ R D μ w p u

theorem CommutingRepetition.TracialStrategy.sum_flatQ {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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : ALabel n X Y A → Af → S.M.A} {Gfam : BLabel n X Y B → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : ALabel n X Y A), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : BLabel n X Y B), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (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 = 1

The flattened posterior is a probability law (eq posterior-branch-normalization pushed forward).

The reveal law's fiber mass at a live coordinate

theorem CommutingRepetition.RevealDatum.revealLaw_sum_fiber {n : ℕ} {D : Finset (Fin n)} (i₀ : Fin n) (hi₀ : i₀ ∉ D) : (∑ d : RevealDatum n D, if d.i = i₀ then d.revealLaw else 0) = 1 / ↑(n - D.card)

The reveal law restricted to a fixed live coordinate i₀ ∉ D has mass 1/m (the live coordinate is uniform on the m non-core coordinates; the same count as revealLaw_sum, one fibre of the outer sum).