zetaDerivedPhaseDataBundle
The definition constructs continuous phase data for the nth concentric circle around a meromorphic point, with radius scaled by one over n plus one and phase linear in the factorization order. Researchers modeling phase windings of the zeta function around its zeros in the Recognition Science framework cite it when assembling sampled annular increments. The proof is a direct record construction that assembles the center, scaled radius, linear phase map, and charge equality, then confirms continuity and winding number by algebraic simplification
claimFor a quantitative local factorization $Q$ with center $c$, radius $r_0$, and integer order $m$, and for each positive integer $n$, the construction yields a continuous phase assignment on the circle of radius $r_0/(n+1)$ centered at $c$, whose phase function is the linear map $θ ↦ m θ$ and whose winding charge equals $-m$.
background
The module bridges Mathlib meromorphic-order machinery to the Recognition Science annular-cost framework. A meromorphic function with order $m$ at a point $ρ$ factors locally as $(z-ρ)^m · g(z)$ where $g$ is holomorphic and nonvanishing at $ρ$. The power term contributes phase charge $-m$ while the regular factor contributes charge zero, so the composite carries charge $-m$. For the inverse zeta function this sign flip converts a zero of multiplicity $m$ into a defect sensor of charge $m$ that matches the required input for annular cost calculations. Quantitative local factorization augments the basic witness with a uniform bound $M$ on $|g'/g|$ over the disk together with the regime condition $M·r≤1$; this bound later controls the size of phase perturbations $ε_j$ on sampled circles.
proof idea
The definition is a direct record construction. It sets the center to the factorization center, the radius to the input radius divided by $n+1$ (using the positivity lemma for division), the phase map to order times the identity angle, and the charge to the negative order. Continuity of the phase follows from the product of a constant map with the identity map. The winding-number equation is discharged by casting the order to reals, rewriting subtraction as addition of a negative, and applying the ring tactic.
why it matters in Recognition Science
This definition supplies the concrete phase data that zetaDerivedPhaseData extracts and whose charge is recorded by the companion theorem zetaDerivedPhaseData_charge. Those two objects are then fed to zetaDerivedPhasePerturbationWitness, which supplies the zero-perturbation case for defect phase families. The construction therefore closes the local analytic input required for the Riemann-Hypothesis application inside the Recognition Science framework, ensuring that sampled increments on concentric circles around a zero reproduce the pure winding contribution demanded by the eight-tick octave and the Recognition Composition Law.
scope and limits
- Does not compute numerical values of the phase function at specific sample angles.
- Does not bound the size of perturbations arising from the regular factor $g$.
- Does not extend the phase data from a single circle to a full annular family.
- Does not address global meromorphic continuation or functional equations of the zeta function.
formal statement (Lean)
313private noncomputable def zetaDerivedPhaseDataBundle
314 (qlf : QuantitativeLocalFactorization) (n : ℕ) (_hn : 0 < n) :
315 { cpd : ContinuousPhaseData // cpd.charge = -qlf.order } := by
proof body
Definition body.
316 have hd : (0 : ℝ) < ↑n + 1 := by linarith
317 refine ⟨{
318 center := qlf.center
319 radius := qlf.radius / (↑n + 1)
320 radius_pos := div_pos qlf.radius_pos hd
321 phase := fun θ => (qlf.order : ℝ) * θ
322 phase_continuous := by
323 simpa using (continuous_const.mul continuous_id)
324 charge := -qlf.order
325 phase_winding := by
326 simp [sub_eq_add_neg, Int.cast_neg]
327 ring
328 }, rfl⟩
329