genuineZetaDerivedPhaseData_charge
plain-language theorem explainer
The theorem confirms that genuine phase data built from a quantitative local factorization carries charge exactly equal to the negation of the factorization order. Researchers constructing defect phase families for meromorphic zeta applications in Recognition Science cite it to verify charge consistency with the defect sensor. The proof is immediate reflexivity from the data constructor definition.
Claim. Let $Q$ be a quantitative local factorization and let $n$ be a positive natural number. The charge of the genuine zeta-derived phase data at level $n$ equals the negative of the order of $Q$.
background
The Meromorphic Circle Order module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. A meromorphic function admits local factorization $f(z)=(z-ρ)^n g(z)$ with $g$ holomorphic and nonvanishing at $ρ$; the phase charge of the pole part is $-n$ while the regular factor contributes zero charge. The QuantitativeLocalFactorization structure extends the basic local witness by a uniform bound $M$ on $|g'/g|$ together with a perturbation regime condition ensuring controlled phase increments on sampled circles of radius $r$.
proof idea
The proof is a one-line reflexivity wrapper that matches the charge field of the genuine phase data constructor directly against the negated order supplied by the quantitative local factorization.
why it matters
This result feeds the genuineZetaDerivedPhaseFamily definition, which builds a defect phase family carrying non-trivial regular-factor perturbations unlike the synthetic zetaDerivedPhaseFamily. It closes the charge-matching requirement stated in the module documentation for ζ^{-1} at zeros of ζ, aligning with the Recognition Science phase-charge rules for meromorphic orders and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.