noncomputable def CommutingRepetition.setWeightX {n : ℕ} {X Y : Type} [DecidableEq X] (S : Finset (Fin n)) (μ : X → Y → ℝ) (xref : Fin n → X) (yref : Fin n → Y) (w : Fin n → X) : ℝ

The revealed-set one-sided weight (generalizing the signed RevealDatum.xWeight, review #9): the S-revealed conditioned unnormalized law of Alice's full question word — consistency with the reference on the revealed set S, times the pinned-Bob halves of the free coordinates' joint laws.

Equations

• CommutingRepetition.setWeightX S μ xref yref w = if CommutingRepetition.agreesOn S w xref then ∏ j ∈ Sᶜ, μ (w j) (yref j) else 0

noncomputable def CommutingRepetition.setWeightY {n : ℕ} {X Y : Type} [DecidableEq Y] (S : Finset (Fin n)) (μ : X → Y → ℝ) (xref : Fin n → X) (yref v : Fin n → Y) : ℝ

The revealed-set one-sided weight for Bob's word.

Equations

• CommutingRepetition.setWeightY S μ xref yref v = if CommutingRepetition.agreesOn S v yref then ∏ j ∈ Sᶜ, μ (xref j) (v j) else 0

noncomputable def CommutingRepetition.TracialStrategy.setEffectA {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) : S.M.A

The revealed-set Alice effect 𝔼[E^{a_D} ∣ X revealed on R₀, Bob's word] (05_prerounding.tex, the conditional expectations of eq alice-reveal-martingale, general revealed set): the setWeightX-average of the core effects.

Equations

• S.setEffectA D R₀ μ xref yref zA = CommutingRepetition.weightedAvg (CommutingRepetition.setWeightX R₀ μ xref yref) fun (w : Fin n → X) => S.coreEffectA D w zA

noncomputable def CommutingRepetition.TracialStrategy.setEffectB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) : S.M.A

The revealed-set Bob effect (mirror).

Equations

• S.setEffectB D R₀ μ xref yref zB = CommutingRepetition.weightedAvg (CommutingRepetition.setWeightY R₀ μ xref yref) fun (v : Fin n → Y) => S.coreEffectB D v zB

theorem CommutingRepetition.TracialStrategy.effectiveH_eq_setEffectA {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) : S.effectiveH d μ x₀ y₀ zA = S.setEffectA D (insert d.i d.CX) μ x₀ y₀ zA

effectiveH is the revealed-set effect at {i} ∪ C_X (the signed node-1.2.4 encoding, re-expressed; definitional).

theorem CommutingRepetition.TracialStrategy.effectiveK_eq_setEffectB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) : S.effectiveK d μ x₀ y₀ zB = S.setEffectB D (insert d.i d.CY) μ x₀ y₀ zB

effectiveK is the revealed-set effect at {i} ∪ C_Y (definitional).

