zetaDerivedPhaseData_charge
plain-language theorem explainer
The declaration shows that for a quantitative local factorization of a meromorphic function and positive integer n, the charge component of the derived phase data at that level equals the negative of the factorization order. Number theorists applying Recognition Science to the Riemann hypothesis cite this result when building defect phase families from actual zeta zeros rather than trivial scaffolding. The proof reduces immediately to the defining property of the associated data bundle.
Claim. Let $Q$ be a quantitative local factorization of a meromorphic function and let $n$ be a positive natural number. The charge of the phase data derived from $Q$ at refinement level $n$ satisfies charge = -order($Q$).
background
In the Meromorphic Circle Order module, meromorphic functions admit local factorizations $f(z) = (z - ρ)^n g(z)$ with $g$ holomorphic and nonvanishing at $ρ$. The phase charge on a small circle around $ρ$ is then -n from the pole or zero factor, as established by charge_additive and related lemmas. QuantitativeLocalFactorization extends the basic witness with a uniform bound on the logarithmic derivative of the regular factor $g$, controlling phase perturbations on sampled circles. This setting connects Mathlib meromorphic order machinery to the Recognition Science annular cost framework, where phase charges match defect sensor charges for zeta reciprocals at zeros of multiplicity $m$.
proof idea
The proof is a one-line term that directly extracts the charge equality from the property of the bundled phase data constructed for the factorization and refinement level.
why it matters
This result supplies the charge equality needed to construct zetaDerivedPhaseFamily, which in turn feeds into canonical defect sampling for ring perturbation control. It realizes the module's goal of extracting genuine phase data from meromorphic factorizations, ensuring that for zeta reciprocal the charge equals the multiplicity $m$ matching the defect sensor. In the Recognition framework this closes the loop from meromorphic order to the phi-ladder defect phases used in the eight-tick octave analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.