IndisputableMonolith.NumberTheory.CirclePhaseLift
CirclePhaseLift defines continuous phase data for nonvanishing functions on circles, packaging a real argument function Θ with integer winding charge. It is cited in carrier-defect budget comparisons and meromorphic order analyses to handle topological charges in annular regions. The module supplies type definitions and basic lemmas on phase existence, continuity, and additivity that build directly on the annular J-cost machinery.
claimContinuous phase data consists of a continuous function $Θ : ℝ → ℝ$ and integer charge $n ∈ ℤ$ satisfying $Θ(2π) − Θ(0) = −2π n$, representing the argument of a nonvanishing function along a circle.
background
This module sits in the NumberTheory domain and extends the annular J-cost framework imported from AnnularCost, where phiCost u := cosh((log φ)·u) − 1 = J(φ^u). It introduces ContinuousPhaseData to package the continuous argument lift Θ for functions on circleMap c R, with the integer charge recording the winding number. Key sibling definitions include RegularFactorPhase together with lemmas guaranteeing continuous phase existence and Lipschitz continuity.
proof idea
This is a definition module, no proofs. It structures phase data via inductive type definitions and supplies existence lemmas for regular factor phases along with continuity, additivity, and integral properties of the phase function.
why it matters in Recognition Science
The module supplies phase-lifting primitives that feed the carrier-defect budget comparison strategy in CarrierBudgetComparison, enabling contradiction arguments for nonzero charge around hypothetical zeros. It also supports MeromorphicCircleOrder by providing the continuous phase machinery needed for local factorizations of meromorphic functions. This advances the RH closure plan by bridging continuous phases to the J-cost framework.
scope and limits
- Does not handle vanishing functions or poles directly.
- Does not compute explicit phases for concrete meromorphic functions.
- Limits phase assignments to continuous lifts on individual circles.
- Does not address global topology beyond local circle maps.
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