The generalized Alice label: a revealed set, the reference words,
and an answer word. The Alice effect at a label is
setEffectA D R₀ μ xref yref zA.
Equations
Instances For
Canonical extension of a core answer assignment to a full word
(fixed default off the core — the node-1.2.11 fallback-answer pattern;
the core effects read only the D-restriction).
Equations
- CommutingRepetition.extendCoreA D zD j = if h : j ∈ D then zD ⟨j, h⟩ else Classical.arbitrary A
Instances For
Canonical extension of a core Bob assignment.
Equations
- CommutingRepetition.extendCoreB D zD j = if h : j ∈ D then zD ⟨j, h⟩ else Classical.arbitrary B
Instances For
Canonicalize a reference word to its values ON the revealed set
(fixed default elsewhere). Labels are canonicalized so that two labels
with the same effect coincide: setEffectA reads its xref only on
R₀ and its yref only off R₀, so the Alice label at R₀ keeps
xref on R₀ and yref off R₀; without this, an arena could
assign unrelated branch vectors to behaviorally identical labels and
the alignment bound would be false.
Equations
- CommutingRepetition.keepOn R₀ wd j = if j ∈ R₀ then wd j else Classical.arbitrary α
Instances For
Canonicalize a reference word to its values OFF the revealed set (fixed default on it).
Equations
- CommutingRepetition.keepOff R₀ wd j = if j ∈ R₀ then Classical.arbitrary α else wd j
Instances For
The canonical Alice label at a revealed set: pinned side kept on
R₀, weight side kept off R₀, core answers canonically extended.
Equations
- CommutingRepetition.aLabel D R₀ xw yw zD = (R₀, CommutingRepetition.keepOn R₀ xw, CommutingRepetition.keepOff R₀ yw, CommutingRepetition.extendCoreA D zD)
Instances For
The canonical Bob label: pinned side (yref) kept on R₀, weight
side (xref) kept off R₀.
Equations
- CommutingRepetition.bLabel D R₀ xw yw zD = (R₀, CommutingRepetition.keepOff R₀ xw, CommutingRepetition.keepOn R₀ yw, CommutingRepetition.extendCoreB D zD)
Instances For
The weighted core mass p = 𝔼[w_D] (05_prerounding.tex,
eq p-q-m, in the weighted run of 07 sec 7.4): questions from the
product prior, core answers from the strategy's core-effect
correlation, weighted by w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The prior Alice alignment cost I_A (05_prerounding.tex, eq
prior-alignment-costs): the ℙ⁰-weighted, w-weighted squared
distances ‖φ_{r,x,y} − φ^B_{r,y}‖² — branch vectors of the
generalized-family arena at the cut-adjacent Alice labels
({i} ∪ C_X, …) (the effective effect H_{r,x}) and (C_X, …) (the
bar H̄_{r,Y_i}), against the full Bob label ({i} ∪ C_Y, …).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The prior Bob alignment cost I_B (eq prior-alignment-costs,
second display): distances ‖φ_{r,x,y} − φ^A_{r,x}‖², the bar on the
Bob side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prior alignment bound (node 1.2.9; 05_prerounding.tex, eqs
IA-size-bias-calculation, prior-alignment-bound):
I_A, I_B ≤ 2p(t₀ + s₀)/m with t₀ = log(1/p),
s₀ = |D|·log(|A||B|), m = n − |D| — for any generalized-family
arena satisfying both entropy budgets (batch #13), any [0,1]-weight,
and the hypothesis-pinned weighted core mass. The proof consumes the
signed reverse experiments (batch #11), the reveal-martingale tower
(batch #14), the budgets telescoped at the uniform cut, and the
weighted accepted-word entropy (finite_weighted_entropy_le_of_weight_bound).
The posterior branch law ℚ (05_prerounding.tex, eq
posterior-branch-law): reveal randomness times prior questions times
the weight times the exact branch mass ‖φ_{r,x,y}‖², divided by p.
Junk-free consumption: every use divides by the hypothesis-pinned
positive p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Posterior normalization (eq posterior-branch-normalization):
the branch-norm identity and the tower property make ℚ a probability
law — the branch mass at the full labels is exactly the conditional
core-word correlation, so the total mass is p/p = 1.
Posterior alignment, Bob-candidate side (node 1.2.9;
05_prerounding.tex, eqs prerounding-normalization-inequality,
two-alignment-bounds): multiplying the normalization inequality by ℚ
cancels the ideal branch mass, so the posterior expected squared
distance between the normalized candidates u_{st} and y_{i,r,y} is
at most 4·I_A/p.
Posterior alignment, Alice-candidate side (mirror): distance to
x_{i,r,x} against I_B.
Posterior histories (node 1.2.10, closeness half) #
The flattened posterior over public histories and live questions, the
locally generated conditional laws, and the history relative-entropy
bound (05_prerounding.tex, eqs label-law-pi, J-A, J-B,
conditioning-divergence, question-answer-conditioning-budget,
JA-chain-rule, first-history-chain-term, bob-block-conditioning-budget,
bob-block-chain-rule, second-history-chain-term,
history-relative-entropy). The exact-seed half of node 1.2.10 is the
Prelim/Seed.lean sampler applied to the conditional laws below at
assembly time (node 1.2.11). The bound itself, history_relative_entropy,
is stated (verbatim, at its frozen hash) in Prerounding/History.lean,
which imports this file.
The posterior tuple space: reveal datum, full reference words, core word.
Equations
- CommutingRepetition.TracialStrategy.PostTuple n X Y A B D = (CommutingRepetition.RevealDatum n D × (Fin n → X) × (Fin n → Y) × (↥D → A) × (↥D → B))
Instances For
The public-history core of a posterior tuple (the manuscript's
R = (i, T₀, Z), eq history-R): the reveal datum, the revealed
question values (kept on C_X resp. C_Y — the live values excluded,
since i ∉ C_X ∪ C_Y), and the core word.
Equations
- CommutingRepetition.TracialStrategy.histCore t = (t.1, CommutingRepetition.keepOn t.1.CX t.2.1, CommutingRepetition.keepOn t.1.CY t.2.2.1, t.2.2.2)
Instances For
The flattening of a posterior tuple to (history, live questions) (the tuple format of eqs J-A, J-B).
Equations
- CommutingRepetition.TracialStrategy.flattenPost t = (CommutingRepetition.TracialStrategy.histCore t, t.2.1 t.1.i, t.2.2.1 t.1.i)
Instances For
The flattened posterior law ℚ(R, x, y) — the pushforward of
posteriorQ under flattenPost (classical decidability of tuple
equality is harmless: the law is noncomputable anyway).
Equations
- S.flatQ R D μ w p u = CommutingRepetition.ClassicalInformation.groupedMass CommutingRepetition.TracialStrategy.flattenPost (S.posteriorQ R D μ w p) u
Instances For
The conditional history law ℚ(R = h ∣ i, X_i = x) (eq J-A's
conditional): supported on histories whose datum has the given live
coordinate; junk value 0 at a vanishing posterior marginal
("Zero posterior marginals use one fixed default distribution" — the
default is chosen at assembly (node 1.2.11); the relative-entropy
statements below are unaffected because zero-marginal cells carry zero
ℚ-mass).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conditional history law ℚ(R = h ∣ i, Y_i = y) (eq J-B's
conditional, mirror).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The locally generated Alice tuple law J_A(R, x, y) = m⁻¹ μ(x,y) ℚ(R ∣ i, X_i = x) (eq J-A), in its defaultless form (zero at
zero-marginal cells; the assembly's fixed default redistributes only
mass that carries no ℚ-weight).
Equations
Instances For
The locally generated Bob tuple law J_B (eq J-B, mirror).