lemmaroutine

Coordinate states with bounded inconsistency

Lemma·ht:states·§4.4 Coordinate states on the original levels

Statement (paper)

The fractional shifts can be fixed so that ∫m=EEme=O(1), \int m=\E_E m_e=O(1), with an absolute constant. At each nonarchimedean entry every edge is consistent outside finitely many threshold levels. If two vertices have matching AA-labels, then ∣zx−zx′∣v≤cve−s; |z_x-z_{x'}|_v\le c_v e^{-s}; matching B1B_1-labels similarly implies ∣wx−wx′∣v≤cves|w_x-w_{x'}|_v\le c_v e^s, where cv=1c_v=1 at nonarchimedean entries and cv=2c_v=\sqrt2 at archimedean entries. All the level functions can be chosen measurable.

In plain English

The fractional shifts can be chosen so that the total inconsistency mm has bounded average, ∫m=EEme=O(1)\int m=\E_E m_e=O(1) with an absolute constant. At nonarchimedean entries every edge is consistent except at finitely many threshold levels, matching AA-labels give ∣zx−zx′∣v≤cve−s|z_x-z_{x'}|_v\le c_v e^{-s}, matching B1B_1-labels give ∣wx−wx′∣v≤cves|w_x-w_{x'}|_v\le c_v e^{s} (with cv=1c_v=1 nonarchimedean, 2\sqrt2 archimedean), and all level functions are measurable.

Why it's here

This lemma sets up the coordinate states on the original levels and records the properties that later place-by-place arguments rely on: a bounded inconsistency budget, consistency away from finitely many thresholds, and coordinate closeness for matching labels. Results such as the place identity for opposite endpoints use these facts to control local contributions at each place vv, with measurability making the integrals meaningful.
Classified routine:
A construction-and-bookkeeping lemma: random fractional shifts of dyadic/ultrametric level partitions give bounded expected inconsistency by a standard random-shift averaging argument, and the label-closeness bounds follow directly from the box sizes at each place.

Uses

Nothing else in the paper

Used by

claimPlace identity and flanking positive-charge intervals

Sources

PaperOpen
Section
§4.4 Coordinate states on the original levels
Page
—
Label
ht:states
Line
sections/03-heights.tex:397
Leannot aligned

Phase 2 aligns this node to a Lean declaration.