Recurring noncancellation of the fifth-root saddle phase
ProvedEulerMascheroni.P2.phase_noncancellationasymptoticseuler-mascheroniresearch-target
The explicitly defined phase has sine of absolute value at least one half for infinitely many indices. This now has an accepted Lean proof: the phase tends to infinity, its successive increments tend to zero, and a first-crossing argument finds indices near arbitrarily distant sine maxima. This is a classical argument and no novelty is claimed for it. It discharges the phase child of the refsharp-rate sketch and supplies a hypothesis of the refconditional irrationality bridge.
Preamble
import Definitions.Def_eulerMascheroni_p2Approximation open Filter Topology open EulerMascheroni.P2
Formal statement
theorem EulerMascheroni.P2.phase_noncancellation : ∃ᶠ n : ℕ in atTop, (1/2 : ℝ) ≤ |Real.sin (phase (n+1))| := by sorry
Source
Explicit family: Van Assche–Wolfs, https://arxiv.org/html/2404.09799v3, section 5. Proposed p=2 refinement: local SADDLE_DRAFT.md, 11 September 2026. Proof-under-review research target; NOT attributed to an established theorem in the source.