pureDefectPhaseData
This definition builds a constant-radius phase package for any defect sensor, assigning phase winding exactly equal to the sensor charge with no regular holomorphic factor. Researchers constructing trivial defect phase families or isolating pure winding increments in zeta meromorphic factorizations would cite it when separating the (z-ρ)^n contribution from the regular g(z) term. The implementation is a direct record construction that copies the sensor real part and charge, fixes radius 1, and sets the linear phase function -charge·θ.
claimGiven a defect sensor $s$ with real part $r$ and integer charge $m$, the map $n>0$ sends each such $n$ to the continuous phase data with center $r$, radius $1$, phase function $θ↦-mθ$, and winding charge $m$.
background
The Meromorphic Circle Order module bridges Mathlib meromorphic-order machinery to the RS annular-cost framework. A meromorphic function with order $n$ admits the local factorization $f(z)=(z-ρ)^n g(z)$ with $g$ holomorphic and $g(ρ)≠0$; the factor $(z-ρ)^n$ carries phase charge $-n$ while the regular factor carries charge $0$. Upstream, DefectSensor (from CostCoveringBridge) packages the real location and integer charge of a defect, while ContinuousPhaseData (from CirclePhaseLift) records center, radius, continuous phase function, and winding charge for use in annular cost calculations. The defect functional from LawOfExistence equals the J-cost, and the eight-tick phase supplies the underlying $2π$-periodic structure.
proof idea
The definition is a direct record literal. For each $n>0$ it returns a ContinuousPhaseData whose center is the sensor real part, radius is the constant 1 (positivity by norm_num), phase is the linear map $-charge·θ$ (continuity by the continuity tactic), charge is copied from the sensor, and phase_winding is discharged by simp followed by ring.
why it matters in Recognition Science
pureDefectPhaseData supplies the unperturbed phase data for trivialDefectPhaseFamily and the zero-perturbation witness trivialDefectPhasePerturbationWitness; it is also invoked inside genuineZetaDerivedPhasePerturbationWitness when the regular factor is present. It isolates the pure winding increment required by the perturbation lemmas that feed RingPerturbationControl, thereby supporting the separation $Δ_j = pure_winding_increment + ε_j$ in the meromorphic factorization of $ζ^{-1}$. In the RS framework this realizes the phase-charge matching between meromorphic order and the defect functional at the annular cost level.
scope and limits
- Does not incorporate any regular holomorphic factor $g(z)$.
- Does not compute or verify the meromorphic order of an underlying function.
- Does not produce bounds on the size of perturbation increments $ε_j$.
- Does not depend on refinement depth beyond the positivity hypothesis on $n$.
- Does not address summability or $log φ$ scaling of errors.
Lean usage
phaseAtLevel := pureDefectPhaseData sensorformal statement (Lean)
126noncomputable def pureDefectPhaseData (sensor : DefectSensor) :
127 (n : ℕ) → 0 < n → ContinuousPhaseData :=
proof body
Definition body.
128 fun n hn =>
129 { center := (sensor.realPart : ℂ)
130 radius := 1
131 radius_pos := by norm_num
132 phase := fun θ => (-(sensor.charge : ℤ) : ℝ) * θ
133 phase_continuous := by
134 continuity
135 charge := sensor.charge
136 phase_winding := by
137 simp [sub_eq_add_neg]
138 ring }
139
140/-- A defect phase family with the correct charge but no regular perturbation. -/