oscOn
plain-language theorem explainer
oscOn supplies the essential oscillation of a real function w on a set s as the difference between its essential supremum and essential infimum under Lebesgue measure restricted to s. Analysts formalizing the local-to-global wedge step in the BRF route to the Riemann hypothesis cite it when converting uniform bounds on dyadic intervals into almost-everywhere phase bounds after rotation. The definition is a direct one-line abbreviation that subtracts essInf from essSup on the restricted measure.
Claim. For a function $w : ℝ → ℝ$ and a set $s ⊆ ℝ$, the essential oscillation is defined by $oscOn(w, s) := essSup(w|_s) - essInf(w|_s)$, where the essential supremum and infimum are taken with respect to Lebesgue measure restricted to $s$.
background
The LocalToGlobalWedge module formalizes the abstract local-to-global wedge step appearing as Lemma local-to-global-wedge in docs/primes/Riemann-proofs/Riemann-active.txt. In the manuscript, one bounds the essential oscillation of a boundary phase w(t) on a Whitney/dyadic schedule of intervals; after a unimodular rotation this yields an a.e. wedge bound |w(t)| ≤ π·Υ. The module implements a clean measure-theoretic core: define the oscillation on a set s as essSup minus essInf with respect to Lebesgue measure restricted to s.
proof idea
The definition is a one-line wrapper that subtracts essInf w (volume.restrict s) from essSup w (volume.restrict s).
why it matters
oscOn supplies the reusable interface for the local-to-global wedge. It is invoked by the core theorem exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion, which produces a constant c such that |w(t) - c| ≤ D a.e. when oscillations on all symmetric intervals [-(n+1), n+1] are bounded by D. It also feeds the oscillation bounds oscOn_Icc_whitney_le_div_c0_mul_L_of_poissonPlateau and related results in CertificateWindow for Poisson-plateau windows. In the Recognition Science framework this step supports the BRF route by turning analytic oscillation control into the global phase bound needed for the Poisson/Cayley step toward the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.