Lemma 14.4: Case-I successor and same-constant absorption

This is the maximal source-faithful reduction available in the current compiled import cone. It uses the literal finite (14.9) equality and the production (14.10) assembler. It assumes neither a mainSum bound, a Claim-14.5/14.6 conclusion, nor a Case-I producer.

The source files for the newer Case-I recurrence/endpoint modules are present, but their .olean modules are absent from the production search path. The purported full internal Claim-14.6 source also does not rebuild: it imports a staged declaration of Section13HatAsymptoticContract which collides with the production declaration. Therefore the exact three analytic estimates not yet available as compiled theorems are exposed below, before terminal scalar absorption:

• hSigma0: the low-prime source estimate supplied mathematically by Claim 14.5 at the endpoint σ;
• hSigma11: the endpoint remainder after the finite-source-layer main term;
• hSigma12: the internal-Claim-14.6 contraction multiplier plus endpoint remainder.

These are source estimates, not renamed final conclusions. Σ₂ is retained in (14.9) and separately eliminated by its exact Case-I zero identity.

noncomputable def MathlibNt.SieveTheory.lemma144ParityIndices (N : ℕ) : Finset ℕ

The finite parity index set occurring in Suzuki's source T_N.

Equations

• MathlibNt.SieveTheory.lemma144ParityIndices N = {n ∈ Finset.Icc 1 N | n % 2 = N % 2}

noncomputable def MathlibNt.SieveTheory.lemma144SourcePred (S : BoundingSieve) (n D p : ℕ) : ℝ

Literal source predecessor sum used in (14.9)--(14.10).

Equations

• MathlibNt.SieveTheory.lemma144SourcePred S n D p = ∑ m ∈ MathlibNt.SieveTheory.lemma144ParityIndices n, MathlibNt.SieveTheory.suzukiSourceV S m D p

structure MathlibNt.SieveTheory.Lemma144StrictFactor : Type

Strict multiplier certificate for same-C absorption.

• ρ : ℝ
• nonneg : 0 ≤ self.ρ
• lt_one : self.ρ < 1

def MathlibNt.SieveTheory.Lemma144Equation149 (S : BoundingSieve) (N D z : ℕ) (σ τ : ℝ) : Prop

Actual finite (14.9), stated on its three literal source sums.

Equations

• MathlibNt.SieveTheory.Lemma144Equation149 S N D z σ τ = (∑ n ∈ MathlibNt.SieveTheory.lemma144ParityIndices N, MathlibNt.SieveTheory.suzukiSourceV S n D z = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), S.nu p * MathlibNt.SieveTheory.lemma144SourcePred S (N - 1) (D ⌈/⌉ p) p + MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOne (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) (MathlibNt.SieveTheory.lemma144SourcePred S) N D σ τ + ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / τ) ≤ ↑p, S.nu p * MathlibNt.SieveTheory.lemma144SourcePred S (N - 1) (D ⌈/⌉ p) p)

theorem MathlibNt.SieveTheory.lemma14_4_caseI_successor_sameC (S : BoundingSieve) (V : ℕ → ℝ) {N D z : ℕ} {β σ τ s C K Δ Vz E ρ e0 e11 e12 : ℝ} (hN2 : 2 ≤ N) (hτs : τ = s) (h149 : Lemma144Equation149 S N D z σ τ) (hSigma2Zero : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / τ) ≤ ↑p, S.nu p * lemma144SourcePred S (N - 1) (D ⌈/⌉ p) p = 0) (hVz : Vz ≠ 0) (hnu : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ τ, 0 ≤ S.nu p) (hIH : SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract (SwitchingPrinciple.suzukiSupportedBelow S z) (lemma144SourcePred S) V (fun (x x_1 : ℕ) (x_2 : ℝ) => E) β C K Δ N D σ τ) (hSigma0 : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), S.nu p * lemma144SourcePred S (N - 1) (D ⌈/⌉ p) p ≤ e0) (hSigma11 : SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven (SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) V Vz β N D σ τ ≤ Vz * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + e11) (hSigma12 : SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve (SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) V (fun (x x_1 : ℕ) (x_2 : ℝ) => E) Vz C K Δ N D σ τ ≤ ρ * (C * E) + e12) (q : Lemma144StrictFactor) (hq : q.ρ = ρ) (hside : e0 + e11 + e12 ≤ (1 - ρ) * (C * E)) : ∑ n ∈ lemma144ParityIndices N, suzukiSourceV S n D z ≤ Vz * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + C * E

The genuine N-1 → N Case-I successor reduction. The same constant C appears in hIH, in the contracted inherited budget, and in the conclusion. No C_N is introduced.

The only induction use is hIH, consumed by the actual equation14_10_finset_assembly. The side allocation is strict in the analytic sense ρ < 1, recorded by q.lt_one.

theorem MathlibNt.SieveTheory.lemma14_4_finite_depth_from_caseI_successor (depth : ℕ) (P : ℕ → Prop) (hbase : P 1) (hsucc : ∀ (N : ℕ), 2 ≤ N → N ≤ depth → P (N - 1) → P N) (N : ℕ) : 1 ≤ N → N ≤ depth → P N

Finite-depth termination, based at the genuine depth one. Every successor call decreases to N-1; hence a target N ≤ depth reaches the base after at most N-1 calls.