eulerQuantitativeFactorization_order
For a point ρ in the complex plane with real part strictly larger than one half and not equal to one, the order of the Euler quantitative factorization equals the meromorphic order m of the reciprocal zeta function whenever the latter is defined. Number theorists applying the Recognition Science carrier framework to the Riemann hypothesis cite this equality to confirm phase charges in defect families. The argument is a direct simplification that extracts the order from the local factorization witness.
claimLet ρ ∈ ℂ satisfy ρ ≠ 1 and 1/2 < Re(ρ). If the meromorphic order of ζ^{-1} at ρ equals the integer m, then the order of the Euler quantitative factorization of ζ^{-1} at ρ equals m.
background
This declaration belongs to the Euler Product Instantiation module, which shows that the Euler product for ζ(s) instantiates the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge. Core objects include the prime sum ∑_p p^{-σ}, the Hilbert-Schmidt norm squared ∑_p p^{-2σ}, and the determinant C(s) = det₂²(I − A(s)), which is holomorphic and nonvanishing for Re(s) > 1/2. The module establishes convergence of the logarithmic derivative and satisfaction of the EulerCarrier interface on that half-plane.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of eulerQuantitativeFactorization together with LocalMeromorphicWitness.shrinkRadius, then directly invokes the second component of the chosen specification from the zetaReciprocal_local_factorization lemma.
why it matters in Recognition Science
The result verifies that the concrete Euler carrier preserves the prescribed meromorphic order, feeding directly into the honest_argument_principle_phase_family theorem. It completes the instantiation chain that converts the Euler product into a cost-covering axiom, supporting a conditional Riemann hypothesis for Re(s) > 1/2. The equality aligns with the Recognition Science forcing chain by ensuring defect phase families carry the correct charge m.
scope and limits
- Does not address zeros on the critical line Re(s) = 1/2.
- Does not bound the possible values of the order m.
- Does not extend the equality to points with real part ≤ 1/2.
- Does not claim holomorphy or convergence outside the given half-plane.
formal statement (Lean)
678theorem eulerQuantitativeFactorization_order (ρ : ℂ)
679 (hρ_ne : ρ ≠ 1) (m : ℤ)
680 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
681 (hσ : 1/2 < ρ.re) :
682 (eulerQuantitativeFactorization ρ hρ_ne m hord hσ).order = m := by
proof body
Term-mode proof.
683 simpa [eulerQuantitativeFactorization, LocalMeromorphicWitness.shrinkRadius] using
684 (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose_spec.2
685
686/-! ### §6. Instantiation of the abstract carrier interfaces -/
687
688/-- **Main instantiation theorem:** The concrete Euler carrier
689 satisfies the abstract EulerCarrier interface from
690 CostCoveringBridge.lean. -/