theorem CommutingRepetition.isPosElem_one {M : StdTracialAlgebra} : IsPosElem 1

1 is algebraically positive.

noncomputable def CommutingRepetition.TracialStrategy.refinedA {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)) (μ : X → Y → ℝ) (s : ALabel n X Y A) (as : Fin n → A) : S.M.A

The fully refined Alice effect at a label: the revealed-set average of the repeated effect at one full answer word (agreeing with the label's core word).

Equations

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

noncomputable def CommutingRepetition.TracialStrategy.refinedB {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)) (μ : X → Y → ℝ) (t : BLabel n X Y B) (bs : Fin n → B) : S.M.A

The fully refined Bob effect at a label.

Equations

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

theorem CommutingRepetition.TracialStrategy.sum_refinedA {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 → ℝ) (s : ALabel n X Y A) : ∑ as : Fin n → A, S.refinedA D μ s as = S.setEffectA D s.1 μ s.2.1 s.2.2.1 s.2.2.2

The refined effects sum to the revealed-set effect (htotF).

theorem CommutingRepetition.TracialStrategy.sum_refinedB {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 → ℝ) (t : BLabel n X Y B) : ∑ bs : Fin n → B, S.refinedB D μ t bs = S.setEffectB D t.1 μ t.2.1 t.2.2.1 t.2.2.2

theorem CommutingRepetition.TracialStrategy.refinedA_isPosElem {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) (s : ALabel n X Y A) (as : Fin n → A) : IsPosElem (S.refinedA D μ s as)

theorem CommutingRepetition.TracialStrategy.refinedB_isPosElem {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) (t : BLabel n X Y B) (bs : Fin n → B) : IsPosElem (S.refinedB D μ t bs)

theorem CommutingRepetition.TracialStrategy.one_sub_coreEffectA_isPosElem {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)) (w : Fin n → X) (zA : Fin n → A) : IsPosElem (1 - S.coreEffectA D w zA)

The complement of a core effect is positive (the remaining answer words).

theorem CommutingRepetition.TracialStrategy.one_sub_coreEffectB_isPosElem {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)) (v : Fin n → Y) (zB : Fin n → B) : IsPosElem (1 - S.coreEffectB D v zB)

theorem CommutingRepetition.TracialStrategy.one_sub_weightedAvg_isPosElem {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)) {ι : Type} [Fintype ι] (wgt : ι → ℝ) (hwgt : ∀ (i : ι), 0 ≤ wgt i) (f : ι → S.M.A) (hf : ∀ (i : ι), IsPosElem (1 - f i)) : IsPosElem (1 - weightedAvg wgt f)

A nonnegative weighted average of contractions is a contraction (the 1 - · complement is positive); junk-safe at zero total weight.

theorem CommutingRepetition.TracialStrategy.one_sub_setEffectA_isPosElem {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 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) : IsPosElem (1 - S.setEffectA D R₀ μ xref yref zA)

theorem CommutingRepetition.TracialStrategy.one_sub_setEffectB_isPosElem {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 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) : IsPosElem (1 - S.setEffectB D R₀ μ xref yref zB)

theorem CommutingRepetition.TracialStrategy.exists_refined_arena {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) : ∃ (R : ResolverArena S.M (S.refinedA D μ) (S.refinedB D μ)), R.ColEntropyBudget ∧ R.RowEntropyBudget

The entropic arena over the fully refined family (node 1.2.5 + 1.2.6 consumed at node 1.2.11).