genuineZetaDerivedPhaseData
plain-language theorem explainer
genuineZetaDerivedPhaseData constructs continuous phase data for a quantitative local factorization by scaling the disk radius to radius/(n+1) and superposing the pole winding order·θ with the regular-factor phase lift obtained from the covering-space construction. Researchers assembling defect phase families for the Riemann hypothesis in Recognition Science cite this when they need non-synthetic perturbations controlled by the log-derivative bound. The definition invokes regularFactorPhaseFromWitness on the scaled radius then assembles the six
Claim. Given a quantitative local factorization $qlf$ of a meromorphic function and integer $n>0$, the genuine phase data is the continuous phase datum with center $qlf.center$, radius $qlf.radius/(n+1)$, phase function $θ ↦ (qlf.order)·θ + φ_{reg}(θ)$, charge $-qlf.order$, and winding number obtained by adding the pole contribution to the zero-charge regular lift.
background
The Meromorphic Circle Order module translates Mathlib meromorphic-order factorizations into the Recognition Science annular-cost setting. A meromorphic function with order $n$ at $ρ$ factors locally as $(z-ρ)^n g(z)$ where $g$ is holomorphic and non-vanishing at $ρ$; the pole factor carries charge $-n$ while the regular factor carries charge 0, so the total charge is $-n$ by charge_additive. QuantitativeLocalFactorization extends the basic local witness by a uniform bound $M$ on $|g'/g|$ together with the regime condition $M·radius ≤ 1$; this bound directly limits the phase perturbation size on circles of radius $r$ by $|ε_j| ≤ M·2πr/(8n)$ at the eight-tick angular spacing.
proof idea
The definition first obtains the scaled radius $r' = radius/(n+1)$ and the strict inequalities $1 < n+1$ and $0 < r'$ by linarith and div_pos. It calls regularFactorPhaseFromWitness on the scaled radius using the supplied logDerivBound to produce the regular phase record rfp. The ContinuousPhaseData structure is then built with center and scaled radius copied from $qlf$, phase function order·θ + rfp.phase θ, charge $-order$, and phase_winding proved by rewriting the pole winding via Int.cast_neg and ring, then adding the zero-charge regular winding.
why it matters
This definition supplies the phase data consumed by genuineZetaDerivedPhaseFamily and genuineZetaDerivedPhasePerturbationWitness, which in turn support canonicalDefectSampledFamily_ringPerturbationControl. It replaces the synthetic linear phase of zetaDerivedPhaseDataBundle with the genuine Lipschitz-controlled lift, ensuring the perturbation terms remain summable in the log φ scale. Within the Recognition Science framework the construction realizes the local meromorphic-order input required for annular-cost analysis around zeros of ζ^{-1}, consistent with the eight-tick octave and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.