genuineZetaDerivedPhaseData_charge
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence or construction of any quantitative local factorization.
- Does not supply bounds on the size of regular-factor phase perturbations.
- Does not address global meromorphic properties outside the local disk.
- Does not compute numerical charges for concrete zeta zeros.
formal statement (Lean)
449private theorem genuineZetaDerivedPhaseData_charge
450 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
451 (genuineZetaDerivedPhaseData qlf n hn).charge = -qlf.order := by
proof body
Decided by rfl or decide.
452 rfl
453
454/-- Build a `RegularFactorPhase` from a `QuantitativeLocalFactorization`
455at a given level. This is the genuine Lipschitz-controlled phase of the
456regular factor on the `n`th circle. -/