exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion
plain-language theorem explainer
If a real function w is essentially bounded above and below and its essential oscillation on every symmetric interval [-(n+1), n+1] stays at most D, then a constant c exists such that |w(t) - c| is at most D almost everywhere. Analysts working on the Riemann hypothesis via the boundary rotation function route cite this result to turn local oscillation controls into a global phase bound after rotation. The proof fixes the base interval [-1,1], takes the midpoint of its essential infimum and supremum as c, then extends the deviation bound to the
Claim. Let $w : {R} {to} {R}$ be essentially bounded above and below with respect to Lebesgue measure. Suppose that for every natural number $n$ the essential oscillation of $w$ on the interval $[-(n+1), n+1]$ is at most $D$. Then there exists a real number $c$ such that $|w(t) - c| {leq} D$ for almost every $t$ with respect to Lebesgue measure.
background
The module develops the local-to-global wedge step for the Riemann hypothesis under the BRF route. Essential oscillation of a boundary phase $w$ on a set $s$ is the difference between its essential supremum and essential infimum relative to Lebesgue measure restricted to $s$. Uniform bounds on this quantity over the nested exhaustion intervals $[-n,n]$ permit extraction of a rotation constant $c$ that yields an a.e. wedge bound on all of ${R}$. The local theoretical setting is the measure-theoretic core that converts analytic oscillation data into the phase control required for subsequent Poisson or Cayley arguments.
proof idea
The tactic proof first restricts to the base interval $I_0 = [-1,1]$ and verifies that the restricted measure is positive and that the almost-everywhere filter is nontrivial. It computes the essential infimum and supremum on this interval, selects their midpoint as the candidate $c$, and inherits the global upper and lower boundedness conditions via absolute continuity of the restricted measure. For each larger interval $I_n = [-(n+1),n+1]$ it establishes measure inclusion, transfers boundedness, and uses the given oscillation hypothesis together with monotonicity of essential bounds to obtain the deviation bound almost everywhere on $I_n$; the countable exhaustion then yields the global almost-everywhere statement.
why it matters
This theorem supplies the core local-to-global wedge lemma that feeds directly into the paper-friendly wrapper exists_shift_ae_abs_sub_le_of_forall_centered_oscOn. It implements the abstract local-to-global-wedge step recorded in the manuscript Riemann-active.txt, turning uniform essential-oscillation controls on dyadic intervals into an a.e. bound after unimodular rotation. Within the Recognition Science development it closes the analytic interface needed for the Riemann-hypothesis argument, though its precise link to the forcing chain or phi-ladder is left to surrounding number-theory files.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.