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

The Alice-reveal reverse datum (05_prerounding.tex, eq size-biased-partition and following): a two-block partition M₀ = L_X ⊔ L_Y⁺ of the non-core coordinates, a full order of the Bob block L_Y⁺, a cut strictly inside it (whose entry is the live coordinate), and the independent forward Alice-side order and cut.

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

@[instance_reducible]

instance CommutingRepetition.instFintypeAliceRevealDatum {n✝ : ℕ} {D✝ : Finset (Fin n✝)} : Fintype (AliceRevealDatum n✝ D✝)

Equations

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

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

The Bob-reveal reverse datum (05_prerounding.tex, eq bob-size-biased-partition): the mirror image, with the Alice block carrying the full order and the interior cut.

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

@[instance_reducible]

instance CommutingRepetition.instFintypeBobRevealDatum {n✝ : ℕ} {D✝ : Finset (Fin n✝)} : Fintype (BobRevealDatum n✝ D✝)

Equations

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

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

The live coordinate i = π_Y[k_Y + 1] (1-indexed manuscript entry = 0-indexed position k_Y).

Equations

• d.liveIdx = ↑(d.πY d.kY)

theorem CommutingRepetition.AliceRevealDatum.liveIdx_mem {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.liveIdx ∈ d.LYp

theorem CommutingRepetition.AliceRevealDatum.liveIdx_notMem_core {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.liveIdx ∉ D

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

The size-biased reverse law (eq size-biased-partition with the uniform order, interior cut, and independent forward variables): 2^{−m}·(2N_A/m) · (1/N_A!) · (1/N_A) · (1/|L_X|!) · (1/(|L_X|+1)), m = n − |D|, N_A = |L_Y⁺|.

Equations

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

theorem CommutingRepetition.AliceRevealDatum.law_nonneg {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : 0 ≤ d.law

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

The live coordinate i = π_X[k_X + 1].

Equations

• d.liveIdx = ↑(d.πX d.kX)

theorem CommutingRepetition.BobRevealDatum.liveIdx_mem {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.liveIdx ∈ d.LXp

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

The size-biased reverse law for the Bob-reveal experiment (eq bob-size-biased-partition).

Equations

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

theorem CommutingRepetition.BobRevealDatum.law_nonneg {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : 0 ≤ d.law

Shared surgery helpers for the pushforward bijections

The pushforward maps, as named data

@[reducible]

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

The forward map of the Alice-reveal pushforward: read off the live coordinate i = π_Y[k_Y+1] and delete it from the Bob-block order.

Equations

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

theorem CommutingRepetition.AliceRevealDatum.toReveal_i {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.toReveal.i = d.liveIdx

theorem CommutingRepetition.AliceRevealDatum.toReveal_LX {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.toReveal.LX = d.LX

theorem CommutingRepetition.AliceRevealDatum.toReveal_LY {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.toReveal.LY = d.LYp.erase d.liveIdx

theorem CommutingRepetition.AliceRevealDatum.toReveal_kX {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : ↑d.toReveal.kX = ↑d.kX

theorem CommutingRepetition.AliceRevealDatum.toReveal_kY {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : ↑d.toReveal.kY = ↑d.kY

theorem CommutingRepetition.AliceRevealDatum.law_toReveal {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) : d.law = d.toReveal.revealLaw

The forward map matches the laws pointwise (eq forward-outcome-probability).

theorem CommutingRepetition.AliceRevealDatum.toReveal_πY_of_lt {n : ℕ} {D : Finset (Fin n)} (d : AliceRevealDatum n D) (t : Fin d.toReveal.LY.card) (s : Fin d.LYp.card) (hval : ↑t = ↑s) (hlt : ↑s < ↑d.kY) : ↑(d.toReveal.πY t) = ↑(d.πY s)

Below the cut, the surgered Bob-block order agrees with the original order: deleting the live coordinate at the cut fixes the strict prefix.

@[reducible]

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

The forward map of the Bob-reveal pushforward (mirror): read off the live coordinate i = π_X[k_X+1] and delete it from the Alice-block order.

Equations

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

theorem CommutingRepetition.BobRevealDatum.toReveal_i {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.toReveal.i = d.liveIdx

theorem CommutingRepetition.BobRevealDatum.toReveal_LXp {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.toReveal.LX = d.LXp.erase d.liveIdx

theorem CommutingRepetition.BobRevealDatum.toReveal_LY {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.toReveal.LY = d.LY

theorem CommutingRepetition.BobRevealDatum.toReveal_kX {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : ↑d.toReveal.kX = ↑d.kX

theorem CommutingRepetition.BobRevealDatum.toReveal_kY {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : ↑d.toReveal.kY = ↑d.kY

theorem CommutingRepetition.BobRevealDatum.law_toReveal {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.law = d.toReveal.revealLaw

The forward map matches the laws pointwise (mirror).

theorem CommutingRepetition.BobRevealDatum.toReveal_πX_of_lt {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) (t : Fin d.toReveal.LX.card) (s : Fin d.LXp.card) (hval : ↑t = ↑s) (hlt : ↑s < ↑d.kX) : ↑(d.toReveal.πX t) = ↑(d.πX s)

Below the cut, the surgered Alice-block order agrees with the original order (mirror).

@[reducible]

def CommutingRepetition.RevealDatum.toAliceReveal {n : ℕ} {D : Finset (Fin n)} (d₀ : RevealDatum n D) : AliceRevealDatum n D

The reverse map of the Alice-reveal pushforward: re-insert the live coordinate into the Bob-block order at the cut.

Equations

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

@[reducible]

def CommutingRepetition.RevealDatum.toBobReveal {n : ℕ} {D : Finset (Fin n)} (d₀ : RevealDatum n D) : BobRevealDatum n D

The reverse map of the Bob-reveal pushforward (mirror).

Equations

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

def CommutingRepetition.aliceRevealEquiv (n : ℕ) (D : Finset (Fin n)) : AliceRevealDatum n D ≃ RevealDatum n D

The Alice-reveal pushforward bijection: delete the live coordinate from the order, with re-insertion at the cut as inverse.

Equations

• CommutingRepetition.aliceRevealEquiv n D = { toFun := CommutingRepetition.AliceRevealDatum.toReveal, invFun := CommutingRepetition.RevealDatum.toAliceReveal, left_inv := ⋯, right_inv := ⋯ }

def CommutingRepetition.bobRevealEquiv (n : ℕ) (D : Finset (Fin n)) : BobRevealDatum n D ≃ RevealDatum n D

The Bob-reveal pushforward bijection (mirror).

Equations

• CommutingRepetition.bobRevealEquiv n D = { toFun := CommutingRepetition.BobRevealDatum.toReveal, invFun := CommutingRepetition.RevealDatum.toBobReveal, left_inv := ⋯, right_inv := ⋯ }

theorem CommutingRepetition.aliceReveal_pushforward_eq (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

The Alice-reveal reverse experiment has exactly the forward law (node 1.2.8; 05_prerounding.tex, "Both reverse experiments have exactly the forward law", verified against eq forward-outcome-probability): there is a bijection from Alice-reveal reverse data to forward reveal data — read off the live coordinate i = π_Y[k_Y+1], delete it from the order — matching the laws pointwise and the derived public data: the live coordinate, the two blocks, and the two cut values are carried over unchanged. (Order compatibility across the bijection — the prefix structure the martingale filtration consumes — is stated with the operator half of node 1.2.8.)

theorem CommutingRepetition.bobReveal_pushforward_eq (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

The Bob-reveal reverse experiment has exactly the forward law (node 1.2.8, mirror statement).