re_phase_nonneg_of_abs_le_pi_div_two
plain-language theorem explainer
If a real number w satisfies |w| ≤ π/2 then the real part of its phase is nonnegative. Analysts working on boundary conditions for the Riemann hypothesis would cite this algebraic fact. The short tactic proof converts the absolute bound into interval membership and applies the standard nonnegativity of cosine on [-π/2, π/2].
Claim. If $w ∈ ℝ$ satisfies $|w| ≤ π/2$, then $0 ≤ Re(exp(i w))$.
background
The module records the boundary wedge condition from the BRF route to the Riemann hypothesis: after unimodular rotation the phase w(t) obeys |w(t)| ≤ π Υ with Υ < 1/2 almost everywhere. This supplies the immediate positivity consequence needed for Poisson transport and the Cayley transform. The phase function is the complex exponential whose real part equals the cosine; upstream eight-tick phase definitions and J-cost structures supply the discrete-to-continuous setting.
proof idea
The tactic proof first rewrites the absolute-value hypothesis as membership of w in the closed interval [-π/2, π/2] via abs_le. It then rewrites the real part of the phase as the cosine and invokes the standard lemma Real.cos_nonneg_of_mem_Icc on that interval.
why it matters
This supplies the entry-point positivity for the boundary condition (P+) in the BRF Riemann route. It is invoked by the almost-everywhere extension ae_re_phase_nonneg_of_ae_abs_le_pi_mul that relaxes the bound to Υ ≤ 1/2. In the framework the result connects the wedge condition to spectral emergence and ledger factorization, which in turn rest on the eight-tick octave and the three-dimensional forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.