Uniform Case-I carrier error transport #
The Claim-14.6 source threshold is chosen before D, N, and s. Enlarging
one natural global cutoff puts every ceiling quotient above that threshold and
also supplies the low-strip logarithmic estimate used by the full coordinate
transport theorem.
The carrierwise error-envelope comparison consumed by the Case-I successor.
Equations
- MathlibNt.SieveTheory.CaseIErrorEnvelopeTransport S H N D d σ s = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, 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)
Instances For
Inspect dependencies
MathlibNt.SieveTheory.CaseIErrorEnvelopeTransport · compiled type and proof/definition references.
After one global quotient cutoff, full coordinate antitonicity gives the Case-I error transport simultaneously at every carrier. The two coordinate hypotheses are exactly the geometric facts supplied by the Case-I pointwise packet: the inherited point is in the predecessor parity domain and the recursive point is below the quotient's source endpoint.
Inspect dependencies
MathlibNt.SieveTheory.exists_caseI_errorEnvelope_transport_quotient_cutoff_uniform_in_S · compiled type and proof/definition references.
Compatibility specialization of the sieve-uniform quotient cutoff.
Inspect dependencies
MathlibNt.SieveTheory.exists_caseI_errorEnvelope_transport_quotient_cutoff · compiled type and proof/definition references.
A square global cutoff puts every Case-I carrier quotient above the threshold.
Inspect dependencies
MathlibNt.SieveTheory.caseI_carrier_quotient_scale · compiled type and proof/definition references.
Eventual form: the square global cutoff and p < D^(1/s), s ≥ 2
put every natural ceiling quotient above the internal Claim-14.6 threshold.
The cutoff precedes N and s.
Inspect dependencies
MathlibNt.SieveTheory.eventually_caseI_errorEnvelope_transport_uniform_in_S · compiled type and proof/definition references.
Compatibility specialization of the sieve-uniform eventual theorem.
Inspect dependencies
MathlibNt.SieveTheory.eventually_caseI_errorEnvelope_transport_uniform · compiled type and proof/definition references.