IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
The Wedge module defines the unimodular complex number e^{i w} for a real phase w and supplies basic lemmas on its real part. It supplies the phase representation needed in the BRF algebraic route to the Riemann hypothesis. Researchers working on boundary oscillation bounds for Schur functions cite it. The module consists of a core definition plus four supporting lemmas on nonnegativity and norm control of the phase.
claimFor real $w$, the unimodular complex number is $e^{i w}$. When $|w|≤π/2$ one has Re$(e^{i w})≥0$. For a measurable phase function $w(t)$ satisfying $|w(t)|≤π·Υ$ almost everywhere, the associated norm satisfies ‖e^{i w(t)}‖≤1 a.e.
background
The module belongs to the BRF (bounded-real-function) route to the Riemann hypothesis. Upstream BRFPlumbing formalizes the purely algebraic correspondence: a function H is Herglotz when 0≤Re H, and its Cayley transform Θ=(H−1)/(H+1) is Schur when ‖Θ‖≤1. The Wedge module supplies the concrete phase representation Θ=e^{i w} that converts the Schur condition into statements about the real-valued phase w on the circle.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The phase definition and its nonnegativity lemmas feed directly into the LocalToGlobalWedge module, which carries out the local-to-global wedge step of the manuscript. That step converts a Whitney/dyadic schedule of local phase bounds into the global a.e. wedge |w(t)|≤π·Υ after a unimodular rotation, exactly as stated in Lemma local-to-global-wedge of docs/primes/Riemann-proofs/Riemann-active.txt.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not treat analytic continuation of the zeta function.
- Does not establish the Herglotz property for any concrete function.
- Does not derive explicit constants beyond the phase definition itself.