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

theorem CommutingRepetition.pushHEqFin {m m' : ℕ} : m = m' → ∀ (a : Fin m) (b : Fin m'), ↑a = ↑b → a ≍ b

theorem CommutingRepetition.pushHEqEquiv {n : ℕ} {S S' : Finset (Fin n)} : S = S' → ∀ (E : Fin S.card ≃ ↥S) (E' : Fin S'.card ≃ ↥S'), (∀ (t : Fin S.card) (t' : Fin S'.card), ↑t = ↑t' → ↑(E t) = ↑(E' t')) → E ≍ E'

theorem CommutingRepetition.pushAliceExt {n : ℕ} {D : Finset (Fin n)} (a b : AliceRevealDatum n D) : a.LX = b.LX → a.LYp = b.LYp → a.πX ≍ b.πX → a.πY ≍ b.πY → a.kX ≍ b.kX → a.kY ≍ b.kY → a = b

theorem CommutingRepetition.pushBobExt {n : ℕ} {D : Finset (Fin n)} (a b : BobRevealDatum n D) : a.LXp = b.LXp → a.LY = b.LY → a.πX ≍ b.πX → a.πY ≍ b.πY → a.kX ≍ b.kX → a.kY ≍ b.kY → a = b

theorem CommutingRepetition.pushRevealExt {n : ℕ} {D : Finset (Fin n)} (a b : RevealDatum n D) : a.i = b.i → a.LX = b.LX → a.LY = b.LY → a.πX ≍ b.πX → a.πY ≍ b.πY → a.kX ≍ b.kX → a.kY ≍ b.kY → a = b

theorem CommutingRepetition.pushInsEval {n : ℕ} (S' : Finset (Fin n)) (i' : Fin n) (h' : i' ∉ S') (π' : Fin S'.card ≃ ↥S') (k' : Fin (S'.card + 1)) (hcc : (insert i' S').card = S'.card + 1) (z : Fin (insert i' S').card) (j : Fin S'.card) : Fin.cast hcc z = k'.succAbove j → ↑(((finCongr hcc).trans ((finSuccEquiv' k').trans (π'.optionCongr.trans (Finset.subtypeInsertEquivOption h').symm))) z) = ↑(π' j)

theorem CommutingRepetition.pushInsEvalCut {n : ℕ} (S' : Finset (Fin n)) (i' : Fin n) (h' : i' ∉ S') (π' : Fin S'.card ≃ ↥S') (k' : Fin (S'.card + 1)) (hcc : (insert i' S').card = S'.card + 1) (z : Fin (insert i' S').card) : Fin.cast hcc z = k' → ↑(((finCongr hcc).trans ((finSuccEquiv' k').trans (π'.optionCongr.trans (Finset.subtypeInsertEquivOption h').symm))) z) = i'

theorem CommutingRepetition.pushDelEval {n : ℕ} (S : Finset (Fin n)) (u : Fin n) (π : Fin S.card ≃ ↥S) (hb : (S.erase u).card = S.card - 1) (hN : S.card - 1 + 1 = S.card) (P : Fin (S.card - 1 + 1)) (hIff : ∀ (a : Fin (S.card - 1 + 1)), a ≠ P ↔ ↑(((finCongr hN).trans π) a) ≠ u) (hg : ∀ (j : Fin n), j ∈ S ∧ j ≠ u ↔ j ∈ S.erase u) (t : Fin (S.erase u).card) : ↑(((finCongr hb).trans ((finSuccAboveEquiv P).trans ((((finCongr hN).trans π).subtypeEquiv hIff).trans ((Equiv.subtypeSubtypeEquivSubtypeInter (fun (x : Fin n) => x ∈ S) fun (x : Fin n) => x ≠ u).trans (Equiv.subtypeEquivRight hg))))) t) = ↑(π (Fin.cast hN (P.succAbove (Fin.cast hb t))))

theorem CommutingRepetition.pushSuccAboveVal {m₁ m₂ : ℕ} (p₁ : Fin (m₁ + 1)) (p₂ : Fin (m₂ + 1)) (j₁ : Fin m₁) (j₂ : Fin m₂) : ↑p₁ = ↑p₂ → ↑j₁ = ↑j₂ → ↑(p₁.succAbove j₁) = ↑(p₂.succAbove j₂)

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).