noncomputable def CommutingRepetition.weightedAvg {ι : Type u_1} [Fintype ι] {V : Type u_2} [AddCommMonoid V] [Module ℂ V] (w : ι → ℝ) (f : ι → V) : V

Average of a family of vectors in a ℂ-module under a real weight function: (∑ w)⁻¹ • ∑ᵢ wᵢ • fᵢ. With Lean's 0⁻¹ = 0 convention the value is 0 at zero total mass; every consuming statement guards its mass. Auxiliary.

Equations

• CommutingRepetition.weightedAvg w f = (↑(∑ i : ι, w i))⁻¹ • ∑ i : ι, ↑(w i) • f i

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

The (T₀, X_i)-conditioned unnormalized law of Alice's full question word: consistency with the revealed values on C_X ∪ {i}, times the pinned-Bob halves of the free coordinates' joint laws (every coordinate outside C_X ∪ {i} lies in C_Y by eq reveal-cover).

Equations

• d.xWeight μ x₀ y₀ w = if CommutingRepetition.agreesOn (insert d.i d.CX) w x₀ then ∏ j ∈ (insert d.i d.CX)ᶜ, μ (w j) (y₀ j) else 0

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

The (T₀, Y_i)-conditioned unnormalized law of Bob's full question word.

Equations

• d.yWeight μ x₀ y₀ v = if CommutingRepetition.agreesOn (insert d.i d.CY) v y₀ then ∏ j ∈ (insert d.i d.CY)ᶜ, μ (x₀ j) (v j) else 0

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

The doubly revealed coordinates' contribution: the joint law at the pinned values on (C_X ∪ {i}) ∩ (C_Y ∪ {i}).

Equations

• d.pinnedWeight μ x₀ y₀ = ∏ j ∈ insert d.i d.CX ∩ insert d.i d.CY, μ (x₀ j) (y₀ j)

theorem CommutingRepetition.RevealDatum.xWeight_nonneg {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ : Fin n → Y) (w : Fin n → X) : 0 ≤ d.xWeight μ x₀ y₀ w

theorem CommutingRepetition.RevealDatum.yWeight_nonneg {n : ℕ} {X Y : Type} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ v : Fin n → Y) : 0 ≤ d.yWeight μ x₀ y₀ v

theorem CommutingRepetition.RevealDatum.priorWeight_eq_mul {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) (w : Fin n → X) (v : Fin n → Y) : priorWeight d μ x₀ y₀ w v = d.pinnedWeight μ x₀ y₀ * (d.xWeight μ x₀ y₀ w * d.yWeight μ x₀ y₀ v)

Weight factorization (node 1.2.4 bridge; eq reveal-cover ⇒ eq prior-factorization): the symmetric (T₀, X_i, Y_i)-conditioned prior weight splits into the doubly pinned block times the two one-sided conditioned laws. This is the exact form of reviewer #7's note-N3 bridge: it makes the one-sided weights the marginals of the symmetric conditioning.

theorem CommutingRepetition.RevealDatum.priorWeight_mass_eq {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) : ∑ w : Fin n → X, ∑ v : Fin n → Y, priorWeight d μ x₀ y₀ w v = d.pinnedWeight μ x₀ y₀ * ((∑ w : Fin n → X, d.xWeight μ x₀ y₀ w) * ∑ v : Fin n → Y, d.yWeight μ x₀ y₀ v)

Total-mass factorization: summing priorWeight_eq_mul over both words (Fubini).

