theorem MathlibNt.SieveTheory.lemma14_4_base_one_full_global_allD {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ1 : Δ < 1) (hCbase : lemma144BaseOneGlobalConstant Δ ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : Lemma144MovingDomainNatCeilAt S H C K d Δ 1 2

The literal no-cutoff depth-one base. The low strip is supplied by lemma14_4_base_one_lowStrip_global_allD; on the complementary Case-I strip 3 < s, both the discrete depth-one source and its continuous main term vanish.

theorem MathlibNt.SieveTheory.lemma144_caseI_additive_to_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C K d Δ s : ℝ} {M D : ℕ} (h : suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s) : suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H M (↑D) d s * Real.log ↑D ^ (-Δ))

Convert the additive output exported by the strict/even Case-I producers to exactly the bracketed moving-domain target used by the no-Dmin induction.

theorem MathlibNt.SieveTheory.lemma14_4_noDmin_allDepth_of_sourceLarge_strict_even (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ C1 Θ : ℝ} (hC145 : 0 ≤ C145) (hd : 0 < d) (hCnorm : claim145UniformNormalizationConstant C145 d ≤ C) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hΔ1 : Δ < 1) (hCbase : lemma144BaseOneGlobalConstant Δ ≤ C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hclaim : ∀ (N D : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145) (hstrict : ∀ (M D : ℕ) (s : ℝ), 2 ≤ M → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon ≤ s → C1 * K ^ Θ < Real.log ↑D → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon < s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 → suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s) (heven : ∀ (M D : ℕ), Even M → 2 ≤ M → 2 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → C1 * K ^ Θ < Real.log ↑D → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 → suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / 2)⌉₊ C K d Δ 2) (hcaseII : ∀ (N D : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N + 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → Lemma144CaseIIFinalSide (N + 1) s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 → suzukiActualT S (N + 1) D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N + 1) s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N + 1) (↑D) d s * Real.log ↑D ^ (-Δ))) (N : ℕ) : 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Literal all-depth/no-Dmin assembly interface after the pointwise source-large strict and even-endpoint Case-I producers land. Their conclusions are kept in the additive form they actually export; this glue performs only the parity/endpoint split and algebraic repackaging.