IndisputableMonolith.NumberTheory.RiemannHypothesis.LocalToGlobalWedge
The module defines essential oscillation oscOn w s as the difference between essential supremum and infimum of w restricted to s under Lebesgue measure. It supplies the oscillation control step that converts local bounds into global wedge confinement for the boundary phase in the BRF route to the Riemann Hypothesis. The module imports the Wedge file that encodes the |w(t)| ≤ π Υ condition with Υ < 1/2 almost everywhere and is imported by WindowToOscillation to close the local-to-global bridge. This is a definition module containing no proofs.
claim$oscOn(w,s) = essSup(w|_s) - essInf(w|_s)$ with respect to Lebesgue measure on the set $s$.
background
The parent Wedge module records the load-bearing boundary condition (P+) of the BRF route: after a unimodular rotation the boundary phase satisfies |w(t)| ≤ π·Υ with Υ < 1/2 almost everywhere. The present module isolates the algebraic consequence of that wedge by introducing the essential oscillation of w on a measurable set s. oscOn is defined directly from the essential supremum and infimum operators with respect to Lebesgue measure, providing the precise quantitative measure of how much w can vary inside any interval or window.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the oscillation control that WindowToOscillation uses to convert a window bound on the positive distribution -w' into a bound on Δ_I(w). It therefore occupies the immediate predecessor slot to the local-to-global-wedge lemma stated in docs/primes/Riemann-proofs/Riemann-active.txt and advances the boundary-wedge → positivity half of the BRF argument toward the Riemann Hypothesis.
scope and limits
- Does not prove the Riemann Hypothesis.
- Does not derive the wedge bound |w(t)| ≤ π·Υ from first principles.
- Does not quantify the constant Υ beyond the hypothesis Υ < 1/2.
- Does not address non-Lebesgue measures or non-boundary functions.