theorem MathlibNt.SieveTheory.pointwiseInductionContract_of_movingDomainIH (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N D Dmin : ℕ) (σ τ : ℝ) (hDmin : 2 ≤ Dmin) (hprime : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊, Nat.Prime p) (hscale : SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D Dmin σ τ) (hinherited : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D σ τ, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) (hV : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D σ τ, 0 ≤ SwitchingPrinciple.suzukiVProduct S ↑p) (hC : 0 ≤ C) (hSource : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D σ τ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hError : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D σ τ, SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hrecursiveSigma : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) D σ τ, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d) (hIH : Lemma144MovingDomainGlobalDepthAt S H C K d Δ (N - 1) Dmin) : SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / τ)⌉₊) (suzukiActualT S) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) 2 C K Δ N D σ τ

Instantiate the predecessor IH only at the actual quotient-recursive coordinates. The carrier geometry supplies their moving-domain bound.

theorem MathlibNt.SieveTheory.lemma14_4_caseI_successor_sameC_uniform_strict_moving (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {C C145 K d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 < C) (hC145 : 0 < C145) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), 2 ≤ N → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; 4 ≤ D → 1 < σ → s ≤ σ → 2 ≤ ↑D ^ (1 / s) → 2 ≤ ↑D ^ (1 / σ) → ↑D ^ (1 / σ) ≤ ↑D ^ (1 / s) → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s → (∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, Nat.Prime p) → SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S z) D Dmin σ s → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d) → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (N - 1) Dmin → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → suzukiActualT S N D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + sigma12InheritedBudget S H N D z C K d Δ s

Uniform Case-I successor with literally the same C: one cutoff precedes N,s, and every geometry/IH premise follows those binders.