The Bob reverse datum as (base, interior cut)

def CommutingRepetition.mkBobDatum {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) : BobRevealDatum n D

The Bob reverse datum with base b (Bob block b.1.1) and interior cut k in the Alice block.

Equations

• CommutingRepetition.mkBobDatum b k = { LXp := Dᶜ \ ↑b.fst, LY := ↑b.fst, disjoint := ⋯, partition := ⋯, πX := b.snd.2.1, πY := b.snd.1, kX := k, kY := b.snd.2.2 }

theorem CommutingRepetition.BobRevealDatum.LY_subset_compl {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.LY ⊆ Dᶜ

theorem CommutingRepetition.BobRevealDatum.LXp_eq {n : ℕ} {D : Finset (Fin n)} (d : BobRevealDatum n D) : d.LXp = Dᶜ \ d.LY

def CommutingRepetition.bobSigmaEquiv {n : ℕ} (D : Finset (Fin n)) : (b : AliceBase n D) × Fin (Dᶜ \ ↑b.fst).card ≃ BobRevealDatum n D

The (base, cut) presentation of the Bob reverse datum.

Equations

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

theorem CommutingRepetition.mkBobDatum_law {n : ℕ} {D : Finset (Fin n)} (hm : D.card < n) (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) : (mkBobDatum b k).law = 2 / ↑(n - D.card) * b.β

The Bob size-biased law in (base, cut) form: (2/m)·β(base) (eq bob-size-biased-partition).

Label identities (mirror)

theorem CommutingRepetition.mkBobDatum_liveIdx {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) : (mkBobDatum b k).liveIdx = ↑(b.πY k)

theorem CommutingRepetition.mkBobDatum_revealPrefix {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) : (mkBobDatum b k).revealPrefix (mkBobDatum b k).kX.castSucc = ordPrefix b.πY ↑k

theorem CommutingRepetition.mkBobDatum_bobPrefixY {n : ℕ} {D : Finset (Fin n)} (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) : (mkBobDatum b k).bobPrefixY = ordPrefix b.snd.1 ↑b.snd.2.2

theorem CommutingRepetition.RevealDatum.CY_of_bob {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) (hLY : r.LY = (mkBobDatum b k).LY) (hpre : r.prefixX = (mkBobDatum b k).revealPrefix (mkBobDatum b k).kX.castSucc) : r.CY = b.SA ∪ ordPrefix b.πY ↑k

C_Y = S_A ∪ π_X^{≤ k_X} (Bob's background plus the revealed Alice-block prefix) for the forward datum wired to (b, k).

theorem CommutingRepetition.RevealDatum.insert_CY_of_bob {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) (hi : r.i = (mkBobDatum b k).liveIdx) (hLY : r.LY = (mkBobDatum b k).LY) (hpre : r.prefixX = (mkBobDatum b k).revealPrefix (mkBobDatum b k).kX.castSucc) : insert r.i r.CY = insert (↑(b.πY k)) (b.SA ∪ ordPrefix b.πY ↑k)

theorem CommutingRepetition.RevealDatum.insert_CX_of_bob {n : ℕ} {D : Finset (Fin n)} (r : RevealDatum n D) (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) (hi : r.i = (mkBobDatum b k).liveIdx) (hLX : r.LX = (mkBobDatum b k).LXp.erase (mkBobDatum b k).liveIdx) (hpy : r.prefixY = (mkBobDatum b k).bobPrefixY) : insert r.i r.CX = b.SB

The KEY collapse on the Bob side: {i} ∪ C_X = D ∪ L_X⁺ ∪ π_Y^{≤ k_Y}, independent of the interior cut.

Unnormalizing the block law (Bob)

theorem CommutingRepetition.block_unnormalizeB {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] [Nonempty X] [Nonempty Y] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (L : Finset (Fin n)) (xw : Fin n → X) (F : (↥L → Y) → ℝ) (Bnd : ℝ) (h : ∏ c : ↥L, ∑ v : Y, μ (xw ↑c) v ≠ 0 → ∑ ω : ↥L → Y, ((∏ c : ↥L, μ (xw ↑c) (ω c)) / ∏ c : ↥L, ∑ v : Y, μ (xw ↑c) v) * F ω ≤ Bnd) : ∑ ω : ↥L → Y, (∏ c : ↥L, μ (xw ↑c) (ω c)) * F ω ≤ (∏ c : ↥L, ∑ v : Y, μ (xw ↑c) v) * Bnd

theorem CommutingRepetition.sum_split_commY {n : ℕ} {Y : Type} [Fintype Y] [DecidableEq Y] [Nonempty Y] (L : Finset (Fin n)) (F : (Fin n → Y) → ℝ) : ∑ yw : Fin n → Y, F yw = ∑ g : { j : Fin n // j ∉ L } → Y, ∑ ω : ↥L → Y, F ((wordSplit L Y).symm (ω, g))

Split a Bob word sum at a block and put the off-block values outside.

theorem CommutingRepetition.sum4_rearrangeB {α β γ δ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] (Q : β → γ → ℝ) (w : β → γ → δ → ℝ) (X : α → β → γ → δ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, Q b c * ∑ d : δ, w b c d * X a b c d = ∑ b : β, ∑ d : δ, ∑ c : γ, Q b c * (w b c d * ∑ a : α, X a b c d)

The Bob-side rearrangements: the cut index outermost and the Alice word innermost.

theorem CommutingRepetition.sum3_rearrangeB {β γ δ : Type} [Fintype β] [Fintype γ] [Fintype δ] (Q : β → γ → ℝ) (w Y : β → γ → δ → ℝ) : ∑ b : β, ∑ c : γ, Q b c * ∑ d : δ, w b c d * Y b c d = ∑ b : β, ∑ d : δ, ∑ c : γ, Q b c * (w b c d * Y b c d)

The per-base telescoping bound (Bob)

noncomputable def CommutingRepetition.TracialStrategy.alignIncB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype 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] {Ffam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A) → Af → S.M.A} {Gfam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B) → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (b : AliceBase n D) (k : Fin (Dᶜ \ ↑b.fst).card) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : ℝ

The Bob alignment increment at base b and interior cut k: Alice's label is fixed at S_B = D ∪ L_X⁺ ∪ π_Y^{≤k_Y}, Bob's grows from S_A ∪ π_X^{≤k} to {π_X(k)} ∪ S_A ∪ π_X^{≤k}.

Equations

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

noncomputable def CommutingRepetition.TracialStrategy.alignEntB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [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 → ℝ) (b : AliceBase n D) (xw : Fin n → X) (yw : Fin n → Y) (zD : (↥D → A) × (↥D → B)) : ℝ

The initial-pairing entropy on the Bob side: Alice at S_B, Bob at S_A.

Equations

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

theorem CommutingRepetition.TracialStrategy.cutSumB_block_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A) → Af → S.M.A} {Gfam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B) → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (hrow : R.RowEntropyBudget) (htotF : ∀ (s : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A)), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → 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) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (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) (b : AliceBase n D) (xw : Fin n → X) (zD : (↥D → A) × (↥D → B)) (g : { j : Fin n // j ∉ b.LYp } → Y) : ∑ ω : ↥b.LYp → Y, (∏ j : Fin n, μ (xw j) ((wordSplit b.LYp Y).symm (ω, g) j)) * (w xw ((wordSplit b.LYp Y).symm (ω, g)) zD.1 zD.2 * ∑ k : Fin (Dᶜ \ ↑b.fst).card, S.alignIncB R b k xw ((wordSplit b.LYp Y).symm (ω, g)) zD) ≤ ∑ ω : ↥b.LYp → Y, (∏ j : Fin n, μ (xw j) ((wordSplit b.LYp Y).symm (ω, g) j)) * (w xw ((wordSplit b.LYp Y).symm (ω, g)) zD.1 zD.2 * S.alignEntB μ b xw ((wordSplit b.LYp Y).symm (ω, g)) zD)

Block bound at a fixed Bob background (mirror of cutSumA_block_le, via scenMartB_rowBudget_mkBLabel).

theorem CommutingRepetition.TracialStrategy.cutSumB_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) {Ffam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A) → Af → S.M.A} {Gfam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B) → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (hrow : R.RowEntropyBudget) (htotF : ∀ (s : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A)), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → 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) → ℝ) (hw0 : ∀ (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B), 0 ≤ w xw yw zA zB) (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) (b : AliceBase n D) : ∑ k : Fin (Dᶜ \ ↑b.fst).card, ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * S.alignIncB R b k xw yw zD ≤ ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * S.alignEntB μ b xw yw zD

