Lemma 14.4, Case I: final producer boundary

Support primality, quotient threshold geometry, inherited parity membership, finite-layer transport, quotient bounds, T positivity, and Claim 14.13 are automatic. The earliest missing edge is error-envelope transport: at an odd predecessor depth the parity domain starts strictly above 1, while Claim 14.6(i) is only available from 3 onward.

def MathlibNt.SieveTheory.CaseIRecursiveCoordinateSourceSigmaQuotient (S : BoundingSieve) (_N D : ℕ) (d s : ℝ) : Prop

The sole source-coordinate edge not generated by carrier geometry. It is stated at the literal ceiling quotient and literal moving sourceSigma endpoint.

Equations

• MathlibNt.SieveTheory.CaseIRecursiveCoordinateSourceSigmaQuotient S _N D d s = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d

theorem MathlibNt.SieveTheory.caseI_inheritedCoordinate_gt {D p : ℕ} {s : ℝ} (hp : 2 ≤ p) (hD : 1 < D) (hs : 0 < s) (hupper : ↑p < ↑D ^ (1 / s)) : s - 1 < SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p

A strict Case-I prime cutoff places the inherited coordinate above s - 1.

theorem MathlibNt.SieveTheory.eventually_caseI_strict_pointwise_packet_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (S : BoundingSieve) (N : ℕ) (s : ℝ), 2 ≤ N → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → 2 ≤ s → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; CaseIErrorEnvelopeTransport S H N D d σ s → (∀ p ∈ S.prodPrimes.primeFactors, Nat.Prime p) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry S.prodPrimes.primeFactors D Dmin σ s ∧ (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) ∧ (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) ∧ CaseIErrorEnvelopeTransport S H N D d σ s ∧ (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) ∧ (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) ∧ ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)

All strict-successor pointwise premises except the genuinely missing error transport are generated uniformly from parity and large-D carrier geometry.

theorem MathlibNt.SieveTheory.eventually_caseI_strict_pointwise_packet (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), 2 ≤ N → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → 2 ≤ s → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; CaseIErrorEnvelopeTransport S H N D d σ s → (∀ p ∈ S.prodPrimes.primeFactors, Nat.Prime p) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry S.prodPrimes.primeFactors D Dmin σ s ∧ (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) ∧ (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) ∧ CaseIErrorEnvelopeTransport S H N D d σ s ∧ (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) ∧ (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) ∧ ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)

Compatibility specialization of the pointwise packet uniform in S.

theorem MathlibNt.SieveTheory.lemma14_4_caseI_final_producer_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {C C145 K d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 < C) (hC145 : 0 < C145) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), 2 ≤ N → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s → SwitchingPrinciple.SuzukiLemma144Equation1410.GlobalDepthLemma144InductionHypothesis (suzukiActualT S) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) 2 C K Δ (N - 1) Dmin → suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + sigma12InheritedBudget S H N D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s

Callable strict Case-I producer. Every carrierwise geometry and error transport family is internal. Besides the standard Case-I domain data, its pointwise recursive inputs are exactly the named quotient-coordinate edge and the global depth induction hypothesis.