module module high

`IndisputableMonolith.NumberTheory.MeromorphicCircleOrder`

The module extracts a genuine local meromorphic factorization from Mathlib's meromorphicOrderAt_eq_int_iff, with the regular factor g taken as the actual analytic nonvanishing part from Weierstrass factorization rather than a dummy constant. Researchers building the analytic trace and defect-sampled trace for the Recognition Science RH bridge would cite it when constructing phase charges and perturbation witnesses. The module supplies definitions and small lemmas that connect continuous complex analysis to discrete annular J-cost sampling via a

claimThe module supplies LocalMeromorphicWitness and local_meromorphic_factorization such that a meromorphic function admits the local factorization $f(z)=z^k g(z)$ where $k$ is the integer order and $g$ is holomorphic and nonvanishing at the point, together with defectPhasePureIncrement and regular_perturbation bounds for phase-charge increments.

background

The module sits inside the NumberTheory layer of Recognition Science and imports Constants (fundamental time quantum τ₀=1 tick), AnnularCost (phiCost u := cosh((log φ)·u)−1 = J(φ^u)), CirclePhaseLift (continuous-phase infrastructure bridging Mathlib complex analysis to discrete AnnularRingSample/AnnularMesh cost framework), and CostCoveringBridge (three-layer RS cost-covering architecture for RH after the budget interface is made realizable). It therefore supplies the concrete factorization objects needed to turn a hypothetical zeta defect into a phase family whose annular excess can be sampled against the carrier budget.

proof idea

This is a definition module, no proofs. It defines LocalMeromorphicWitness, DefectPhaseFamily, pureDefectPhaseData, trivialDefectPhaseFamily, defectPhasePureIncrement, DefectPhasePerturbationWitness, and the three regular_perturbation lemmas by direct appeal to Mathlib's meromorphicOrderAt_eq_int_iff, extracting the genuine Weierstrass regular factor g rather than a constant placeholder.

why it matters in Recognition Science

The module feeds AnalyticTrace (now axiom-free), CarrierBudgetComparison (Phase 4a of the RH closure plan), DefectSampledTrace (realized annular meshes for hypothetical zeta defects), and HonestPhaseBudgetBridge (Euler/Hadamard-style quantitative control for phase families). It supplies the honest perturbation witness that converts a phase family into bounded annular excess data, closing the remaining bottleneck after Axiom 1 was eliminated.

scope and limits

Does not prove the Riemann Hypothesis.
Does not supply global factorization or entire-function properties.
Does not compute explicit orders or residues for the zeta function.
Does not replace the full cost-covering argument in CostCoveringBridge.

used by (4)

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

IndisputableMonolith.NumberTheory.AnalyticTrace module_import
IndisputableMonolith.NumberTheory.CarrierBudgetComparison module_import
IndisputableMonolith.NumberTheory.DefectSampledTrace module_import
IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.NumberTheory.AnnularCost module_import
IndisputableMonolith.NumberTheory.CirclePhaseLift module_import
IndisputableMonolith.NumberTheory.CostCoveringBridge module_import

declarations in this module (43)

structure LocalMeromorphicWitness L51
theorem local_meromorphic_factorization L85
theorem meromorphic_phase_charge L110
structure DefectPhaseFamily L118
def pureDefectPhaseData L126
def trivialDefectPhaseFamily L141
def defectPhasePureIncrement L152
structure DefectPhasePerturbationWitness L167
theorem regular_factor_increment_decomposition L187
theorem regular_perturbation_small L196
theorem regular_perturbation_linear_term_bounded L203
theorem regular_perturbation_quadratic_term_bounded L213
def trivialDefectPhasePerturbationWitness L223
theorem defect_phase_family_with_perturbation_exists L250
theorem defect_phase_family_exists L257
structure QuantitativeLocalFactorization L269
def phaseIncrementEpsilonBound L278
theorem phaseIncrementEpsilonBound_nonneg L283
theorem phaseIncrementEpsilonBound_decreasing L296
def zetaDerivedPhaseDataBundle L313
def zetaDerivedPhaseData L330
theorem zetaDerivedPhaseData_charge L335
def zetaDerivedPhaseFamily L348
theorem zetaDerivedPhaseFamily_sensor L360
def zetaDerivedPhasePerturbationWitness L367
def regularFactorPhaseFromWitness L402
def genuineZetaDerivedPhaseData L420
theorem genuineZetaDerivedPhaseData_charge L449
def qlf_regularFactorPhase L457
def genuineZetaDerivedPhaseFamily L471
def genuineRegularFactorPhaseAt L486
theorem genuineRegularFactorPhaseAt_logDerivBound L502
theorem epsilon_abs_bound L510
theorem epsilon_log_phi_small L519
theorem sum_epsilon_abs_bound L555
theorem sum_epsilon_sq_bound L588
theorem convexOn_sinh_Ici L638
theorem sinh_mul_le_mul_sinh L646
theorem genuine_pure_increment_abs_eq L656
theorem sum_inv_succ_mul_succ_le_one L680
theorem sum_inv_succ_mul_succ_sq_le_one L717
def genuineZetaDerivedPhasePerturbationWitness L735
structure ZetaPhaseFamilyData L965