Uniform Case-II quotient error transport

The Case-II carrier is the cubic strip, with upper endpoint D^(1/3) and outer endpoint sourceSigma D d. One cutoff, chosen before D, N, and the Case-II coordinate s, puts every ceiling quotient above the internal Claim-14.6 threshold. The moving-coordinate theorem then puts the recursive coordinate below the quotient's own source endpoint.

def MathlibNt.SieveTheory.CaseIIErrorEnvelopeTransport (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D : ℕ) (d : ℝ) : Prop

Carrierwise error transport required by the cubic Case-II pointwise induction contract.

Equations

• MathlibNt.SieveTheory.CaseIIErrorEnvelopeTransport S H N D d = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 3)⌉₊) D (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 3, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)

theorem MathlibNt.SieveTheory.caseII_cubic_carrier_quotient_scale (S : BoundingSieve) {D Dmin : ℕ} {d : ℝ} (hDmin : 2 ≤ Dmin) (hD : Dmin ^ 2 ≤ D) : SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 3)⌉₊) D Dmin (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 3

theorem MathlibNt.SieveTheory.eventually_caseII_errorEnvelope_transport_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (S : BoundingSieve) (N : ℕ) (s : ℝ), Odd N → 1 < s → s ≤ 3 → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 3)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 3, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) → CaseIIErrorEnvelopeTransport S H N D d

Uniform Case-II transport with the cutoff selected before the varying bounding sieve. The only local input is the parity-domain packet already required by the rounded endpoint. Coordinate ordering follows from natural ceiling division; the recursive upper endpoint follows uniformly from the moving quotient-source theorem; and Claim 14.6(i) is generated internally at each quotient source endpoint.

The threshold is independent of S, N, and every s ∈ (1,3].

theorem MathlibNt.SieveTheory.eventually_caseII_errorEnvelope_transport_uniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), Odd N → 1 < s → s ≤ 3 → (∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 3)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 3, SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1)) → CaseIIErrorEnvelopeTransport S H N D d

Compatibility wrapper for the original sieve-first Case-II transport API.