The Alice-side scenario reveal martingale: the path space is the
Alice values on the progressively revealed block L, the law is the
product of the pinned-Bob conditional weights (normalized by the total
block mass), and the index path is the canonical Alice label at the
growing revealed set SA ∪ π[1..j], with the off-block values frozen
to the background g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The martingale's path-space Fintype instFintypeΩ is definitionally the
canonical one on ↥L → X, but only at default transparency, so this
provable (non-rfl-trivial) univ equality is not skipped by simp and
canonicalizes the summation index after simp only [scenMartA] leaves the
projected instance behind.
The Bob-side scenario reveal martingale: the path space is the Bob
values on the progressively revealed block L, the law is the
pinned-Alice conditional weight (normalized by the block mass), and the
index path is the canonical Bob label at the growing revealed set
SA ∪ π[1..j], freezing the off-block values to a background g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bob-side Fintype canonicalization (mirror of scenMartA_univ_eq).
Block-law renormalization, Alice (node 1.2.9 assembly step (2)):
the scenario law times the total block mass M₀ is the unnormalized
block product weight ∏_{c∈L} μ(ω c, yw c). This converts the
martingale's law-weighted block-value sum into the alignCostA
reference-word prior sum after the wordSplit at L.
Block-law renormalization, Bob (mirror of scenMartA_law_mul_M0).
The scenario martingale is a mean tower for the arena's Alice
totals: on each fiber of the current canonical label, the law-weighted
average of the next revealed-set effect is the current one
(setEffectA_reveal, fiber-refined).
Alice-column budget, consumed on the scenario martingale (node
1.2.6 → 1.2.9 bridge): the reveal-martingale mean tower feeds the signed
column budget, so the total law-weighted squared L²-increment of the
branch vectors along the Alice scenario reveal (block L, background
SA, pinned Bob index j) is at most the scalar entropy H₁ of the
initial branch pairing. This is the per-scenario budget consumption that
node 1.2.9 telescopes at the uniform cut.
The Bob scenario martingale is a mean tower for the arena's Bob
totals (setEffectB_reveal, fiber-refined).
Bob-row budget, consumed on the scenario martingale (mirror of
scenMartA_colBudget): feeding the Bob mean tower to RowEntropyBudget
bounds the total law-weighted squared L²-increment of the branch vectors
(second slot) along the Bob scenario reveal by the scalar entropy H₁ of
the initial branch pairing.
Single cut-step column budget (node 1.2.9 assembly step (1)):
dropping the other nonnegative reveal steps, the law-weighted squared
increment at any single step k is bounded by the same scalar entropy
H₁. This is the per-datum cut increment that node 1.2.9 identifies
with the alignCostA integrand.
Single cut-step row budget (Bob-side mirror of
scenMartA_cut_le).
Column budget in canonical-label form (node 1.2.9 assembly bridge):
scenMartA_colBudget with the martingale's .idx steps expanded via
scenMartA_idx/ordPrefix_succ into the mkALabel canonical labels that the
alignCostA integrand (through the aLabel = mkALabel rfl bridge and the
reveal-datum wiring revealMartA_cut(Succ)_eq_effectiveH(Bar)) actually names.
The total, over all reveal steps s, of the law-weighted squared branch
increment ‖φ_{insert (π s) prefix} − φ_{prefix}‖² against a fixed Bob index
J is bounded by H₁ of the initial pairing (label at the background SA).
Node 1.2.9 identifies each alignCostA cut-datum (at cut kY) with the step
s = kY (prefix = SA ∪ ordPrefix π kY = C_X,
insert (π kY) prefix = insert i C_X); summing the cut-data over the uniform
interior cut kY : Fin L.card reconstructs this ∑ s telescoping sum, because
the Bob index bLabel (insert i C_Y) = bLabel (D ∪ L ∪ alicePrefixX) is
kY-independent (insert i C_Y collapses off the live coordinate).
Row budget in canonical-label form (Bob-side mirror of
scenMartA_colBudget_mkALabel), for the alignCostB cut assembly.