theorem CommutingRepetition.TracialStrategy.setEffectA_reveal {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) (c : Fin n) (hc : c ∉ R₀) : S.setEffectA D R₀ μ xref yref zA = weightedAvg (fun (x' : X) => μ x' (yref c)) fun (x' : X) => S.setEffectA D (insert c R₀) μ (Function.update xref c x') yref zA

One-step reveal identity, Alice side (the tower property making eq alice-reveal-martingale a martingale): revealing one more coordinate c is averaging over its conditional law μ(·∣yref c). Junk-safe: at a vanishing conditional marginal both sides are 0.

theorem CommutingRepetition.TracialStrategy.setEffectB_reveal {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D R₀ : Finset (Fin n)) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) (c : Fin n) (hc : c ∉ R₀) : S.setEffectB D R₀ μ xref yref zB = weightedAvg (fun (y' : Y) => μ (xref c) y') fun (y' : Y) => S.setEffectB D (insert c R₀) μ xref (Function.update yref c y') zB

One-step reveal identity, Bob side (the tower property of eq bob-reveal-martingale).

def CommutingRepetition.AliceRevealDatum.revealPrefix {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) (j : Fin (d.LYp.card + 1)) : Finset (Fin n)

The first j entries of the reverse Bob-block order π_Y, as a set: the progressively revealed coordinates of eq alice-reveal-martingale.

Equations

• d.revealPrefix j = Finset.image (fun (t : Fin d.LYp.card) => ↑(d.πY t)) {t : Fin d.LYp.card | ↑t < ↑j}

def CommutingRepetition.AliceRevealDatum.alicePrefixX {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : Finset (Fin n)

The forward Alice-block prefix π_X^{≤ k_X} carried by the reverse datum, as a set.

Equations

• d.alicePrefixX = Finset.image (fun (t : Fin d.LX.card) => ↑(d.πX t)) {t : Fin d.LX.card | ↑t < ↑d.kX}

theorem CommutingRepetition.AliceRevealDatum.revealPrefix_succ {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.revealPrefix d.kY.succ = insert d.liveIdx (d.revealPrefix d.kY.castSucc)

The reveal prefix grows by exactly the live coordinate at the cut: π_Y[1..k_Y+1] = {π_Y[k_Y+1]} ∪ π_Y[1..k_Y] (aux).

def CommutingRepetition.BobRevealDatum.revealPrefix {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) (j : Fin (d.LXp.card + 1)) : Finset (Fin n)

The first j entries of the reverse Alice-block order π_X, as a set (eq bob-reveal-martingale).

Equations

• d.revealPrefix j = Finset.image (fun (t : Fin d.LXp.card) => ↑(d.πX t)) {t : Fin d.LXp.card | ↑t < ↑j}

def CommutingRepetition.BobRevealDatum.bobPrefixY {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : Finset (Fin n)

The forward Bob-block prefix π_Y^{≤ k_Y} carried by the reverse datum, as a set.

Equations

• d.bobPrefixY = Finset.image (fun (t : Fin d.LY.card) => ↑(d.πY t)) {t : Fin d.LY.card | ↑t < ↑d.kY}

theorem CommutingRepetition.BobRevealDatum.revealPrefix_succ {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.revealPrefix d.kX.succ = insert d.liveIdx (d.revealPrefix d.kX.castSucc)

The reveal prefix grows by exactly the live coordinate at the cut (aux, mirror).

noncomputable def CommutingRepetition.TracialStrategy.revealMartA {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq A] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : AliceRevealDatum n D) (μ : X → Y → ℝ) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) (j : Fin (d.LYp.card + 1)) : S.M.A

The Alice reveal martingale F_{j,z}(U_A) (05_prerounding.tex, eq alice-reveal-martingale): the revealed-set Alice effect after the background D ∪ L_X plus the first j entries of the Bob-block order.

Equations

• S.revealMartA d μ xref yref zA j = S.setEffectA D (D ∪ d.LX ∪ d.revealPrefix j) μ xref yref zA

noncomputable def CommutingRepetition.TracialStrategy.revealMartB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq Y] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : BobRevealDatum n D) (μ : X → Y → ℝ) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) (j : Fin (d.LXp.card + 1)) : S.M.A

The Bob reveal martingale G_{j,z}(U_B) (eq bob-reveal-martingale, mirror).

Equations

• S.revealMartB d μ xref yref zB j = S.setEffectB D (D ∪ d.LY ∪ d.revealPrefix j) μ xref yref zB

theorem CommutingRepetition.TracialStrategy.revealMartA_cut_eq_effectiveHBar {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : AliceRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLX : r.LX = d.LX) (hpre : r.prefixY = d.revealPrefix d.kY.castSucc) : S.revealMartA d μ xref yref zA d.kY.castSucc = S.effectiveHBar r μ xref yref zA

