StructuralInput.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Minimal structural inputs from Ford, The distribution of totients, arXiv:1104.3264v2 (14 July 2013), Theorems 10 and 16.

The exceptional sets count values with some failing preimage, as in the convention preceding Theorem 10, p. 5. Consequently every preimage of a value outside the exceptional set satisfies the property. Ford's coordinates in (4.2), p. 17, are clamped double logarithms. Theorem 16, (6.1)--(6.2), p. 29, also supplies the terminal lower bound that allows removing this clamp.

The band center below is Ford's B*rho^i*(1-i/m), not the phase-dependent bandScale in Basic.lean. Passing between these two centers is an additional analytic step, governed by the manuscript's equation alpha-comparison.

def OAI.TotientAsymptotic.fordPrime line 27
Source documentation
Prime factors with multiplicity, largest first, padded by 1.
```
def fordPrime (n i : ℕ) : ℕ := (n.primeFactorsList.reverse[i]?).getD 1
```
def OAI.TotientAsymptotic.primeDoubleLog line 29
def OAI.TotientAsymptotic.fordPrimeCoordinate line 31
def OAI.TotientAsymptotic.fordBandScale line 33
def OAI.TotientAsymptotic.fordBandCondition line 36
def OAI.TotientAsymptotic.fordPositiveBandCondition line 42
Source documentation
Theorem 10 is used only on positive coordinates, where the indicated prime exists and its raw and clamped double logarithms agree. Missing or nonpositive coordinates are handled separately by Theorem 16.
```
def fordPositiveBandCondition (x η : ℝ) (i n : ℕ) : Prop :=
…
```
def OAI.TotientAsymptotic.preimageExceptionValues line 45
def OAI.TotientAsymptotic.preimageExceptionCount line 50
def OAI.TotientAsymptotic.FordTheorem10Input line 57
Source documentation
Ford Theorem 10(a),(b), restricted to positive coordinates, the indices and the errors needed here. This does not assign a value to the raw double logarithm of a missing prime. The endpoint i=m is omitted because the application uses i≤m-P<m.
```
def FordTheorem10Input : Prop :=
…
```
def OAI.TotientAsymptotic.fordSimplexCoordinate line 68
def OAI.TotientAsymptotic.rawSimplexCoordinate line 71
def OAI.TotientAsymptotic.fordSimplexCondition line 76
Source documentation
The needed consequence of membership in Ford's S_L(xi). It retains the last adjacent inequality with coefficient 1 and coordinate ordering.
```
def fordSimplexCondition (x : ℝ) (Ψ n : ℕ) : Prop :=
…
```
def OAI.TotientAsymptotic.FordTheorem16Input line 87
Source documentation
Ford Theorem 16, with its uniform exp(-Psi^2/4) exceptional-value bound.
```
def FordTheorem16Input : Prop :=
…
```
lemma OAI.TotientAsymptotic.fordSimplexCondition_coordinate_pos line 93
def OAI.TotientAsymptotic.extractedSimplexCondition line 99
Source documentation
The weaker, unclamped simplex used in equation ford-simplex of the manuscript.
```
def extractedSimplexCondition (x : ℝ) (Ψ n : ℕ) : Prop :=
…
```
lemma OAI.TotientAsymptotic.outside_preimageExceptions_iff line 106
lemma OAI.TotientAsymptotic.preimageExceptionCount_mono line 119
lemma OAI.TotientAsymptotic.fordPrimeCoordinate_eq_raw_of_pos line 129
lemma OAI.TotientAsymptotic.fordBandScale_pos line 136
lemma OAI.TotientAsymptotic.fordBandCondition_removes_clamp line 143
lemma OAI.TotientAsymptotic.fordSimplexCondition_implies_extracted line 158
theorem OAI.TotientAsymptotic.extracted_simplex_exception_bound line 201
Source documentation
Theorem 16 controls the weaker unclamped condition without changing its exceptional-set constant or its quantifier over all preimages.
```
theorem extracted_simplex_exception_bound (hford : FordTheorem16Input) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
      ∀ Ψ : ℕ, Ψ < m x →
        preimageExceptionCount x (extractedSimplexCondition x Ψ) ≤
          C * V x * Real.exp (-(Ψ : ℝ)^2/4) := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.preimageExceptionCount, OAI.TotientAsymptotic.extractedSimplexCondition, OAI.TotientAsymptotic.V