theorem MathlibNt.SieveTheory.caseI1423_sigmaZero_realEndpoint_sourceBound (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C C145 K d Δ : ℝ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hC145 : 0 ≤ C145) : ∃ (A0 : ℝ), 0 ≤ A0 ∧ ∀ (N : ℕ) (s : ℝ), 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → ∀ᶠ (D : ℕ) in Filter.atTop, s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; caseISigmaZeroDirectRemainder S H N D C145 K d Δ ≤ A0 * caseI1423RemainderUnit (sigma12InheritedBudget S H N D z C K d Δ s) (↑D) σ

Claim 14.6(i) transports the direct Σ₀ packet from its moving source endpoint to the fixed Case-I budget coordinate.