Live increment, Alice side, lower cut (node 1.2.8; 05_prerounding.tex, eq alice-live-increment first identity): F_{k_Y,z} = H̄_{r,Y_i} — at the cut, the reveal martingale is the bar-averaged effective effect of the forward datum. The forward datum r is pinned by the signed pushforward carryover (review #11) plus the order-compatibility facts deferred to this operator half.

theorem CommutingRepetition.TracialStrategy.revealMartA_cutSucc_eq_effectiveH {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : AliceRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLX : r.LX = d.LX) (hpre : r.prefixY = d.revealPrefix d.kY.castSucc) : S.revealMartA d μ xref yref zA d.kY.succ = S.effectiveH r μ xref yref zA

Live increment, Alice side, upper cut (eq alice-live-increment second identity): F_{k_Y+1,z} = H_{r,X_i} — one step past the cut, the reveal martingale is the effective effect itself.

theorem CommutingRepetition.TracialStrategy.aliceFixedBobEffect_eq_effectiveK {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : AliceRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLY : r.LY = d.LYp.erase d.liveIdx) (hpx : r.prefixX = d.alicePrefixX) : S.setEffectB D (D ∪ d.LYp ∪ d.alicePrefixX) μ xref yref zB = S.effectiveK r μ xref yref zB

The fixed Bob effect under the Alice-reveal background (eq alice-fixed-bob-effect with eq alice-live-increment third identity): K_z(U_A) = 𝔼[F^{b_D} ∣ U_A] = K_{r,Y_i} — Bob's word is revealed on D ∪ L_Y⁺ ∪ π_X^{≤k_X}, which is exactly the forward {i} ∪ C_Y.

theorem CommutingRepetition.TracialStrategy.revealMartB_cut_eq_effectiveKBar {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : BobRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLY : r.LY = d.LY) (hpre : r.prefixX = d.revealPrefix d.kX.castSucc) : S.revealMartB d μ xref yref zB d.kX.castSucc = S.effectiveKBar r μ xref yref zB

Live increment, Bob side, lower cut (eq bob-live-increment first identity): G_{k_X,z} = K̄_{r,X_i}.

theorem CommutingRepetition.TracialStrategy.revealMartB_cutSucc_eq_effectiveK {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : BobRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zB : Fin n → B) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLY : r.LY = d.LY) (hpre : r.prefixX = d.revealPrefix d.kX.castSucc) : S.revealMartB d μ xref yref zB d.kX.succ = S.effectiveK r μ xref yref zB

Live increment, Bob side, upper cut (eq bob-live-increment second identity): G_{k_X+1,z} = K_{r,Y_i}.

theorem CommutingRepetition.TracialStrategy.bobFixedAliceEffect_eq_effectiveH {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : BobRevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (xref : Fin n → X) (yref : Fin n → Y) (zA : Fin n → A) (r : RevealDatum n D) (hi : r.i = d.liveIdx) (hLX : r.LX = d.LXp.erase d.liveIdx) (hpy : r.prefixY = d.bobPrefixY) : S.setEffectA D (D ∪ d.LXp ∪ d.bobPrefixY) μ xref yref zA = S.effectiveH r μ xref yref zA

The fixed Alice effect under the Bob-reveal background (eq bob-live-increment third identity): H_z(U_B) = H_{r,X_i}.

Strengthened pushforwards (review-#14 note N3)

The signed pushforward statements (review #11) carry the live coordinate, the blocks, and the cut values, and defer order compatibility; the wiring identities above take that compatibility as prefix-set hypotheses. The strengthened forms below expose exactly those prefix conjuncts, so the arena invocation (node 1.2.11) can discharge the wiring hypotheses from one bijection. Provable by the same order surgery as the signed aliceReveal_pushforward_eq / bobReveal_pushforward_eq (deleting at the cut preserves the strict prefix and the untouched forward-side order).

theorem CommutingRepetition.aliceReveal_pushforward_strong (n : ℕ) (D : Finset (Fin n)) : ∃ (e : AliceRevealDatum n D ≃ RevealDatum n D), (∀ (d : AliceRevealDatum n D), d.law = (e d).revealLaw) ∧ ∀ (d : AliceRevealDatum n D), (e d).i = d.liveIdx ∧ (e d).LX = d.LX ∧ (e d).LY = d.LYp.erase d.liveIdx ∧ ↑(e d).kX = ↑d.kX ∧ ↑(e d).kY = ↑d.kY ∧ (e d).prefixY = d.revealPrefix d.kY.castSucc ∧ (e d).prefixX = d.alicePrefixX

Alice-reveal pushforward, strengthened carryover (node 1.2.8; 05_prerounding.tex "Both reverse experiments have exactly the forward law", with the order compatibility deferred by review #11 now explicit): the datum bijection matches laws pointwise and carries over the live coordinate, blocks, cut values, AND both prefix sets.

theorem CommutingRepetition.bobReveal_pushforward_strong (n : ℕ) (D : Finset (Fin n)) : ∃ (e : BobRevealDatum n D ≃ RevealDatum n D), (∀ (d : BobRevealDatum n D), d.law = (e d).revealLaw) ∧ ∀ (d : BobRevealDatum n D), (e d).i = d.liveIdx ∧ (e d).LY = d.LY ∧ (e d).LX = d.LXp.erase d.liveIdx ∧ ↑(e d).kY = ↑d.kY ∧ ↑(e d).kX = ↑d.kX ∧ (e d).prefixX = d.revealPrefix d.kX.castSucc ∧ (e d).prefixY = d.bobPrefixY

Bob-reveal pushforward, strengthened carryover (mirror).