structure CommutingRepetition.EffectMartingale (I : Type) (steps : ℕ) : Type 1

A finite effect-martingale datum (05_prerounding.tex, eqs alice-reveal-martingale, bob-reveal-martingale, abstracted): a finite path space Ω with a probability law and, at each of steps + 1 times, an index into the effect family, deterministic at time 0 (the background-conditioned mean, eq alice-reveal-martingale at j = 0). The martingale property relative to a family is IsMeanTower below.

• Ω : Type
• instFintypeΩ : Fintype self.Ω
• law : self.Ω → ℝ
• law_nonneg (ω : self.Ω) : 0 ≤ self.law ω
• law_sum : ∑ ω : self.Ω, self.law ω = 1
• idx : Fin (steps + 1) → self.Ω → I
• idx_zero (ω ω' : self.Ω) : self.idx 0 ω = self.idx 0 ω'

def CommutingRepetition.EffectMartingale.IsMeanTower {I : Type} {steps : ℕ} [DecidableEq I] {M : StdTracialAlgebra} (X : EffectMartingale I steps) (E : I → M.A) : Prop

The mass-weighted martingale condition relative to a family E : I → M.A (the tower property making eq alice-reveal-martingale a "positive-contraction martingale"): on each fiber of the time-s index, the law-weighted sum of the time-(s+1) family elements equals the fiber mass times the current element. Division-free, so zero-mass fibers carry no condition; conditioning on the index fiber is implied by conditioning on any finer background, so this hypothesis is weaker than the manuscript's question filtration.

Equations

• X.IsMeanTower E = ∀ (s : Fin steps) (i : I), ↑(∑ ω : X.Ω with X.idx s.castSucc ω = i, X.law ω) • E i = ∑ ω : X.Ω with X.idx s.castSucc ω = i, ↑(X.law ω) • E (X.idx s.succ ω)

def CommutingRepetition.ResolverArena.ColEntropyBudget {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} [DecidableEq I] (R : ResolverArena M F G) : Prop

The Alice-column entropy budget (node 1.2.6, consumed form; 04_resolver_corner.tex eq alice-resolver-entropy telescoped and σ-paired per 05_prerounding.tex eqs positive-functional through random-martingale-increment): for every effect martingale over the Alice totals, every unit density, and every fixed Bob index, the total law-weighted squared L²-increment of the branch vectors along the martingale is at most the scalar entropy H₁ = Real.negMulLog of the initial branch pairing re τ(σ* F_{i₀} σ G_j) (the branch probability of eq functional-probability-bridge). The per-step factor 1/N_A of eq random-martingale-increment is the uniform cut and stays in section 5.

Equations

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

def CommutingRepetition.ResolverArena.RowEntropyBudget {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} [DecidableEq J] (R : ResolverArena M F G) : Prop

The Bob-row entropy budget (node 1.2.6, consumed form; the adjoint-oriented mirror, 04_resolver_corner.tex eq bob-resolver-entropy telescoped and σ-paired): martingale over the Bob totals, fixed Alice index, increments in the second branch slot.

Equations

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

theorem CommutingRepetition.resolver_arena_entropic (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [Nonempty A] [Nonempty B] (F : I → A → M.A) (G : J → B → M.A) (hF : ∀ (i : I) (a : A), IsPosElem (F i a)) (hG : ∀ (j : J) (b : B), IsPosElem (G j b)) (hF1 : ∀ (i : I), IsPosElem (1 - ∑ a : A, F i a)) (hG1 : ∀ (j : J), IsPosElem (1 - ∑ b : B, G j b)) : ∃ (R : ResolverArena M F G), R.ColEntropyBudget ∧ R.RowEntropyBudget

Entropic resolver arena (nodes 1.2.5 + 1.2.6; 04_resolver_corner.tex, thm common-resolver-arena together with lem resolver-entropy-cutoffs in the consumed form of DIFFERENCES.md D15): every pair of finite refined [0,1]-effect families over nonempty answer sets admits a resolver arena satisfying both telescoped entropy budgets. The budgets hold for the corner construction (the Cornered vocabulary of Resolver/EntropyLemma.lean), not for an arbitrary arena, so they are part of the existence claim.