No-Dmin bridges for the source Lemma 14.4 induction

The literal all-D ≥ 2 predecessor assertion is exactly the production moving contract at cutoff 2. This file records that conversion and the two concrete pre-branch transports needed by the direct source induction. It deliberately reuses ActualClaim145BoundAt and claim14_5Scale; no second Claim-14.5 scale is introduced.

theorem MathlibNt.SieveTheory.lemma144MovingDomainGlobalDepthAt_two_iff_allD (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N : ℕ) : Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 ↔ ∀ (D z : ℕ), 2 ≤ D → 2 ≤ z → ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, x ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → ↑D ^ (1 / x) = ↑z → suzukiActualT S N D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d x * Real.log ↑D ^ (-Δ))

A literal all-D ≥ 2 predecessor assertion is the moving-domain contract with Dmin = 2. This is the bridge used when the source induction hypothesis has no cutoff binder.

theorem MathlibNt.SieveTheory.nat_cutoff_paid_by_source_log_large {D D0 : ℕ} {C1 K Θ : ℝ} (hD : 2 ≤ D) (hD0 : 2 ≤ D0) (hbudget : Real.log ↑D0 ≤ C1 * K ^ Θ) (hlarge : C1 * K ^ Θ < Real.log ↑D) : D0 ≤ D

A source logarithmic lower bound pays any fixed natural cutoff. The cutoff is selected before the depth, exactly as in the production moving Case-I and Case-II eventual APIs.

theorem MathlibNt.SieveTheory.claim14_5VProduct_le_suzukiVProduct (S : BoundingSieve) {z D : ℝ} (hzD : z ≤ D) : SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D ≤ SwitchingPrinciple.suzukiVProduct S z

The production Euler product decreases when its cutoff is enlarged.

theorem MathlibNt.SieveTheory.ActualClaim145BoundAt.to_lemma144_moving_of_scalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ s : ℝ} {N D : ℕ} (hC145 : 0 ≤ C145) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD : 2 ≤ D) (hs : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) (hzD : ↑⌈↑D ^ (1 / s)⌉₊ ≤ ↑D) (hscalar : C145 / (Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ C) (hclaim : ActualClaim145BoundAt S H N D d Δ K s C145) : suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

Concrete normalization from the production Claim-14.5 bound to the Lemma-14.4 right-hand side. The only scalar input is the literal inequality needed after unfolding the already-defined production scale.

noncomputable def MathlibNt.SieveTheory.claim145UniformNormalizationConstant (C145 d : ℝ) : ℝ

A concrete normalization constant for the Claim-14.5 scalar. It is fixed before the natural quotient D and uses only the lower endpoint D = 2.

Equations

• MathlibNt.SieveTheory.claim145UniformNormalizationConstant C145 d = C145 / (Real.log 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma 2 d)

theorem MathlibNt.SieveTheory.claim145_uniform_scalar_normalization (C145 d : ℝ) (hC145 : 0 ≤ C145) (hd : 0 < d) : 0 ≤ claim145UniformNormalizationConstant C145 d ∧ ∀ (D : ℕ), 2 ≤ D → C145 / (Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ claim145UniformNormalizationConstant C145 d

The Claim-14.5 scalar is uniformly bounded on the full source range D ≥ 2; no eventual-D threshold is used.

theorem MathlibNt.SieveTheory.exists_claim145_uniform_scalar_normalization (C145 d : ℝ) (hC145 : 0 ≤ C145) (hd : 0 < d) : ∃ (Cnorm : ℝ), 0 ≤ Cnorm ∧ ∀ (D : ℕ), 2 ≤ D → C145 / (Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ Cnorm

Existential form of the same uniform normalization, with the constant chosen before D.

theorem MathlibNt.SieveTheory.ActualClaim145BoundAt.to_lemma144_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C145 K d Δ s : ℝ} {N D : ℕ} (hC145 : 0 ≤ C145) (hd : 0 < d) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD : 2 ≤ D) (hs : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) (hzD : ↑⌈↑D ^ (1 / s)⌉₊ ≤ ↑D) (hclaim : ActualClaim145BoundAt S H N D d Δ K s C145) : suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + claim145UniformNormalizationConstant C145 d * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

Claim 14.5 implies the Lemma-14.4 moving right-hand side with one explicit constant independent of D. The natural ceiling and parity-domain hypotheses are unchanged from to_lemma144_moving_of_scalar.