module module high

`IndisputableMonolith.NumberTheory.MeromorphicCircleOrder`

The MeromorphicCircleOrder module extracts genuine local meromorphic factorizations from Mathlib's meromorphicOrderAt_eq_int_iff, with the regular factor g taken as the actual Weierstrass analytic nonvanishing part. Number theorists building the Recognition Science cost-covering bridge to the Riemann hypothesis cite these constructions for precise circle phase and defect sampling. The module assembles sibling definitions and witnesses rather than a single proof.

claimLocalMeromorphicWitness realizes $f(z)=(z-a)^n g(z)$ with $g$ holomorphic and $g(a)\neq 0$, extracted from meromorphicOrderAt_eq_int_iff; also defines DefectPhaseFamily, meromorphic_phase_charge, defectPhasePureIncrement, and regular perturbation bounds on linear and quadratic terms.

background

This module sits in the NumberTheory layer and imports Constants (where $\tau_0=1$ tick), AnnularCost (with $\mathrm{phiCost}(u)=\cosh((\log\phi)\cdot u)-1=J(\phi^u)$), CirclePhaseLift (continuous-phase infrastructure bridging Mathlib complex analysis to discrete AnnularRingSample cost frameworks), and CostCoveringBridge (the three-layer RS cost-covering architecture for RH). It supplies local meromorphic factorization primitives so that regular factors remain genuine analytic nonvanishing functions rather than dummy constants. Sibling objects include LocalMeromorphicWitness, DefectPhaseFamily, pureDefectPhaseData, and regular_factor_increment_decomposition.

proof idea

This is a definition module that constructs witnesses and decompositions such as local_meromorphic_factorization, defectPhasePureIncrement, regular_factor_increment_decomposition, and the three regular_perturbation bounds. It supplies the analytic primitives needed for downstream cost comparisons without a single overarching proof.

why it matters in Recognition Science

The module supplies the meromorphic factorization tools required by AnalyticTrace (which assembles the full RH bridge after axiom elimination), CarrierBudgetComparison (carrier-defect budget comparison on the same circles), DefectSampledTrace (annular meshes for hypothetical zeta defects), and HonestPhaseBudgetBridge (perturbation witnesses that turn honest phase families into bounded annular excess data). It fills the requirement for genuine regular factors stated in the module doc-comment.

scope and limits

Does not prove the Riemann hypothesis.
Does not handle global meromorphic properties of the zeta function.
Does not compute explicit numerical phase-charge values.
Does not replace upstream Mathlib analytic results.
Does not establish bounded annular excess without additional witnesses.

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