Suzuki's upper-source pairing and the amplitude normalization

This module records the source-faithful front half of the normalization A = 2 exp γ at κ = 1, β = 2.

Suzuki (10.2), (10.5) extends P = F⁺ + F⁻ = 2 + T⁺ - T⁻ by s P(s) = A on 1 < s < 2. For the standard adjoint p = r_{1,-1}, Section 10 gives p'(s) = -p(s+1)/s. Consequently the Iwaniec pairing at the source threshold is exactly A p(1). Proposition 11.8(iii) makes this pairing 2; the independent standard-adjoint boundary evaluation p(1)=exp(-γ) then gives A=2 exp γ.

The production tree does not yet construct r_{1,-1} or prove its boundary evaluation. Accordingly, this file does not assert the final equality. It constructs the genuine upper source P, its Section-10 pairing, proves the threshold identity from the actual adjoint equation, and exposes the exact final bridge. No Section-13 hat layer occurs here.

noncomputable def MathlibNt.SieveTheory.suzukiUpperSourceP (s : ℝ) : ℝ

Suzuki's genuine upper source P. Below the source threshold this is the Section-10 initial-history extension; strictly above it this is literally F⁺ + F⁻ = 2 + T⁺ - T⁻ from the production parity source series. The value at one switching point is assigned by the initial-history convention, which does not affect any interval integral.

Equations

• MathlibNt.SieveTheory.suzukiUpperSourceP s = if s ≤ 2 then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s else MathlibNt.SieveTheory.suzukiContinuousUpperFactor s + MathlibNt.SieveTheory.suzukiContinuousLowerFactor s

noncomputable def MathlibNt.SieveTheory.suzukiUpperSourcePairing (p : ℝ → ℝ) (s : ℝ) : ℝ

The Section-10 Iwaniec pairing for the upper equation at κ=1. The plus sign is -b in (10.9), because the upper source has DDE parameter b=-1.

Equations

• MathlibNt.SieveTheory.suzukiUpperSourcePairing p s = s * p s * MathlibNt.SieveTheory.suzukiUpperSourceP s + ∫ (t : ℝ) in s - 1..s, p (t + 1) * MathlibNt.SieveTheory.suzukiUpperSourceP t

@[simp]

theorem MathlibNt.SieveTheory.suzukiUpperSourceP_of_le_two {s : ℝ} (hs : s ≤ 2) : suzukiUpperSourceP s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s

theorem MathlibNt.SieveTheory.suzukiUpperSourceP_of_two_lt {s : ℝ} (hs : 2 < s) : suzukiUpperSourceP s = 2 + suzukiProposition118SourceTPlus s - suzukiContinuousLowerTail s

theorem MathlibNt.SieveTheory.mul_suzukiUpperSourceP_eq_amplitude {s : ℝ} (hs₀ : s ≠ 0) (hs₂ : s ≤ 2) : s * suzukiUpperSourceP s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude

The actual upper source has the exact Section-10 initial history s P(s)=A (including the harmless chosen switching-point value).

theorem MathlibNt.SieveTheory.integral_upperAdjoint_shift_div_eq_sub {p : ℝ → ℝ} (hp : ∀ t ∈ Set.uIcc 1 2, HasDerivAt p (-p (t + 1) / t) t) (hint : IntervalIntegrable (fun (t : ℝ) => p (t + 1) / t) MeasureTheory.volume 1 2) : ∫ (t : ℝ) in 1..2, p (t + 1) / t = p 1 - p 2

Integrating the standard upper-adjoint equation on [1,2] gives the exact boundary coefficient used in Suzuki's Proposition 11.8 formula.

theorem MathlibNt.SieveTheory.suzukiUpperSourcePairing_two_eq_amplitude_mul_adjoint_one {p : ℝ → ℝ} (hp : ∀ t ∈ Set.uIcc 1 2, HasDerivAt p (-p (t + 1) / t) t) (hint : IntervalIntegrable (fun (t : ℝ) => p (t + 1) / t) MeasureTheory.volume 1 2) : suzukiUpperSourcePairing p 2 = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude * p 1

Source-faithful threshold evaluation: the genuine upper-source pairing is A p(1). This is the finite Section-10 pairing calculation, not a definition of A and not an assumed normalization.

theorem MathlibNt.SieveTheory.suzukiLowerSieveAmplitude_eq_two_mul_exp_eulerMascheroni_of_upperPairing {p : ℝ → ℝ} (hp : ∀ t ∈ Set.uIcc 1 2, HasDerivAt p (-p (t + 1) / t) t) (hint : IntervalIntegrable (fun (t : ℝ) => p (t + 1) / t) MeasureTheory.volume 1 2) (hpair : suzukiUpperSourcePairing p 2 = 2) (hpone : p 1 = Real.exp (-Real.eulerMascheroniConstant)) : SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude = 2 * Real.exp Real.eulerMascheroniConstant

Exact final algebraic bridge. Its two hypotheses are precisely the two source statements still needing producers: Proposition 11.8(iii) for the actual upper source, and the independent standard-adjoint value r_{1,-1}(1)=exp(-γ).