noncomputable def MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracket (N : ℕ) (D d Δ σ C K : ℝ) : ℝ

The relative coefficient used by the double-rounded Case-II endpoint. The natural cutoffs occur only in the discrete sum and Euler product; all analytic coordinates in this coefficient remain the exact real roots.

Equations

• MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracket N D d Δ σ C K = (1 + 3 * K / Real.log D) * (1 - 1 / σ) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 + MathlibNt.SieveTheory.caseIISharpPositiveEndpointRelativeCoeff N D d Δ σ C K

theorem MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracket_C_independent (N : ℕ) (D d Δ σ C₁ C₂ K : ℝ) : caseIIConcreteRoundedRelativeBracket N D d Δ σ C₁ K = caseIIConcreteRoundedRelativeBracket N D d Δ σ C₂ K

The repaired relative bracket is genuinely scale-free: changing the outer constant C does not change it.

theorem MathlibNt.SieveTheory.caseII_total_le_doubleRounded_concrete_relative_of_rawBase_natCeil (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D y z : ℕ} {yr zr d Δ σ C K B0 s : ℝ} (hD : Real.exp 1 ≤ ↑D) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hs1 : 1 < s) (hK : 0 ≤ K) (hC : 0 ≤ C) (hσ : 0 ≤ σ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hyr : yr = ↑D ^ (1 / 3)) (hzr : zr = ↑D ^ (1 / s)) (_hyceil : y = ⌈yr⌉₊) (_hzceil : z = ⌈zr⌉₊) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (hClaim14_6_iii : ∫ (t : ℝ) in 3..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) (↑D) d 0 3) (hLambdaCubic : SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) (↑D) d 0 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation (↑D) d 0 3 * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) (↑D) d 0 s) (hP : 1 ≤ C * Real.exp √K) (hPE : 1 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (hE : 1 / 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (hRaw : ∑ n ∈ Finset.Icc 1 N with n % 2 = N % 2, suzukiSourceV S n D z ≤ SwitchingPrinciple.suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + caseIIRoundedEndpointErr S H N D z yr zr d Δ σ C K B0 s + SwitchingPrinciple.suzukiVProduct S ↑z * (K * 3 ^ 2 / (s * Real.log ↑D))) : ∑ n ∈ Finset.Icc 1 N with n % 2 = N % 2, suzukiSourceV S n D z ≤ B0 + SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * caseIIConcreteRoundedRelativeBracket N (↑D) d Δ σ C K)

Concrete relative assembly from the double-rounded sharp raw endpoint.

The premise hRaw is the canonicalized rounded raw conclusion obtained after applying the explicit transport-error bridge. A downstream direct theorem connects it to the long Claim-14.5 input packet. The rounded endpoint packet and the exact-real-root integral transport are consumed internally.

theorem MathlibNt.SieveTheory.exists_caseIIConcreteRoundedRelativeBracket_lt_one_threshold (N : ℕ) (K C d Δ : ℝ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hK : 0 ≤ K) (hC : 0 ≤ C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → caseIIConcreteRoundedRelativeBracket N D d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) C K < 1

Eventual consumer for the concrete rounded bracket.