pith. machine review for the scientific record. sign in
structure definition def or abbrev high

QuantitativeLocalFactorization

show as:
view Lean formalization →

QuantitativeLocalFactorization augments the local meromorphic witness with an explicit positive bound M on the logarithmic derivative of the regular factor together with the regime condition M times radius at most 1. Researchers applying annular cost comparisons to hypothetical zeros of zeta cite this structure to obtain uniform control on phase perturbations epsilon_j at sampled points. The declaration is a direct structure extension of LocalMeromorphicWitness by three fields that enforce the bound, its positivity, and the small-perturbation r

claimA quantitative local factorization consists of a center $c$, integer order $n$, positive radius $r$, and regular factor $g$ that is analytic and non-vanishing on the closed disk of radius $r$ about $c$, together with a positive real $M$ such that $M r ≤ 1$.

background

LocalMeromorphicWitness supplies the base data: a center in the complex plane, an integer order, a positive radius, and a regular factor that is analytic at the center, differentiable on the closed disk, and nowhere zero inside that disk. The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the Recognition Science annular-cost framework by factoring a meromorphic function locally as $(z - ρ)^n g(z)$ with $g$ holomorphic and non-vanishing, so that the phase charge of the pole part is exactly the order while the regular factor contributes zero charge. Upstream results on eight-tick phases and phi-forcing supply the discrete angular sampling and J-cost scale in which the perturbation bound M is later applied.

proof idea

The declaration is a structure definition that extends LocalMeromorphicWitness by adjoining the three fields logDerivBound, logDerivBound_pos and perturbation_regime; no tactics or lemmas are invoked.

why it matters in Recognition Science

It is the analytic input required by mkSharedCirclePair and the subsequent carrier_defect_comparison_rh theorem, which shows that any nonzero-charge defect on shared circles exceeds every carrier budget for large refinement depth. The structure therefore closes the local-to-global step that converts a meromorphic-order hypothesis into a concrete annular-cost divergence, directly supporting the Recognition Science route to the Riemann hypothesis via phase-charge and phi-ladder cost bounds. It touches the open question of whether the Euler-product carrier bound can be made uniform enough to rule out all off-critical-line zeros.

scope and limits

Lean usage

noncomputable def example (ρ : ℂ) (hρ_ne : ρ ≠ 1) (m : ℤ) (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m) (hσ : 1/2 < ρ.re) : QuantitativeLocalFactorization := eulerQuantitativeFactorization ρ hρ_ne m hord hσ

formal statement (Lean)

 269structure QuantitativeLocalFactorization extends LocalMeromorphicWitness where
 270  logDerivBound : ℝ
 271  logDerivBound_pos : 0 < logDerivBound
 272  perturbation_regime : logDerivBound * radius ≤ 1
 273
 274/-- On a circle of radius `r` centered at `w.center`, adjacent sample
 275points at angular spacing `2π/(8n)` are separated by arc length
 276`2πr/(8n)`. If the regular factor has log-derivative bounded by `M`,
 277then each phase perturbation satisfies `|ε_j| ≤ M · 2πr/(8n)`. -/

used by (31)

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

… and 1 more

depends on (12)

Lean names referenced from this declaration's body.