Finite source-Q weighted derivatives and telescoping

This module closes the finite, source-level calculus behind Suzuki Proposition 9.3(iii) and Proposition 9.4(vi), specialized to κ = 1, β = 2.

The base layer is kept separate. On 2 < s < 3, its weighted derivative is -1; this is the term which combines with the even-layer derivatives to recover the prescribed history Q(s-1) = A_m/(s-1). Above 3, the ordinary layer recurrences telescope, leaving only the last even layer.

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiLayer_one_one_two_of_lt_three {s : ℝ} (hs0 : 0 < s) (hs3 : s < 3) : HasDerivAt (fun (u : ℝ) => u * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 1 u) (-1) s

The exceptional f₁ derivative on the first source strip. This is the base term used in the 2 < s < 3 finite-Q equation.

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiLayer_one_one_two_of_three_lt {s : ℝ} (hs3 : 3 < s) : HasDerivAt (fun (u : ℝ) => u * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 1 u) 0 s

Above the support endpoint of f₁, its weighted derivative is zero.

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiLayer_one_two_of_two_le {s : ℝ} {n : ℕ} (hn : 2 ≤ n) (hs : 2 + ↑(SuzukiFiniteContinuousLayers.sourceEpsilon n) < s) : HasDerivAt (fun (u : ℝ) => u * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 n u) (-SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (n - 1) (s - 1)) s

The ordinary recursive weighted derivative, stated separately from the exceptional base layer.

theorem MathlibNt.SieveTheory.sum_range_suzukiLayer_even_predecessors (m : ℕ) (x : ℝ) : ∑ k ∈ Finset.range m, SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k) x = suzukiEvenSourceLowerPartialSum m x - SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * m) x

The even predecessors of the first m odd layers are exactly the first m even layers with the terminal even layer removed. This is the finite index telescope in Proposition 9.3(iii).

theorem MathlibNt.SieveTheory.sum_range_suzukiLayer_odd_predecessors (m : ℕ) (x : ℝ) : ∑ k ∈ Finset.range m, SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1) - 1) x = suzukiOddSourceUpperPartialSum m x

The predecessors of the first m even layers are exactly the first m odd layers.

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiProposition118SourceQPrefix_low {m : ℕ} (hm : 1 ≤ m) {s : ℝ} (hs2 : 2 < s) (hs3 : s < 3) : HasDerivAt (fun (u : ℝ) => u * suzukiProposition118SourceQPrefix m u) (-suzukiProposition118SourceQPrefix m (s - 1)) s

On the missing window 2 < s < 3, the finite source prefix satisfies the exact weighted delay equation with no residual. The -1 from f₁ is essential: it turns 1 + T_{2m-1}(s-1) into the prescribed history A_m/(s-1).

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiProposition118SourceQPrefix_high (m : ℕ) {s : ℝ} (hs3 : 3 < s) : HasDerivAt (fun (u : ℝ) => u * suzukiProposition118SourceQPrefix m u) (-suzukiProposition118SourceQPrefix m (s - 1) + SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * m) (s - 1)) s

Above the common differentiability threshold 3, all recursive layers differentiate and telescope; only the last even layer remains.

theorem MathlibNt.SieveTheory.hasDerivAt_weighted_suzukiProposition118SourceQPrefix {m : ℕ} (hm : 1 ≤ m) {s : ℝ} (hs2 : 2 < s) (hs3 : s ≠ 3) : HasDerivAt (fun (u : ℝ) => u * suzukiProposition118SourceQPrefix m u) (-suzukiProposition118SourceQPrefix m (s - 1) + suzukiProposition118SourceQTerminal m s) s

Unified finite telescoping equation away from the genuine source kink s = 3. The residual is exactly suzukiProposition118SourceQTerminal.