theorem MathlibNt.SieveTheory.errorEnvelope_antitoneOn_plus_lowStrip {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {N : ℕ} {D d : ℝ} (hsign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N = SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus) (hd : 0 ≤ d) (hD : 1 < D) (hlarge : (1 + 3 * d) * 4 ^ d ≤ 1 / 3 * Real.log D) : AntitoneOn (SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d) (Set.Icc 1 3)

On the odd predecessor's initial strip, the exact Section-13 value weightedHat H plus = 1 turns the envelope into perturbation/t; for a large enough recursive argument this quotient is antitone on [1,3].

theorem MathlibNt.SieveTheory.errorEnvelope_coordinate_transport_full {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {N : ℕ} {D d σ x y : ℝ} (hd : 0 ≤ d) (hD : 1 < D) (hlarge : (1 + 3 * d) * 4 ^ d ≤ 1 / 3 * Real.log D) (hi : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H D d σ) (hxdom : x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) (hxy : x ≤ y) (hyσ : y ≤ σ) : SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d y ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d x

Full coordinate transport. The minus predecessor is already in the Claim-14.6(i) interval. For the plus predecessor, the proof uses the exact initial formula below 3, Claim 14.6(i) above 3, and composes the two bounds when the coordinate pair crosses 3.