genuineZetaDerivedPhaseData
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
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not establish existence of a quantitative local factorization for the zeta function itself.
- Does not derive an explicit value for the log-derivative bound from zeta growth estimates.
- Does not compute numerical phase values at concrete zeros.
- Does not address global analytic continuation or functional equation properties.
formal statement (Lean)
420private noncomputable def genuineZetaDerivedPhaseData
421 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
422 ContinuousPhaseData :=
proof body
Definition body.
423 let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
424 let hd : (0 : ℝ) < ↑n + 1 := by linarith
425 let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
426 let hr : 0 < qlf.radius / (↑n + 1) := div_pos qlf.radius_pos hd
427 let hrw : qlf.radius / (↑n + 1) < qlf.radius :=
428 div_lt_self qlf.radius_pos hgt1
429 let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
430 (qlf.radius / (↑n + 1)) hr hrw qlf.logDerivBound qlf.logDerivBound_pos
431 { center := qlf.center
432 radius := qlf.radius / (↑n + 1)
433 radius_pos := hr
434 phase := fun θ => (qlf.order : ℝ) * θ + rfp.phase θ
435 phase_continuous := by
436 exact (continuous_const.mul continuous_id).add rfp.phase_continuous
437 charge := -qlf.order
438 phase_winding := by
439 simp only [add_sub_add_comm]
440 have hw_pole : (qlf.order : ℝ) * (2 * π) - (qlf.order : ℝ) * 0 =
441 -(2 * π * ((-qlf.order : ℤ) : ℝ)) := by
442 simp [Int.cast_neg]; ring
443 have hw_reg := rfp.toContinuousPhaseData.phase_winding
444 rw [rfp.charge_zero] at hw_reg
445 simp at hw_reg
446 rw [hw_pole, hw_reg, add_zero] }
447
448/-- The genuine phase data has the correct charge. -/