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

The remaining source estimate, with all quantifiers exposed. It excludes the scalar equation (10.53) only for a genuine earliest-crossing candidate: the last implication explicitly carries the strict history before s. Thus this is not the withdrawn arbitrary-stationary exclusion, and it is not a majorant, delayed/current ratio, asymptotic certificate, or Claim statement.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.UniformQhatStationaryExclusion H = ∃ (s₀ : ℝ) (C : ℝ), 4 ≤ s₀ ∧ 1 ≤ C ∧ ∀ (c : ℝ), C ≤ c → (∀ u ∈ Set.Icc 4 s₀, Section10Lemma1028FirstCrossing.normalizedMinusBase (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat H) Section10CanonicalXi.xi u < c) → ∀ (s : ℝ), s₀ ≤ s → (∀ (u : ℝ), s₀ ≤ u → u < s → Section10Lemma1028FirstCrossing.normalizedMinusBase (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat H) Section10CanonicalXi.xi u < c) → Section10Lemma1028FirstCrossing.normalizedMinusBase (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat H) Section10CanonicalXi.xi s = c → False

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.canonical_log_lt_xi {s : ℝ} (hs : Real.exp 1 ≤ s) : Real.log s < Section10CanonicalXi.xi s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.canonicalXi_eventual_log_lower (c : ℝ) : ∃ (S : ℝ) (A : ℝ), 3 ≤ S ∧ 1 ≤ A ∧ ∀ (s : ℝ), S ≤ s → 1 / A * Real.log (Real.exp 1 * s) ≤ Section10CanonicalXi.xi s - c - 2 / s

The eventual logarithmic lower bound required by the sanitized Lemma 10.28 record, derived from the canonical inverse rather than assumed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.canonicalXiTheorem : Section10Lemma1028FirstCrossing.CanonicalXiTheorem Section10CanonicalXi.xi

Canonical ξ package used by the first-crossing constructor.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus (section13Qhat H) 3

The Section-13 source DDE, positivity and proved pairing identity give the complete non-circular first-crossing apparatus for the single function Qhat.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData hH = { adjoint := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus, beta_ge_one := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData._proof_2, continuous := ⋯, positive := ⋯, original_dde := ⋯, adjoint_positive := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData._proof_8, adjoint_dde := ⋯, pairing_zero := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.global_nonpos_of_uniformQhatStationaryExclusion {H : Section13HatLayers} (hH : Section13HatSourceContract H) (hexcl : UniformQhatStationaryExclusion H) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ (s : ℝ), 4 ≤ s → Section10Lemma1028FirstCrossing.normalizedMinusBase (section13Qhat H) Section10CanonicalXi.xi s - c ≤ 0

Compactness turns the source-valid exclusion of genuine earliest candidates into the global nonpositive normalized slope. No derivative at the left endpoint is used: the construction is entirely a closed-set minimum argument.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13Qhat_cutoffMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) (hexcl : UniformQhatStationaryExclusion H) : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)

A single honest cutoff majorant for Qhat, produced from source data and the raw uniform stationary exclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13Qhat_cutoffMajorant hH hexcl = { xi := Section10CanonicalXi.xi, cMinus := Classical.choose ⋯, cutoff := max 4 (Classical.choose ⋯), A := Classical.choose ⋯, four_le_cutoff := ⋯, one_le_A := ⋯, majorizes_log := ⋯, envelope_slope_nonpos := ⋯ }

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.duplicateQhatMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) (Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)) (sign : ErrorSign) : CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat

The sign-indexed bridges are definitionally based on the same scalar Qhat; therefore the one majorant is reused, not reconstructed, for both signs.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.duplicateQhatMajorant hH Q x✝ = Q

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.MovingClaim146iiiConclusion (H : Section13HatLayers) (d Δ : ℝ) : Prop

Exact moving Claim 14.6(iii) conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.MovingClaim146iiiConclusion H d Δ = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → ∫ (t : ℝ) in s..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t < (1 - 1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.moving_claim14_6_iii_of_uniformQhatStationaryExclusion {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d Δ : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hexcl : UniformQhatStationaryExclusion H) : MovingClaim146iiiConclusion H d Δ

Section 13 Qhat single-majorant closure through the moving Claim 14.6(iii). The only residual premise is the quantified candidate-level stationary exclusion above; no majorant, ratio, certificate, or Claim conclusion is assumed.