theorem MathlibNt.SieveTheory.compact_tail_integral {f : ℝ → ℝ} {x B : ℝ} (hcont : ContinuousOn f (Set.Icc x B)) (hzero : ∀ (t : ℝ), B ≤ t → f t = 0) : MeasureTheory.IntegrableOn f (Set.Ioi x) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi x, f t = ∫ (t : ℝ) in min x B..B, f t

A continuous function vanishing beyond an endpoint has an integrable compact tail.

theorem MathlibNt.SieveTheory.Lemma132FiniteTailIdentity_exactRecursionThreshold (N : ℕ) (x : ℝ) : 2 ≤ N → 2 + ↑(N % 2) ≤ x → MeasureTheory.IntegrableOn (fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (t - 1)) (Set.Ioi x) MeasureTheory.volume ∧ x * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x = ∫ (t : ℝ) in Set.Ioi x, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (t - 1)

The finite-tail identity at the exact lower threshold used by the recursive numerator: 2 on even layers and 3 on odd layers.

The weaker hypothesis x ∈ parityDomain 2 N is sufficient on the even branch, but not on the odd branch: there it only says 1 < x, while the recursive lower endpoint remains clamped at 3.

theorem MathlibNt.SieveTheory.Lemma132FiniteTailIdentity_even_parityDomain (N : ℕ) (x : ℝ) (hN : 2 ≤ N) (hEven : N % 2 = 0) (hx : x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) : MeasureTheory.IntegrableOn (fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (t - 1)) (Set.Ioi x) MeasureTheory.volume ∧ x * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x = ∫ (t : ℝ) in Set.Ioi x, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (t - 1)

On the even parity branch, Suzuki's exact parity-domain lower endpoint is already the exact recursion threshold.