Claim 14.6(i) to the production error envelope

The production definitions do not identify lambda H sign D d 0 s directly with errorEnvelope H N D d s: at κ = 1, lambda has one additional factor of s. This file records the exact normalization and derives the endpoint transport needed from Claim 14.6(i).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_eq_lambda_div_internal (H : Section13HatLayers) {N : ℕ} {D d s : ℝ} (hs : 0 < s) : errorEnvelope H N D d s = lambda H (ErrorSign.ofDepth N) D d 0 s / s

Exact production normalization at κ = 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_eq_s_mul_errorEnvelope (H : Section13HatLayers) {N : ℕ} {D d s : ℝ} (hs : 0 < s) : lambda H (ErrorSign.ofDepth N) D d 0 s = s * errorEnvelope H N D d s

Equivalent orientation: lambda is s times the error envelope, rather than literally the error envelope.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_antitoneOn_of_claim14_6_internal {H : Section13HatLayers} {β D d σ : ℝ} (N : ℕ) (hH : Section13HatContract H β) (hD : 1 < D) (hi : Claim14_6_MonotoneLambdaPremise H D d σ) : AntitoneOn (errorEnvelope H N D d) (Set.Icc (H.betaHat + (ErrorSign.ofDepth N).epsilon) σ)

Claim 14.6(i) makes the production error envelope antitone on the matching parity interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_endpoint_le_of_claim14_6 {H : Section13HatLayers} {β D d σ s : ℝ} {N : ℕ} (hH : Section13HatContract H β) (hD : 1 < D) (hi : Claim14_6_MonotoneLambdaPremise H D d σ) (hs : s ∈ Set.Icc (H.betaHat + (ErrorSign.ofDepth N).epsilon) σ) : errorEnvelope H N D d σ ≤ errorEnvelope H N D d s

Pointwise endpoint transport E(σ) ≤ E(s) under the Claim 14.6(i) domain hypotheses.