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

The exact source-endpoint Claim 14.6 packet needed by the rounded producer. It is strictly upstream of the desired Lemma 14.4 successor conclusion.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddSourceClaim146 H d Δ = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H D d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ∧ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H D d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma 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

def MathlibNt.SieveTheory.Lemma144CaseIIOddRawRoundedProducer (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (B₀ : ℕ → ℕ → ℝ) (d Δ C K : ℝ) : Prop

Exact accepted raw producer boundary. This is the conclusion of caseII_total_le_doubleRounded_direct_concrete_relative_natCeil after its source geometry and Claim-14.6 premises have been supplied. It contains the recursive raw base B₀, but does not contain or assume the desired successor.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddRawRoundedProducer S H B₀ d Δ C K = ∀ (N D : ℕ) (s : ℝ), Odd N → 3 ≤ N → 1 < s → s ≤ 3 → MathlibNt.SieveTheory.SourceRoundedGeometryPacket S D ⌈↑D ^ (1 / 3)⌉₊ ⌈↑D ^ (1 / s)⌉₊ d s → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H (↑D) d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → ∫ (t : ℝ) in 3..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t ≤ (1 - 1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) (↑D) d 0 3 → have z := ⌈↑D ^ (1 / s)⌉₊; ∑ n ∈ Finset.Icc 1 N with n % 2 = N % 2, MathlibNt.SieveTheory.suzukiSourceV S n D z ≤ B₀ N D + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracket N (↑D) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C K)

theorem MathlibNt.SieveTheory.lemma144_caseII_odd_roundedRelativeProducer_of_raw (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {B₀ : ℕ → ℕ → ℝ} {d Δ C K : ℝ} (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC : 0 ≤ C) (hK : 0 ≤ K) (h146 : Lemma144CaseIIOddSourceClaim146 H d Δ) (hraw : Lemma144CaseIIOddRawRoundedProducer S H B₀ d Δ C K) : Lemma144CaseIIOddRoundedRelativeProducer S H B₀ d Δ C K

Source geometry, the source Claim-14.6 packet, the eventual concrete bracket, and the raw double-rounded producer construct the rounded-relative producer required by the same-C terminal algebra.

theorem MathlibNt.SieveTheory.lemma144_caseII_odd_sameC_producer_of_raw_and_scaling (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C K C145 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC : 0 < C) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (h146 : Lemma144CaseIIOddSourceClaim146 H d Δ) (hraw : Lemma144CaseIIOddRawRoundedProducer S H (caseIIOddClaim145Endpoint S d) d Δ C K) (hs1 : 1 < s) (hs3 : s ≤ 3) : Lemma144CaseIIOddSuccessorSameCProducer S H d Δ C K s

Full odd same-C producer. Claim 14.5 and its scaling bridge are consumed internally; the only remaining discrete premise is the exact raw producer.

theorem MathlibNt.SieveTheory.lemma144_caseII_odd_sameC_producer_of_raw_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C K C145 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hC : 0 < C) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hraw : Lemma144CaseIIOddRawRoundedProducer S H (caseIIOddClaim145Endpoint S d) d Δ C K) (hs1 : 1 < s) (hs3 : s ≤ 3) : Lemma144CaseIIOddSuccessorSameCProducer S H d Δ C K s