structure CommutingRepetition.RevealDatum (n : ℕ) (D : Finset (Fin n)) : Type

The finite public reveal datum λ = (i, L_X, L_Y, π_{X,−i}, π_{Y,−i}, k_X, k_Y) of the forward reveal experiment over the core D (05_prerounding.tex, eq lambda-full): a live coordinate i ∉ D, a two-block partition L_X ⊔ L_Y of the non-core coordinates other than i, uniform orders of the two blocks (encoded as position↦element equivalences), and cuts k_X ∈ {0,…,|L_X|}, k_Y ∈ {0,…,|L_Y|}.

• i : Fin n
• i_notMem : self.i ∉ D
• LX : Finset (Fin n)
• LY : Finset (Fin n)
• disjoint : Disjoint self.LX self.LY
• partition : self.LX ∪ self.LY = (insert self.i D)ᶜ
• πX : Fin self.LX.card ≃ ↥self.LX
• πY : Fin self.LY.card ≃ ↥self.LY
• kX : Fin (self.LX.card + 1)
• kY : Fin (self.LY.card + 1)

@[instance_reducible]

instance CommutingRepetition.instFintypeRevealDatum {n✝ : ℕ} {D✝ : Finset (Fin n✝)} : Fintype (RevealDatum n✝ D✝)

Equations

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

