lemmaroutineinferred_dep

Common height band of accurate wedges

Lemma·ext:band·§7.2 Point profiles and a common height band

Statement (paper)

There are a constant c>0c>0, independent of tt along the fixed sequence, a sequence δt→0\delta_t\to0, and scales J→∞J\to\infty such that a set of ordinary wedges of probability at least cR0log⁡(2R0)=t−o(1) \frac{c}{R_0\log(2R_0)}=t^{-o(1)} satisfies, uniformly on the set, J≤Hp∗+Hr∗≤2J,E1+E2≤δt(Hp∗+Hr∗). J\le H_p^*+H_r^*\le2J,\qquad E_1+E_2\le\delta_t(H_p^*+H_r^*). Every such wedge has p≠rp\ne r.

In plain English

Along the fixed sequence, there is a set of ordinary wedges of probability at least c/(R0log⁡(2R0))=t−o(1)c/(R_0\log(2R_0))=t^{-o(1)}, with c>0c>0 independent of tt, on which J≤Hp∗+Hr∗≤2JJ\le H_p^*+H_r^*\le 2J and E1+E2≤δt(Hp∗+Hr∗)E_1+E_2\le\delta_t(H_p^*+H_r^*) for some δt→0\delta_t\to0 and J→∞J\to\infty. Every such wedge has p≠rp\ne r.

Why it's here

This is a pigeonhole step. The positive rare mass from com-rare-positive and the tail cutoff at R0SR_0S from ext-tail confine Hp∗+Hr∗H_p^*+H_r^* to about log⁡R0\log R_0 dyadic scales, so one scale keeps a 1/(R0log⁡(2R0))1/(R_0\log(2R_0)) share, while the o(S)o(S) average errors E1,E2E_1,E_2 from ext-profiles are small relative to the height on most of it. On this band, point profiles are accurate stand-ins for wedge differences at one common height scale, which is what the organized pair graph needs.
Classified routine:
A dyadic pigeonhole argument combined with Markov's inequality. It applies the positive-mass lower bound (com-rare-positive), the tail cutoff (ext-tail) and the o(S) average errors (ext-profiles) to select one height scale carrying a 1/(R_0 log R_0) share of the mass.

Uses

propRare point exceptions have positive masslemTail of H star is negligiblelemPoint profiles approximate wedge differences

Used by

propOrganized pair graph with height-controlled ratios

Sources

PaperOpen
Section
§7.2 Point profiles and a common height band
Page
—
Label
ext:band
Line
sections/06-extraction.tex:262
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: Proof of ext:band (06-extraction.tex:278-308) sets Z=E_1+E_2 from Lemma ext:profiles and uses at line 306, but the DAG has no edge.