pith. machine review for the scientific record. sign in
theorem proved term proof

zetaDerivedPhaseData_charge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 335private theorem zetaDerivedPhaseData_charge
 336    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 337    (zetaDerivedPhaseData qlf n hn).charge = -qlf.order :=

proof body

Term-mode proof.

 338  (zetaDerivedPhaseDataBundle qlf n hn).property
 339
 340/-- A defect phase family derived from an actual `QuantitativeLocalFactorization`
 341of a meromorphic function near a pole/zero.
 342
 343Unlike `trivialDefectPhaseFamily` (which uses constant-phase scaffolding),
 344this construction extracts genuine phase data from `meromorphic_phase_charge`
 345on circles of decreasing radius `r₀/(n+1)` around the factorization center.
 346The charge on each circle equals `-order`, which for `zetaReciprocal` at a
 347zero of ζ with multiplicity `m` gives charge `m = sensor.charge`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.