noncomputable def CommutingRepetition.TracialStrategy.coreEffectA {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (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) : S.M.A

Alice's core effect E_{x^n}^{a_D}: the repeated POVM effect at the question word w summed over all answer words agreeing with the core answer word zA on D (05_prerounding.tex, "Let E_{x^n}^{a_D} and F_{y^n}^{b_D} be the repeated POVM effects after summing all answers outside D"). The core word is carried by a full-word representative; only its D-coordinates matter.

Equations

• S.coreEffectA D w zA = ∑ as : Fin n → A, if CommutingRepetition.agreesOn D as zA then S.E w as else 0

noncomputable def CommutingRepetition.TracialStrategy.coreEffectB {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq 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) : S.M.A

Bob's core effect F_{y^n}^{b_D}.

Equations

• S.coreEffectB D v zB = ∑ bs : Fin n → B, if CommutingRepetition.agreesOn D bs zB then S.F v bs else 0

theorem CommutingRepetition.TracialStrategy.coreEffectA_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq 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 (S.coreEffectA D w zA)

theorem CommutingRepetition.TracialStrategy.coreEffectB_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq 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 (S.coreEffectB D v zB)

theorem CommutingRepetition.TracialStrategy.coreEffect_correlation {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D : Finset (Fin n)) (w : Fin n → X) (v : Fin n → Y) (zA : Fin n → A) (zB : Fin n → B) : (∑ as : Fin n → A, ∑ bs : Fin n → B, if agreesOn D as zA ∧ agreesOn D bs zB then S.correlation w v as bs else 0) = (S.M.τ (star S.σ * (S.coreEffectA D w zA * S.σ * S.coreEffectB D v zB))).re

Bilinear collapse of the core-answer correlation mass: the probability of answering consistently with the core word z = (zA, zB) at questions (w, v) is the trace pairing of the two core effects (05_prerounding.tex, eq WD-t-z context with eq tracial-correlation-formula).

noncomputable def CommutingRepetition.TracialStrategy.effectiveH {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) : S.M.A

The effective Alice branch effect H_{r,x} = 𝔼[E_{X^n}^{a_D} ∣ T₀ = t, X_i = x] (05_prerounding.tex, eq effective-HK): the xWeight-average of the core effects over Alice's full question word. The reference word x₀ carries the revealed values and the live question x = x₀ i; the history's core answers are zA.

Equations

• S.effectiveH d μ x₀ y₀ zA = CommutingRepetition.weightedAvg (d.xWeight μ x₀ y₀) fun (w : Fin n → X) => S.coreEffectA D w zA

noncomputable def CommutingRepetition.TracialStrategy.effectiveK {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) : S.M.A

The effective Bob branch effect K_{r,y} = 𝔼[F_{Y^n}^{b_D} ∣ T₀ = t, Y_i = y].

Equations

• S.effectiveK d μ x₀ y₀ zB = CommutingRepetition.weightedAvg (d.yWeight μ x₀ y₀) fun (v : Fin n → Y) => S.coreEffectB D v zB

theorem CommutingRepetition.TracialStrategy.effectiveH_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) : IsPosElem (S.effectiveH d μ x₀ y₀ zA)

Effective effects are algebraically positive — "finite convex combinations of positive contractions in M" (eq effective-HK; positivity half, see the header note on contractivity).

theorem CommutingRepetition.TracialStrategy.effectiveK_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) : IsPosElem (S.effectiveK d μ x₀ y₀ zB)

noncomputable def CommutingRepetition.TracialStrategy.effectiveHLive {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) (a : A) : S.M.A

The live refinement H_{r,x}^a (05_prerounding.tex, eq live-refinements): the effective effect further restricted to live answer a at the live coordinate.

Equations

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

noncomputable def CommutingRepetition.TracialStrategy.effectiveKLive {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) (b : B) : S.M.A

The live refinement of Bob's effective effect.

Equations

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

theorem CommutingRepetition.TracialStrategy.effectiveH_eq_sum_live {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) : S.effectiveH d μ x₀ y₀ zA = ∑ a : A, S.effectiveHLive d μ x₀ y₀ zA a

H_{r,x} = ∑_a H_{r,x}^a (eq live-refinements): the live answers partition each answer word.

