IndisputableMonolith.NumberTheory.CirclePhaseLift
CirclePhaseLift packages ContinuousPhaseData that assigns a continuous real phase function Θ to a nonvanishing function on a circle together with its integer winding charge. Researchers on the RH closure plan cite it when bounding carrier cost against defect topological floor on the same annulus. The module consists of structure definitions plus existence and Lipschitz lemmas that lift regular factors to continuous phases.
claimA continuous phase assignment for a nonvanishing function on the circle of radius $R$ centered at $c$ consists of a continuous map $Θ : ℝ → ℝ$ and integer charge $n$ satisfying $Θ(2π) − Θ(0) = −2π n$, where $Θ$ tracks the argument along the parametrization.
background
The module imports the Annular J-Cost Framework, whose core object is the φ-weighted cost phiCost u := cosh((log φ)·u) − 1 = J(φ^u). It introduces the ContinuousPhaseData structure that packages a continuous real-valued phase Θ for a nonvanishing function f along circleMap c R, with the integer charge recording the winding number. The local setting is the topological cost-covering bridge of Recognition Science, where phase windings enter the defect cost on annular regions.
proof idea
This is a definition module, no proofs. It defines the structures ContinuousPhaseData and RegularFactorPhase, then supplies lemmas establishing existence of a continuous phase lift for regular factors together with Lipschitz continuity of the resulting phase map.
why it matters in Recognition Science
The module supplies the phase machinery required by CarrierBudgetComparison, which formalizes Phase 4a of the RH closure plan by showing carrier sampled cost remains bounded while defect topological floor diverges for nonzero charge. It also supports MeromorphicCircleOrder in bridging meromorphic-order factorization to the annular cost framework. In the Recognition Science chain it provides the continuous phase assignment needed to compute winding integrals and charge additivity.
scope and limits
- Does not compute explicit phase functions for arbitrary meromorphic functions.
- Does not address global topology beyond a single circle.
- Does not incorporate the phi-ladder mass formula or Berry threshold.
- Does not extend the phase lift to functions with interior zeros.
used by (2)
depends on (1)
declarations in this module (13)
-
structure
ContinuousPhaseData -
structure
RegularFactorPhase -
theorem
regularFactor_continuousPhase_exists -
theorem
regularFactor_phase_lipschitz -
theorem
and -
def
mkRegularFactorPhase -
theorem
holomorphic_nonvanishing_zero_charge -
theorem
zpow_phase_charge -
theorem
charge_additive -
theorem
winding_integral_simple_pole -
theorem
holomorphic_circle_integral_zero -
theorem
logDeriv_circle_integral_zero -
theorem
zpow_charge_eq_winding_integral