theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_explicit_endpoint_error_absorb {H : Section13HatLayers} {N : ℕ} {D d Δ σ s outer logScale mainTerm total qEndpoint sigma11Endpoint ratioExcess qCoeff sigma11Coeff ratioCoeff : ℝ} (hs : 0 < s) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (hOuter : 0 ≤ outer) (hLogScale : 0 ≤ logScale) (hiii : ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * lambda H (ErrorSign.ofDepth N) D d 0 3) (hLambda3 : lambda H (ErrorSign.ofDepth N) D d 0 3 ≤ lambda H (ErrorSign.ofDepth N) D d 0 s) (hqEndpoint : qEndpoint ≤ qCoeff * errorEnvelope H N D d s) (hSigma11 : sigma11Endpoint ≤ outer * logScale * (sigma11Coeff * errorEnvelope H N D d s)) (hRatio : ratioExcess ≤ outer * logScale * (ratioCoeff * errorEnvelope H N D d s)) (hraw : total ≤ mainTerm + outer * logScale * ((1 / s * ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t) + qEndpoint) + sigma11Endpoint + ratioExcess) : total ≤ mainTerm + outer * logScale * (((1 - 1 / σ) ^ (1 - Δ) + qCoeff + sigma11Coeff + ratioCoeff) * errorEnvelope H N D d s)

Honest algebraic absorption of the Case-II endpoint error.

The raw endpoint estimate has three pieces after transport from the cubic endpoint: the Claim-14.6(iii) integral, the explicit qD/dimension-one endpoint, and the Sigma11 plus Euler-product-ratio excesses. Claim 14.6(iii) controls the integral at lambda ... 3; the separate hypothesis hLambda3 is intentionally visible because Claim 14.6(i) is only stated on [betaHat+epsilon, sigma] and, at odd depth with betaHat=2, does not compare a Case-II point s<3 with 3. Likewise the two explicit endpoint bounds are kept as exact premises; proving them may require a distinct large-D inequality.

This theorem is arranged in the scale used by Claim 14.5: outer * logScale * errorEnvelope. It is directly reusable after instantiating outer with the Euler-product/exponential prefactor and logScale with (log D)^(-Delta).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseII_explicit_endpoint_error_absorb_packet {H : Section13HatLayers} {N : ℕ} {D d Δ σ s outer logScale mainTerm total explicitEndpoint endpointCoeff : ℝ} (hs : 0 < s) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (hOuter : 0 ≤ outer) (hLogScale : 0 ≤ logScale) (hiii : ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * lambda H (ErrorSign.ofDepth N) D d 0 3) (hLambda3 : lambda H (ErrorSign.ofDepth N) D d 0 3 ≤ lambda H (ErrorSign.ofDepth N) D d 0 s) (hexplicit : explicitEndpoint ≤ outer * logScale * (endpointCoeff * errorEnvelope H N D d s)) (hraw : total ≤ mainTerm + outer * logScale * (1 / s * ∫ (t : ℝ) in 3..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t) + explicitEndpoint) : total ≤ mainTerm + outer * logScale * (((1 - 1 / σ) ^ (1 - Δ) + endpointCoeff) * errorEnvelope H N D d s)

A convenient version in which the three non-integral explicit errors are bounded together. This is the maximal honest endpoint theorem when the product-ratio and Sigma11 estimates are available only as one eventual large-D packet.