PNT-normalized port envelope controlled by the logarithmic gap
ProvedErdos390.WholePaper.bankPaperCanonical_weightedPNTEnvelope_le_logGap_compactanalytic-number-theoryerdos-390erdos390-source-construction
Let be a regular relative mesh with , , nonzero cutoff , and scale separation, so its canonical prime partition is defined. Fix a ratio . Assume further and that exceeds the uniform reciprocal-prime-sum cutoff. Let and let be a canonical tangent prime. Write for the current ratio-cell lower endpoint, for its exponent-band upper endpoint, for the source port numerator envelope, and for the uniform reciprocal-sum constant. Let be the source PNT denominator for the current cell, and let be its natural prime label. Then
This is the normalized pointwise traffic estimate used in distributed tangent budgets.
Preamble
import Definitions.Def_erdos390_analytic_compact_goals_005
Formal statement
theorem Erdos390.WholePaper.bankPaperCanonical_weightedPNTEnvelope_le_logGap_compact : Erdos390.AnalyticCompactBatch005Goal001 := by sorry
Source