Per-base telescoped bound, Bob side (mirror of cutSumA_le).

The size-bias entropy step (Bob)

theorem CommutingRepetition.TracialStrategy.sizeBiasB {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) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) (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) (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 = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * (S.M.τ (star S.σ * (S.coreEffectA D xw (mkExtA D zD.1) * S.σ * S.coreEffectB D yw (mkExtB D zD.2)))).re) (hppos : 0 < p) (hm : D.card < n) : ∑ b : AliceBase n D, b.β * ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * S.alignEntB μ b xw yw zD ≤ p * Real.log ((↑(Fintype.card A) * ↑(Fintype.card B)) ^ D.card / p)

The size-bias entropy bound, Bob side (mirror of sizeBiasA; the pairing is Alice at S_B, Bob at S_A, again a covering pair containing the core).

The Bob conjunct

theorem CommutingRepetition.TracialStrategy.alignSumB_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)} {Af Bf : Type} [Fintype Af] [Fintype Bf] (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) {Ffam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A) → Af → S.M.A} {Gfam : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B) → Bf → S.M.A} (R : ResolverArena S.M Ffam Gfam) (htotF : ∀ (s : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → A)), ∑ a : Af, Ffam s a = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2) (htotG : ∀ (t : Finset (Fin n) × (Fin n → X) × (Fin n → Y) × (Fin n → B)), ∑ b : Bf, Gfam t b = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2) (hrow : R.RowEntropyBudget) (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) (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 = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * (S.M.τ (star S.σ * (S.coreEffectA D xw (mkExtA D zD.1) * S.σ * S.coreEffectB D yw (mkExtB D zD.2)))).re) (hppos : 0 < p) (hm : D.card < n) : ∑ r : RevealDatum n D, r.revealLaw * ∑ xw : Fin n → X, ∑ yw : Fin n → Y, (∏ j : Fin n, μ (xw j) (yw j)) * ∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * ‖R.branch S.σ (mkALabel D (insert r.i r.CX) xw yw zD.1) (mkBLabel D (insert r.i r.CY) xw yw zD.2) - R.branch S.σ (mkALabel D (insert r.i r.CX) xw yw zD.1) (mkBLabel D r.CY xw yw zD.2)‖ ^ 2 ≤ 2 * p * (Real.log p⁻¹ + ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))) / (↑n - ↑D.card)

The prior Bob alignment cost is at most 2p(t₀ + s₀)/m (node 1.2.9, eq prior-alignment-bound, second conjunct; the body of alignCostB with the canonical labels).