zetaDerivedPhaseDataBundle
plain-language theorem explainer
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
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.