noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile (C s : ℝ) : ℝ

Quantitative lower profile in Proposition 13.1(ii), κ = 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s = Real.exp (-s * Real.log s - s * Real.log (Real.log (3 * s)) - C * s)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131iiUniformQuantitativeLower (H : Section13HatLayers) : Prop

Uniform two-sign quantitative lower form of Proposition 13.1(ii).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131iiUniformQuantitativeLower H = ∃ (C : ℝ) (M : ℝ), 0 ≤ C ∧ 3 ≤ M ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), M ≤ s → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s ≤ H.T sign s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131ii_source_tail_identity {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {s : ℝ} (hs : 3 < s) : ∫ (t : ℝ) in Set.Ioi s, hatTailIntegrand H sign t = weightedHat H sign s

The first, fully internal step of the lower-bound argument: the source DDE and weightedHat → 0 give the exact positive tail representation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131ii_first_unit_strict {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {s : ℝ} (hs : 3 < s) : ∫ (t : ℝ) in s..s + 1, hatTailIntegrand H sign t < weightedHat H sign s

Every first unit of the tail has mass strictly smaller than the whole tail. This is the positivity input used by the source unit-interval iteration.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131ii_first_unit_pointwise {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {s t : ℝ} (hs : 4 < s) (ht : t ∈ Set.Icc s (s + 1)) : 1 / s * weightedHat H sign.opposite s ≤ hatTailIntegrand H sign t

Pointwise kernel estimate on the first unit. Together with the preceding strict mass inequality it is the first nontrivial ratio produced by the unit-interval argument, without assuming any lower or asymptotic estimate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131ii_first_unit_ratio {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {s : ℝ} (hs : 4 < s) : 1 / s * weightedHat H sign.opposite s < weightedHat H sign s

The resulting honest one-unit ratio edge. It is strictly weaker than the factorial iteration needed for Proposition 13.1(ii), but is derived solely from the source contract and identifies the exact starting inequality for that iteration.