claimroutineinferred_dep

Central-window excess and product-formula cancellation

Claim·§5.2 Three fixed pair experiments·inside propUpper score budget for pair experiments

Statement (paper)

Suppose only common positives remain, and let Jv={s:(v,s)∈C, ∣ρ(v,s)−1/2∣≤δ}J_v=\{s:(v,s)\in\mathcal C,\ |\rho(v,s)-1/2|\le\delta\}, which is an interval. Then the positive charge over the full intervals in , with coefficient 1−λ1-\lambda extended across both and increased by 2λ2\lambda on JvJ_v, exceeds 2Tv2T_v by at most λ∣Jv∣ 1{ne(v),ne′(v)∈int⁡Jv}\lambda|J_v|\,\mathbf1_{\{n_e(v),n_{e'}(v)\in\operatorname{int}J_v\}}; this bound is also valid in the rare-positive case. Combining it with the negative charge and and summing over places, the logarithm cancels by the product formula for the fixed nonzero element (d−d′)(1/d−1/d′)(d-d')(1/d-1/d'), with additive allowance 2∑v∗cv=2log⁡22\sum_v^*c_v=2\log 2, and places of zero level width may be included in the sum.

In plain English

Once only common positives remain, at each place vv the positive charge, with coefficient 1−λ1-\lambda across the full intervals and raised by 2λ2\lambda on the central window JvJ_v, exceeds 2Tv2T_v by at most λ∣Jv∣\lambda|J_v|, and only when both ne(v)n_e(v) and ne′(v)n_{e'}(v) lie in the interior of JvJ_v. Combining this with the negative charge and the place identity and summing over places, the logarithm cancels by the product formula, leaving an additive allowance of 2log⁡22\log 2.

Why it's here

The interval-overlap lemma caps the gain from the central window at λ∣Jv∣\lambda|J_v|, charged only when both endpoints lie inside JvJ_v. Since all positive charge sits in I±I_\pm with total at most 2Tv2T_v (the one-sided claim for rare positives), the local place identity then sums over places. The product formula for (d−d′)(1/d−1/d′)(d-d')(1/d-1/d') kills the logarithmic term, so only the 2∑v∗cv=2log⁡22\sum_v^* c_v=2\log 2 constant and the window terms remain for the final averaging step.
Classified routine:
A direct combination of the earlier interval-overlap lemma (bud-intervals), the place identity (claim-bud-upper-1) and the rare-positive claim, summed over places. The logarithmic term then cancels by the standard product formula for number fields.

Uses

lemInterval overlap envelope and interior mass boundclaimPlace identity and flanking positive-charge intervalsclaimRare positives lie on one side onlylemWeighted product formula for number fields

Used by

claimAveraging bounds distinct-pair budget by 10δ²λC_i

Figures

A horizontal axis labeled $s$ carries tick marks at $b-T$, $b$, $b'$, $b'+T$. Above the axis, two light-blue shaded bands with dark blue lines mark the flanking intervals $I_-=[b-T,b]$ and $I_+=[b',b'+T]$, separated by a gray band labeled "different bits" over $[b,b']$. Below the axis, an orange bracketed segment labeled "central window $J$" starts inside $I_-$ and ends inside $I_+$, with dotted vertical lines showing that $b$ and $b'$ both lie in its interior. It illustrates that a window whose overlap with the two flanks exceeds $T$ must contain both thresholds strictly inside.
Figure 1schematicp. 26
The intervals I−=[b−T,b]I_-=[b-T,b] and I+=[b′,b′+T]I_+=[b',b'+T], with b≤b′b\le b' and T≥0T\ge0, flank the bit-difference interval. The central window JJ in creates excess only if its total overlap with the two flanks exceeds TT; then both thresholds lie strictly inside JJ.
What it shows
A horizontal axis labeled ss carries tick marks at b−Tb-T, bb, b′b', b′+Tb'+T. Above the axis, two light-blue shaded bands with dark blue lines mark the flanking intervals I−=[b−T,b]I_-=[b-T,b] and I+=[b′,b′+T]I_+=[b',b'+T], separated by a gray band labeled "different bits" over [b,b′][b,b']. Below the axis, an orange bracketed segment labeled "central window JJ" starts inside I−I_- and ends inside I+I_+, with dotted vertical lines showing that bb and b′b' both lie in its interior. It illustrates that a window whose overlap with the two flanks exceeds TT must contain both thresholds strictly inside.
Read from the image by claude-opus-5.5 · confidence 85%
SupportslemInterval overlap envelope and interior mass boundclaimPlace identity and flanking positive-charge intervalsclaimCentral-window excess and product-formula cancellation

Sources

PaperOpen
Section
§5.2 Three fixed pair experiments
Page
—
Label
—
Line
sections/04-budgets.tex:345
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Central-window excess and product-formula cancellation" rests on claim-bud-upper-1
  • info
    inferred_dep
    outline: "Central-window excess and product-formula cancellation" rests on claim-bud-upper-2
  • info
    inferred_dep
    outline: "Central-window excess and product-formula cancellation" rests on ht:product