The Alice reverse datum as (base, interior cut) #
An Alice reverse base: the Alice block L_X ⊆ Dᶜ (the Bob block is
L_Y⁺ = Dᶜ \ L_X), the forward order π_X, the reverse order π_Y, and the
forward cut k_X. The interior cut k_Y ∈ Fin |L_Y⁺| is split off
(aliceSigmaEquiv), because the alignment integrand is summed over it
uniformly (eq IA-size-bias-calculation).
Equations
Instances For
Bob's fixed revealed set D ∪ L_Y⁺ ∪ π_X^{≤ k_X} (the set behind
aliceFixedBobEffect_eq_effectiveK, cut-independent).
Instances For
The size-biased law of a datum in (base, cut) form: (2/m)·β(base) (the
factor (2N_A/m)·(1/N_A) = 2/m of eq size-biased-partition; the cut's
existence forces N_A > 0).
The base weights sum to one: fair partitions 2^{-m} over the 2^m
Alice blocks, uniform orders and forward cut (eq size-biased-partition,
"the last sum of the fair-partition weights is at most one" — here exact).
Label identities for a datum in (base, cut) form (STEP 1 of the roadmap) #
C_X = S_A ∪ π_Y^{≤ k_Y} for the forward datum wired to (b, k).
{i} ∪ C_X = {π_Y(k_Y)} ∪ (S_A ∪ π_Y^{≤ k_Y}).
The KEY collapse: {i} ∪ C_Y = D ∪ L_Y⁺ ∪ π_X^{≤ k_X} = S_B, independent of the
cut k_Y (the set behind aliceFixedBobEffect_eq_effectiveK).
Unnormalizing the block law #
Convert a bound on a block-law-weighted sum (the martingale's normalized
law ∏μ / M₀) into a bound on the raw-prior-weighted sum, with the block
mass M₀ as the factor; at M₀ = 0 every raw block weight vanishes.
The size-bias identities (STEP 4 of the roadmap) #
Collapse of the prior pairing to the core mass: for revealed sets
S_A ⊇ D, S_B ⊇ D covering every coordinate, the prior-weighted pairing of the
two revealed-set effects, summed over the core answers with the D-measurable
weight, is exactly the weighted core mass p (pairSum_eq_core, the tower
property). This is the identity ∑ wᵢ hᵢ = p behind eq accepted-word-entropy.
Total prior weight: the [0,1]-weighted prior mass over the core answers
is at most the number (|A||B|)^{|D|} of core answer words ("the accepted words
have number at most e^{s₀}").
Sum rearrangements #
Split a word sum at a block and put the off-block values outside.
The per-base telescoping bound (STEPS 2–3 of the roadmap) #
The alignment increment at base b and interior cut k: the squared
branch-vector increment between the Alice labels at S_A ∪ π_Y^{≤k} and at
{π_Y(k)} ∪ S_A ∪ π_Y^{≤k}, against Bob's cut-independent label at S_B
(the alignCostA integrand read through insert_CX_of_alice /
insert_CY_of_alice).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar entropy H₁ of the initial branch pairing at base b:
H₁(re τ(σ* F_{S_A} σ G_{S_B})) — H₁(p_z(U_A)) of eq
random-martingale-increment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Block bound at a fixed Alice background (eqs random-martingale-increment
summed over the uniform cut, via scenMartA_colBudget_mkALabel): for fixed Bob
word yw, core answers zD and off-block Alice values g, the raw-prior-weighted
sum over the Bob-block values ω of the cut-summed increments is at most the
same weighted sum of the initial-pairing entropy.
Per-base telescoped bound (STEPS 2–3 of the roadmap): at a fixed base, the uniform interior cut sums the alignment increments into the column budget, so the prior-weighted cut-sum is at most the prior-weighted initial-pairing entropy.
The size-bias entropy step (STEP 4 of the roadmap) #
Reshaping the base-indexed flat sums into nested sums.
The size-bias entropy bound (eqs accepted-word-logsum,
accepted-word-entropy, in the weighted form of
finite_weighted_entropy_le_of_weight_bound): the base-weighted prior average of
the initial-pairing entropies is at most p·log(N/p), N = (|A||B|)^{|D|},
because the same weights average the pairings themselves to exactly p
(sum_pairing_eq_coreMass) and have total mass at most N
(sum_prior_weight_le, AliceBase.sum_β).
The Alice conjunct #
The prior Alice alignment cost is at most 2p(t₀ + s₀)/m (node 1.2.9,
eqs IA-size-bias-calculation, prior-alignment-bound; the body of alignCostA
with the canonical labels mkALabel/mkBLabel).