det2_log_summable
Absolute convergence of the summed logarithms of the per-prime factors holds for σ > 1/2. Analysts studying the holomorphic properties of the regularized determinant det₂(I − A(σ)) cite this result to justify interchanging sums and products in the Euler product. The argument reduces the absolute sum to a constant multiple of the Hilbert-Schmidt series via an explicit per-prime bound and comparison of geometric denominators.
claimFor real σ > 1/2 the series ∑_{p prime} |log(1 − p^{-σ}) + p^{-σ}| converges.
background
The EulerInstantiation module instantiates the abstract RS carrier from AnnularCost and CostCoveringBridge by realizing the Euler product of ζ(s) as a concrete Hilbert–Schmidt operator A(s) whose regularized determinant supplies the carrier C(s). The per-prime log-factor is given by det2LogFactor(p, σ) := log(1 − p^{-σ}) + p^{-σ}, whose absolute value satisfies the bound |det2LogFactor p σ| ≤ p^{-2σ}/(1 − p^{-σ}) from the upstream theorem det2_log_factor_bound. The comparison series ∑ p^{-2σ} is known to converge for σ > 1/2 by the upstream result hilbert_schmidt_convergent, which states that the squared Hilbert–Schmidt norm of A(s) remains finite in this half-plane.
proof idea
The proof constructs the explicit constant C := 1/(1 − 2^{-σ}) and verifies 0 ≤ C together with positivity of the denominator via linarith. It applies hilbert_schmidt_convergent to obtain summability of the scaled series C ⋅ p^{-2σ}. For each prime the bound from det2_log_factor_bound is invoked; the remaining inequality p^{-2σ}/(1 − p^{-σ}) ≤ C ⋅ p^{-2σ} is established by showing that the reciprocal of the denominator for p is at most C, using rpow monotonicity to compare 2^σ and p^σ and then applying one_div_le_one_div_of_le.
why it matters in Recognition Science
This result supplies the absolute summability needed for det2_product_convergent to conclude that the infinite product ∏_p det₂_factor(p, σ) converges, which in turn guarantees that the carrierValue σ is well-defined, positive, and nonvanishing for σ > 1/2 as recorded in carrier_pos. It completes the concrete step in the module’s instantiation chain from primes through the Hilbert–Schmidt operator to a holomorphic nonvanishing C(s) on Re(s) > 1/2, thereby enabling the EulerCarrier interface and the subsequent application of the cost-covering axiom toward conditional RH. Within the Recognition Science framework the convergence supplies the analytic control required for the regularized determinant to function as the carrier in the Euler product instantiation.
scope and limits
- Does not establish convergence for real parts σ ≤ 1/2.
- Does not extend the result to complex values of σ.
- Does not prove absolute convergence of the infinite product itself.
- Does not supply explicit rates or remainder estimates.
formal statement (Lean)
134theorem det2_log_summable {σ : ℝ} (hσ : 1/2 < σ) :
135 Summable (fun (p : Nat.Primes) => |det2LogFactor p σ|) := by
proof body
Tactic-mode proof.
136 let C : ℝ := 1 / (1 - (2 : ℝ) ^ (-σ))
137 have hσ_pos : 0 < σ := by linarith
138 have htwo_term_lt : (2 : ℝ) ^ (-σ) < 1 := by
139 exact Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
140 have hC_nonneg : 0 ≤ C := by
141 unfold C
142 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ) := by linarith
143 exact div_nonneg zero_le_one hden_pos.le
144 have hsumC : Summable (fun p : Nat.Primes => C * (p : ℝ) ^ (-2 * σ)) := by
145 exact (hilbert_schmidt_convergent hσ).mul_left C
146 refine hsumC.of_nonneg_of_le (fun p => abs_nonneg _) ?_
147 intro p
148 have hbound := det2_log_factor_bound hσ p
149 have hp_two : (2 : ℝ) ≤ p := by
150 exact_mod_cast p.prop.two_le
151 have hpow_ge : (2 : ℝ) ^ σ ≤ (p : ℝ) ^ σ := by
152 exact Real.rpow_le_rpow (by norm_num) hp_two (le_of_lt hσ_pos)
153 have hpow_ge_pos : 0 < (2 : ℝ) ^ σ := Real.rpow_pos_of_pos (by norm_num) _
154 have hx_le : (p : ℝ) ^ (-σ) ≤ (2 : ℝ) ^ (-σ) := by
155 rw [Real.rpow_neg (by positivity), Real.rpow_neg (by positivity)]
156 simpa [one_div] using one_div_le_one_div_of_le hpow_ge_pos hpow_ge
157 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ) := by linarith
158 have hden_le : 1 - (2 : ℝ) ^ (-σ) ≤ 1 - (p : ℝ) ^ (-σ) := by linarith
159 have hfrac_le :
160 (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ)) ≤
161 C * (p : ℝ) ^ (-2 * σ) := by
162 have hrecip :
163 (1 - (p : ℝ) ^ (-σ))⁻¹ ≤ C := by
164 unfold C
165 simpa [one_div] using one_div_le_one_div_of_le hden_pos hden_le
166 calc
167 (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ))
168 = (p : ℝ) ^ (-2 * σ) * (1 - (p : ℝ) ^ (-σ))⁻¹ := by rw [div_eq_mul_inv]
169 _ ≤ (p : ℝ) ^ (-2 * σ) * C := by
170 gcongr
171 _ = C * (p : ℝ) ^ (-2 * σ) := by ring
172 exact hbound.trans hfrac_le
173
174/-- The product ∏_p det₂_factor(p,σ) converges for σ > 1/2. -/