def CommutingRepetition.RevealDatum.prefixX {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : Finset (Fin n)

The first k_X entries of the order π_{X,−i}, as a set: π_{X,−i}^{≤ k_X} (05_prerounding.tex, eq forward-reveal-sets).

Equations

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

def CommutingRepetition.RevealDatum.prefixY {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : Finset (Fin n)

The first k_Y entries of the order π_{Y,−i}, as a set: π_{Y,−i}^{≤ k_Y}.

Equations

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

def CommutingRepetition.RevealDatum.CX {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : Finset (Fin n)

Alice's revealed coordinate set C_X = D ∪ L_X ∪ π_{Y,−i}^{≤ k_Y} (05_prerounding.tex, eq forward-reveal-sets).

Equations

• d.CX = D ∪ d.LX ∪ d.prefixY

def CommutingRepetition.RevealDatum.CY {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : Finset (Fin n)

Bob's revealed coordinate set C_Y = D ∪ L_Y ∪ π_{X,−i}^{≤ k_X}.

Equations

• d.CY = D ∪ d.LY ∪ d.prefixX

theorem CommutingRepetition.RevealDatum.prefixX_subset {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.prefixX ⊆ d.LX

theorem CommutingRepetition.RevealDatum.prefixY_subset {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.prefixY ⊆ d.LY

theorem CommutingRepetition.RevealDatum.LX_subset {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.LX ⊆ (insert d.i D)ᶜ

theorem CommutingRepetition.RevealDatum.LY_subset {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.LY ⊆ (insert d.i D)ᶜ

theorem CommutingRepetition.RevealDatum.core_subset {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : D ⊆ d.CX ∩ d.CY

First half of eq reveal-cover: D ⊆ C_X ∩ C_Y.

theorem CommutingRepetition.RevealDatum.union_eq_compl_singleton {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.CX ∪ d.CY = {d.i}ᶜ

Second half of eq reveal-cover: C_X ∪ C_Y = [n] \ {i} — every coordinate other than the live one is revealed to at least one player. This is what makes the prior factorize (eq prior-factorization).

theorem CommutingRepetition.RevealDatum.i_notMem_CX {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.i ∉ d.CX

The live coordinate is unrevealed to Alice.

theorem CommutingRepetition.RevealDatum.i_notMem_CY {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.i ∉ d.CY

The live coordinate is unrevealed to Bob.

theorem CommutingRepetition.RevealDatum.card_LX_add_card_LY {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : d.LX.card + d.LY.card = n - D.card - 1

Block sizes: |L_X| + |L_Y| = m − 1 with m = n − |D| non-core coordinates.

noncomputable def CommutingRepetition.RevealDatum.revealLaw {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : ℝ

The forward reveal law (05_prerounding.tex, eqs lambda-full and forward-outcome-probability): i uniform on the m non-core coordinates, each remaining coordinate assigned to a block by a fair coin, uniform orders of the two blocks, uniform cuts — the datum's probability is 2^{1−m} / (m · |L_X|! · (|L_X|+1) · |L_Y|! · (|L_Y|+1)).

Equations

• d.revealLaw = 1 / ↑(n - D.card) * (1 / 2 ^ (n - D.card - 1)) * (1 / ↑d.LX.card.factorial) * (1 / ↑d.LY.card.factorial) * (1 / (↑d.LX.card + 1)) * (1 / (↑d.LY.card + 1))

theorem CommutingRepetition.RevealDatum.revealLaw_nonneg {n : ℕ} {D : Finset (Fin n)} (d : RevealDatum n D) : 0 ≤ d.revealLaw

theorem CommutingRepetition.RevealDatum.revealLaw_sum {n : ℕ} {D : Finset (Fin n)} (hD : D.card < n) : ∑ d : RevealDatum n D, d.revealLaw = 1

The forward reveal law is a probability law on reveal data (05_prerounding.tex, eq lambda-full with eq forward-outcome-probability: m choices of i, 2^{m−1} block assignments, |L_X|!·|L_Y|! orders, (|L_X|+1)(|L_Y|+1) cuts). Requires a proper core |D| < n, which the greedy conditioning guarantees (|D| < n/2).

def CommutingRepetition.agreesOn {n : ℕ} {α : Type u_1} (S : Finset (Fin n)) (w w' : Fin n → α) : Prop

Two words agree on a finite index set.

Equations

• CommutingRepetition.agreesOn S w w' = ∀ j ∈ S, w j = w' j

@[instance_reducible]

instance CommutingRepetition.instDecidableAgreesOnOfDecidableEq {n : ℕ} {α : Type u_1} [DecidableEq α] (S : Finset (Fin n)) (w w' : Fin n → α) : Decidable (agreesOn S w w')

Equations

• CommutingRepetition.instDecidableAgreesOnOfDecidableEq S w w' = id inferInstance

noncomputable def CommutingRepetition.priorWeight {n : ℕ} {X Y : Type} [DecidableEq X] [DecidableEq Y] {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (x : Fin n → X) (y : Fin n → Y) : ℝ

The unnormalized posterior weight of a full question-word pair given the reveal: the product prior ∏_j μ(x_j, y_j) restricted to the words consistent with the revealed values — x on C_X ∪ {i} and y on C_Y ∪ {i} (the conditioning (T₀ = t, X_i = x, Y_i = y) of 05_prerounding.tex, eq prior-factorization, with the revealed values packaged as reference words x₀, y₀).

Equations

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

theorem CommutingRepetition.prior_factorization {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (f : (Fin n → X) → ℝ) (g : (Fin n → Y) → ℝ) : (∑ x : Fin n → X, ∑ y : Fin n → Y, priorWeight d μ x₀ y₀ x y * (f x * g y)) * ∑ x : Fin n → X, ∑ y : Fin n → Y, priorWeight d μ x₀ y₀ x y = (∑ x : Fin n → X, ∑ y : Fin n → Y, priorWeight d μ x₀ y₀ x y * f x) * ∑ x : Fin n → X, ∑ y : Fin n → Y, priorWeight d μ x₀ y₀ x y * g y

Prior factorization (node 1.2.3; 05_prerounding.tex, eq prior-factorization): given the reveal and the live questions, the full Alice word and the full Bob word are conditionally independent under the referee's product prior, because the unrevealed Alice coordinates and the unrevealed Bob coordinates occupy disjoint coordinate sets (eq reveal-cover) and each carries a pinned half of its coordinate's joint law. Stated division-free as the exact identity E[fg]·E[1] = E[f]·E[g] for the unnormalized conditioned weight, for every pair of test functions; the identity is under the prior ℙ, not under the posterior ℚ.