@[reducible, inline]

abbrev MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.CutoffMajorant (R : ℝ → ℝ) : Type

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.CutoffMajorant = Section10Lemma1028FirstCrossing.Section10CommonMajorant

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.section10_unitShift_after_cutoff {R : ℝ → ℝ} (hDDE : Section10DDEApparatus R 3) (Q : CutoffMajorant R) {s : ℝ} (hs : Q.cutoff ≤ s) : R s ≤ Q.A / (s * Real.log (Real.exp 1 * s)) * R (s - 1)

Cutoff-corrected one-unit estimate for the genuine scalar DDE(2,1,3). The estimate is derived from the eventual Lemma 10.28 majorant and is not a field of either input interface.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.section13Hat_unitShift_after_cutoff {H : Section13HatLayers} (sign : ErrorSign) (B : BridgeAssembly.Section13HatSection10BridgeAtThree H sign) (Q : CutoffMajorant B.Qhat) {s : ℝ} (hs : Q.cutoff ≤ s) : H.T sign s ≤ B.K ^ 2 * Q.A / (s * Real.log (Real.exp 1 * s)) * H.T sign (s - 1)

Sign-independent transport of the cutoff-corrected unit shift. Both signs use the same real Qhat scalar DDE domain β = 3.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.section13Hat_twoStep_after_cutoff {H : Section13HatLayers} (sign : ErrorSign) (B : BridgeAssembly.Section13HatSection10BridgeAtThree H sign) (Q : CutoffMajorant B.Qhat) {M : ℝ} (hM : Q.cutoff ≤ M + 1) : H.T sign (M + 2) ≤ (B.K ^ 2 * Q.A) ^ 2 / ((M + 1) * Real.log (Real.exp 1 * (M + 1)) * ((M + 2) * Real.log (Real.exp 1 * (M + 2)))) * H.T sign M

The corresponding two-unit ratio, obtained by two applications of the cutoff-corrected unit shift (and not stored in either source record).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.CutoffCorrectedRatio.section13HatAsymptoticContract_of_atThree_cutoff {H : Section13HatLayers} (hH : Section13HatContract H 2) (bridge : (sign : ErrorSign) → BridgeAssembly.Section13HatSection10BridgeAtThree H sign) (majorant : (sign : ErrorSign) → CutoffMajorant (bridge sign).Qhat) : Section13HatAsymptoticContract H

Cutoff-corrected Proposition 13.1 ratio interface. The compact interval before the eventual cutoff is handled only by continuity and positivity; after the cutoff, two derived unit shifts provide the logarithmic-square decay.