turns
plain-language theorem explainer
The lemma converts a uniform bound on essential oscillation of a measurable phase function w on the exhaustion intervals [-n,n] into the existence of a rotation constant c such that |w(t) - c| is bounded almost everywhere on the real line. Analysts working on the BRF route to the Riemann hypothesis cite it to obtain the global wedge condition required for the subsequent Poisson or Cayley transform. The argument is a direct exhaustion argument that extracts the limiting rotation from the sequence of essential suprema and infima on the nested dyz
Claim. Let $w : ℝ → ℝ$ be Lebesgue measurable. If there exists $D ≥ 0$ such that the essential oscillation of $w$ on $[-n,n]$ is at most $D$ for every natural number $n$, then there exists a constant $c ∈ ℝ$ satisfying $|w(t) - c| ≤ D$ for almost every $t ∈ ℝ$.
background
The module supplies the measure-theoretic core for the local-to-global wedge step in the BRF route to the Riemann hypothesis, exactly as stated in the manuscript lemma local-to-global-wedge. Essential oscillation on a set s is defined by oscOn w s = essSup(w restricted to s) - essInf(w restricted to s) with respect to Lebesgue measure. The local theoretical setting assumes a boundary phase w(t) whose oscillation is controlled on a Whitney or dyadic schedule of intervals; after a unimodular rotation the phase satisfies an a.e. wedge bound |w(t)| ≤ π·Υ needed for the Poisson/Cayley step.
proof idea
The proof applies the definitions of essential supremum and infimum on each compact interval [-n,n] to produce a sequence of candidate rotation constants. Compactness of the interval [0,D] yields a convergent subsequence whose limit c satisfies the a.e. bound on the union of the intervals, which exhausts ℝ. It is a one-line wrapper that invokes the exhaustion property of Lebesgue measure together with the definition of oscOn.
why it matters
This lemma supplies the reusable interface that turns local oscillation estimates into the global wedge bound required for the Poisson/Cayley step in the BRF route. It is invoked by direct_rh_from_honestPhaseChargeZeroBridge to establish the analytic RH core and by mellinReflect in the Mellin-transform package. In the Recognition Science framework it closes the local-to-global step that connects analytic phase control to the eight-tick octave and phi-forcing structures; it touches the open question of obtaining explicit numerical bounds on oscillation from the underlying J-cost or defectDist definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.