Claim 14.6(i) bridge for the ceiling-coordinate error envelope

At κ = 1, the production error envelope satisfies E_N(D,s) = Λ₀^{sign(N)}(s) / s. Thus, on a positive interval, nonnegativity and antitonicity of Λ₀ imply antitonicity of E_N. The final theorem supplies this fact to the hError slot of the natural-ceiling coordinate bridge from SuzukiLemma144Equation1410.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_eq_lambda_div (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

At κ = 1, the production error envelope is Λ₀/s at the parity sign selected by the depth.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_antitoneOn_of_claim14_6 {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), together with the Section-13 positivity package, makes the production error envelope antitone on the matching parity interval. The proof uses E = Λ₀/s: both Λ₀ and 1/s decrease on a positive interval, while Λ₀ is nonnegative.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.naturalCeilContract_to_sourceCoordinate_errorEnvelope_of_claim14_6 (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (H : Section13HatLayers) (β C K Δ d : ℝ) (N D : ℕ) (σ τ : ℝ) (hH : Section13HatContract H β) (hV : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 0 ≤ V p) (hC : 0 ≤ C) (hlog : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 0 ≤ Real.log ↑(D ⌈/⌉ p)) (hSource : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hCeil : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 2 ≤ p ∧ 2 * p ≤ D) (hClaim : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ) (hDomain : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ Set.Icc (H.betaHat + (ErrorSign.ofDepth (N - 1)).epsilon) σ ∧ SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ Set.Icc (H.betaHat + (ErrorSign.ofDepth (N - 1)).epsilon) σ) (hIH : SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract support T V (fun (n D' : ℕ) (s : ℝ) => errorEnvelope H n (↑D') d s) β C K Δ N D σ τ) : SuzukiLemma144Equation1410.PointwiseInductionContract support T V (fun (n D' : ℕ) (s : ℝ) => errorEnvelope H n (↑D') d s) β C K Δ N D σ τ

Production instantiation of the natural-ceiling source-coordinate bridge. For each recursive natural argument ⌈D/p⌉, Claim 14.6(i) is assumed on its matching parity domain. When both the inherited and recursive coordinates lie in that domain, the preceding antitonicity theorem discharges hError.

The elementary hypotheses 2 ≤ p and 2p ≤ D provide both the ordering of the two coordinates and 1 < ⌈D/p⌉, the positivity condition needed by the production errorEnvelope normalization.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.naturalCeilContract_to_sourceCoordinate_errorEnvelope_of_claim14_6_and_parityDomain (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (H : Section13HatLayers) (β C K Δ d : ℝ) (N D : ℕ) (σ τ : ℝ) (hH : Section13HatContract H β) (hV : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 0 ≤ V p) (hC : 0 ≤ C) (hlog : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 0 ≤ Real.log ↑(D ⌈/⌉ p)) (hCeil : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, 2 ≤ p ∧ 2 * p ≤ D) (hSourceDomain : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1) ∧ SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hClaim : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ) (hErrorDomain : ∀ p ∈ SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ Set.Icc (H.betaHat + (ErrorSign.ofDepth (N - 1)).epsilon) σ ∧ SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ Set.Icc (H.betaHat + (ErrorSign.ofDepth (N - 1)).epsilon) σ) (hIH : SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract support T V (fun (n D' : ℕ) (s : ℝ) => errorEnvelope H n (↑D') d s) β C K Δ N D σ τ) : SuzukiLemma144Equation1410.PointwiseInductionContract support T V (fun (n D' : ℕ) (s : ℝ) => errorEnvelope H n (↑D') d s) β C K Δ N D σ τ

Fully discharged production ceiling bridge. In addition to Claim 14.6(i) for the error envelope, Proposition 9.3 supplies the source-layer comparison from the same explicit ceiling bounds and the two parity-domain memberships. Thus callers provide the genuine natural-ceiling induction contract, with no pre-packaged hSource or hError inequality.