Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiProposition118SourcePairingFinal

Final source-pairing closure for Suzuki Proposition 11.8 #

The genuine source pairing is continuous on every [2,M] and has zero right derivative at every point of [2,M), including the lower endpoint 2 and the kink 3. The right-derivative constant theorem therefore proves conservation on the whole closed interval in one step. Decay at infinity then forces the boundary scalar, and hence Suzuki's B, to vanish.

The genuine source pairing has zero right derivative throughout [2,∞), including both exceptional endpoints required by the one-sided argument.