theorem CommutingRepetition.TracialStrategy.effectiveK_eq_sum_live {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) : S.effectiveK d μ x₀ y₀ zB = ∑ b : B, S.effectiveKLive d μ x₀ y₀ zB b

K_{r,y} = ∑_b K_{r,y}^b (eq live-refinements).

noncomputable def CommutingRepetition.TracialStrategy.effectiveHBar {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) : S.M.A

The locally describable average H̄_{r,y} = ∑_{x'} μ(x' ∣ y) H_{r,x'} (05_prerounding.tex, eq bar-HK): the effective Alice effect averaged over the live Alice question with the conditional question law given the live Bob question y = y₀ i.

Equations

• S.effectiveHBar d μ x₀ y₀ zA = CommutingRepetition.weightedAvg (fun (x' : X) => μ x' (y₀ d.i)) fun (x' : X) => S.effectiveH d μ (Function.update x₀ d.i x') y₀ zA

noncomputable def CommutingRepetition.TracialStrategy.effectiveKBar {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)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) : S.M.A

The locally describable average K̄_{r,x} = ∑_{y'} μ(y' ∣ x) K_{r,y'} (eq bar-HK).

Equations

• S.effectiveKBar d μ x₀ y₀ zB = CommutingRepetition.weightedAvg (fun (y' : Y) => μ (x₀ d.i) y') fun (y' : Y) => S.effectiveK d μ x₀ (Function.update y₀ d.i y') zB

theorem CommutingRepetition.TracialStrategy.branch_probability_core {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) (zB : Fin n → B) : (∑ w : Fin n → X, ∑ v : Fin n → Y, priorWeight d μ x₀ y₀ w v * ∑ as : Fin n → A, ∑ bs : Fin n → B, if agreesOn D as zA ∧ agreesOn D bs zB then S.correlation w v as bs else 0) = d.pinnedWeight μ x₀ y₀ * (S.M.τ (star S.σ * ((∑ w : Fin n → X, ↑(d.xWeight μ x₀ y₀ w) • S.coreEffectA D w zA) * S.σ * ∑ v : Fin n → Y, ↑(d.yWeight μ x₀ y₀ v) • S.coreEffectB D v zB))).re

Exact branch probability, division-free core (node 1.2.4; 05_prerounding.tex, eq branch-probability via eq prior-factorization): the prior-weighted core-answer correlation mass equals the pinned-block weight times the trace pairing of the unnormalized weighted core effects. Dividing by the total mass (branch_probability below) gives the manuscript's p_r(x,y) = τ(σ* H_{r,x} σ K_{r,y}).

theorem CommutingRepetition.TracialStrategy.branch_probability {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) (zB : Fin n → B) (hmass : 0 < ∑ w : Fin n → X, ∑ v : Fin n → Y, priorWeight d μ x₀ y₀ w v) : (∑ w : Fin n → X, ∑ v : Fin n → Y, priorWeight d μ x₀ y₀ w v * ∑ as : Fin n → A, ∑ bs : Fin n → B, if agreesOn D as zA ∧ agreesOn D bs zB then S.correlation w v as bs else 0) / ∑ w : Fin n → X, ∑ v : Fin n → Y, priorWeight d μ x₀ y₀ w v = (S.M.τ (star S.σ * (S.effectiveH d μ x₀ y₀ zA * S.σ * S.effectiveK d μ x₀ y₀ zB))).re

Exact branch probability (node 1.2.4; 05_prerounding.tex, eq branch-probability): on positive conditioning mass, the conditional probability of the core answers given (T₀, X_i, Y_i) is the trace pairing of the effective effects, p_r(x,y) = τ(σ* H_{r,x} σ K_{r,y}). The mass hypothesis is the manuscript's "Question conditionals are used only on positive marginal support".

Candidates and the ideal answer law (node 1.2.7)

The consumed corner layer of 05_prerounding.tex, "The common finite resolver corner" (eqs normalized-candidates, candidate-positivity-order, ideal-answer-law): normalized candidate vectors from arena branches, the ideal answer law as the ratio of the arena's two exact identities, and the positivity orders that keep the local denominators nonzero on positive posterior edges. The specific wiring of labels s = (i, r, x), t = (i, r, y), the fallback choices at zero edges, and the assembly into a PreroundedStrategy are node 1.2.11.

noncomputable def CommutingRepetition.ResolverArena.candidate {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] {F : I → A → M.A} {G : J → B → M.A} (R : ResolverArena M F G) (σ : M.A) (i : I) (j : J) : R.N.H

The normalized candidate vector u = Φ/‖Φ‖ of eq normalized-candidates (with Lean's 0⁻¹ = 0, the zero branch yields the zero vector; the manuscript's arbitrary fixed unit vectors at zero edges are a choice of node 1.2.11 that "changes no π-average").

Equations

• R.candidate σ i j = ↑‖R.branch σ i j‖⁻¹ • R.branch σ i j

theorem CommutingRepetition.ResolverArena.candidate_norm {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] {F : I → A → M.A} {G : J → B → M.A} (R : ResolverArena M F G) (σ : M.A) (i : I) (j : J) (hb : R.branch σ i j ≠ 0) : ‖R.candidate σ i j‖ = 1

On a positive branch the candidate is a unit vector ("evaluation by the relevant positive vector functional proves strictly positive norm").

theorem CommutingRepetition.ResolverArena.candidate_answer {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] {F : I → A → M.A} {G : J → B → M.A} (R : ResolverArena M F G) (σ : M.A) (i : I) (j : J) (a : A) (b : B) (hb : R.branch σ i j ≠ 0) : inner ℂ (R.candidate σ i j) ((R.N.L (R.Ameas i a)) ((R.N.Rop (R.Bmeas j b)) (R.candidate σ i j))) = M.τ (star σ * (F i a * σ * G j b)) / M.τ (star σ * ((∑ a' : A, F i a') * σ * ∑ b' : B, G j b'))

The ideal answer law (node 1.2.7; 05_prerounding.tex, eq ideal-answer-law): on a positive branch, the normalized candidate's answer pairing is the ratio of the arena's exact refinement identity to its norm identity — ⟨u, L(A_i^a) R(B_j^b) u⟩ = τ(σ* F_i^a σ G_j^b) / τ(σ* F_i σ G_j), "which is exactly ℚ(A_i = a, B_i = b ∣ R = r, X_i = x, Y_i = y)".

theorem CommutingRepetition.TracialStrategy.effectiveKBar_sub_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zB : Fin n → B) (y : Y) : IsPosElem (S.effectiveKBar d μ x₀ y₀ zB - ↑(μ (x₀ d.i) y / ∑ y' : Y, μ (x₀ d.i) y') • S.effectiveK d μ x₀ (Function.update y₀ d.i y) zB)

Candidate positivity order, Bob side (node 1.2.7; 05_prerounding.tex, eq candidate-positivity-order): K̄_{r,x} ≽ μ(y ∣ x) K_{r,y} in the D13 cone — the bar average dominates each conditional multiple of a single live effect, because the difference is the nonnegative combination of the remaining live questions. True with the junk conventions at a vanishing live marginal (both sides collapse to 0).

theorem CommutingRepetition.TracialStrategy.effectiveHBar_sub_isPosElem {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) {D : Finset (Fin n)} (d : RevealDatum n D) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) (x₀ : Fin n → X) (y₀ : Fin n → Y) (zA : Fin n → A) (x : X) : IsPosElem (S.effectiveHBar d μ x₀ y₀ zA - ↑(μ x (y₀ d.i) / ∑ x' : X, μ x' (y₀ d.i)) • S.effectiveH d μ (Function.update x₀ d.i x) y₀ zA)

Candidate positivity order, Alice side (eq candidate-positivity-order): H̄_{r,y} ≽ μ(x ∣ y) H_{r,x}.