claimroutineinferred_dep

Place identity and flanking positive-charge intervals

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

Statement (paper)

Fix a base and two distinct opposite endpoints with incident jumps d≠d′d\ne d'. At a place vv, with b=min⁡(ne(v),ne′(v))b=\min(n_e(v),n_{e'}(v)), b′=max⁡(ne(v),ne′(v))b'=\max(n_e(v),n_{e'}(v)), u=−log⁡∣d−d′∣vu=-\log|d-d'|_v and α=u−b\alpha=u-b, one has −log⁡∣(d−d′)(1/d−1/d′)∣v=2α−(b′−b)-\log|(d-d')(1/d-1/d')|_v=2\alpha-(b'-b), and the integrated bit-difference charge at vv equals b′−bb'-b. Moreover, with cv=log⁡2c_v=\log 2 at archimedean entries and cv=0c_v=0 otherwise, Tv:=α+cv≥0T_v:=\alpha+c_v\ge0, and all positive charges at vv lie in I−=[b−Tv,b]I_-=[b-T_v,b] and I+=[b′,b′+Tv]I_+=[b',b'+T_v], even when these intervals are not contained in the chosen level interval.

In plain English

For a base with two distinct opposite endpoints with jumps d≠d′d\ne d', at each place vv one has −log⁡∣(d−d′)(1/d−1/d′)∣v=2α−(b′−b)-\log|(d-d')(1/d-1/d')|_v=2\alpha-(b'-b), where b,b′b,b' are the smaller and larger of ne(v),ne′(v)n_e(v),n_{e'}(v) and α=−log⁡∣d−d′∣v−b\alpha=-\log|d-d'|_v-b. The integrated bit-difference charge at vv equals b′−bb'-b, the quantity Tv=α+cvT_v=\alpha+c_v is nonnegative, and all positive charges at vv lie in I−=[b−Tv,b]I_-=[b-T_v,b] and I+=[b′,b′+Tv]I_+=[b',b'+T_v], even if these are not inside the chosen level interval.

Why it's here

This is the local bookkeeping step at a single place: it rewrites the pair's log-size as 2α2\alpha minus the bit-difference charge and confines positive charges to two explicit intervals of length TvT_v on either side of [b,b′][b,b']. The later claims use this localization to show rare positives sit on one side and to carry out the central-window and product-formula cancellation. It relies on the coordinate closeness bounds with constants cvc_v from the coordinate-state lemma, which is where the archimedean correction log⁡2\log 2 enters in Tv≥0T_v\ge0.
Classified routine:
Local valuation bookkeeping at a single place: the identity follows from 1/d−1/d′=(d′−d)/(dd′)1/d-1/d'=(d'-d)/(dd') together with the coordinate closeness bounds from the ht-states lemma, which supply the log⁡2\log 2 archimedean constant. It is a direct calculation rather than a new idea.

Uses

lemCoordinate states with bounded inconsistency

Used by

claimRare positives lie on one side onlyclaimCentral-window excess and product-formula cancellation

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:301
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Place identity; positive charges in flanking intervals" rests on ht:states