BandExtraction.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The finite-union and geometric-tail argument behind the manuscript's ford-bands estimate. Only Ford's explicitly stated Theorems 10 and 16 remain hypotheses; the summation and the passage to model bands are proved.

def OAI.TotientAsymptotic.modelBandsCondition line 17
def OAI.TotientAsymptotic.extractedStructureCondition line 22
def OAI.TotientAsymptotic.positiveFordBandsCondition line 25
lemma OAI.TotientAsymptotic.totientCount_nonneg line 28
lemma OAI.TotientAsymptotic.preimageExceptionCount_forall_le line 32
lemma OAI.TotientAsymptotic.preimageExceptionCount_and_le line 48
lemma OAI.TotientAsymptotic.backward_exponential_sum_le line 63
lemma OAI.TotientAsymptotic.linear_exponential_le line 98
def OAI.TotientAsymptotic.bandExceptionFactor line 118
lemma OAI.TotientAsymptotic.bandExceptionFactor_pos line 120
lemma OAI.TotientAsymptotic.band_error_sum_le line 125
lemma OAI.TotientAsymptotic.ford10_single_band_estimate line 146
theorem OAI.TotientAsymptotic.positive_ford_bands_exception_bound line 196
Source documentation
Theorem 10 gives the geometric-tail estimate for existing positive coordinates. Theorem 16 supplies the missing-coordinate estimate below.
```
theorem positive_ford_bands_exception_bound (hford : FordTheorem10Input) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ P : ℕ, 0 < P → P < m x →
      preimageExceptionCount x (positiveFordBandsCondition x P) ≤
        C * V x * Real.exp (-(P : ℝ)/2500) := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.preimageExceptionCount, OAI.TotientAsymptotic.positiveFordBandsCondition, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.extracted_structure_exception_bound line 225
Source documentation
Bands and the unclamped simplex hold for every preimage outside one exceptional set with exponential decay in P.
```
theorem extracted_structure_exception_bound
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ P : ℕ, 0 < P → P < m x →
      preimageExceptionCount x (extractedStructureCondition x P) ≤
        C * V x * Real.exp (-(P : ℝ)/2500) := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.preimageExceptionCount, OAI.TotientAsymptotic.extractedStructureCondition, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.model_bands_exception_bound line 264
Source documentation
Missing and nonpositive coordinates are included via Theorem 16, before the positive-coordinate estimate from Theorem 10 is applied.
```
theorem model_bands_exception_bound (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ P : ℕ, 0 < P → P < m x →
      preimageExceptionCount x (modelBandsCondition x P) ≤
        C * V x * Real.exp (-(P : ℝ)/2500) := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.preimageExceptionCount, OAI.TotientAsymptotic.modelBandsCondition, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.extracted_structure_eventually line 276
Source documentation
The manuscript's order of quantifiers: choose P, then take x large. Here every P≥1 works, with absolute constants independent of P.
```
theorem extracted_structure_eventually
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) :
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧ ∀ P : ℕ, 0 < P → ∀ᶠ x : ℝ in atTop,
      P < m x ∧ preimageExceptionCount x (extractedStructureCondition x P) ≤
        C * V x * Real.exp (-c * P) := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.preimageExceptionCount, OAI.TotientAsymptotic.extractedStructureCondition, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.extracted_structure_all_preimages line 293
Source documentation
The exceptional set removes values with any failing preimage, so the surviving values satisfy the full retained range simultaneously in every positive preimage.
```
theorem extracted_structure_all_preimages
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) :
    ∃ C c : ℝ, 0 < C ∧ 0 < c ∧ ∀ P : ℕ, 0 < P → ∀ᶠ x : ℝ in atTop,
      ∃ E : Finset ℕ, P < m x ∧ (E.card : ℝ) ≤ C * V x * Real.exp (-c * P) ∧
        ∀ v ∈ Finset.Icc 1 ⌊x⌋₊, v ∉ E → ∀ n : ℕ, 0 < n → n.totient = v →
          extractedStructureCondition x P n := by
…
```
Mentions: OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.extractedStructureCondition