Scaling.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The common-endpoint argument from Proposition mass in the manuscript. CommonEndpointComparison names an internal estimate still requiring proof; it is not classified as a published input. The proof below shows precisely how that estimate and Ford's published order bounds yield regular variation, without any phase-continuity assumption.

def OAI.TotientAsymptotic.pairedNormalized line 19
def OAI.TotientAsymptotic.CommonEndpointComparison line 22
lemma OAI.TotientAsymptotic.paired_normalized_sub_tendsto line 26
theorem OAI.TotientAsymptotic.inverse_scaling_of_internal_comparison line 47
Source documentation
The reciprocal form is convenient because Ford's lower bound controls its denominator at the larger endpoint directly.
```
theorem inverse_scaling_of_internal_comparison {c : ℝ} (hc : 0 < c)
    (hford : FordScaleBounds) (hcommon : CommonEndpointComparison c) :
    Tendsto (fun x => V (x/c) / V x) atTop (nhds (1/c)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.CommonEndpointComparison, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.scaling_of_internal_comparison line 83
Source documentation
The endpoint comparison yields the manuscript's fixed-scale conclusion. The unproved internal comparison remains explicit in this reduction theorem.
```
theorem scaling_of_internal_comparison {c : ℝ} (hc : 0 < c)
    (hford : FordScaleBounds) (hcommon : CommonEndpointComparison c) :
    Tendsto (fun x => V (c*x) / V x) atTop (nhds c) := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.CommonEndpointComparison, OAI.TotientAsymptotic.V