ConditionalCompanion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.conditional_companion_positive_of_structure line 12
Source documentation
Full positive alternative, including uniform positivity, a ratio asymptotic, and comparison with the number of distinct totients.
```
theorem conditional_companion_positive_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    {d k : ℕ} (hk : 1≤k) (hd : IsTotient d) (hseed : k*d<ell d)
    (hppt : PPTBoundedFiberPropagation d) :
    ∃ cMinus cPlus : ℝ, 0<cMinus ∧ 0<cPlus ∧
      (∀ s∈Set.Ico (0 : ℝ) 1, cMinus≤A (fk k) s ∧ A (fk k) s≤cPlus) ∧
      Tendsto (fun x => N k x/(tupleNormalization x*A (fk k) (theta x))) atTop (nhds 1) ∧
      ∀ᶠ x : ℝ in atTop, (cMinus/cPlus)*V x≤N k x ∧ N k x≤V x := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.V

theorem OAI.TotientAsymptotic.conditional_companion_theorem_of_structure line 47

Source documentation

The manuscript's weighted companion theorem, conditional only on the named published analytic inputs and the published full-fiber propagation.

theorem conditional_companion_theorem_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    (hppt : ∀ d : ℕ, IsTotient d → PPTBoundedFiberPropagation d) (k : ℕ) (hk : 1≤k) :
    TendstoUniformlyOn (fun H => AH H (fk k)) (A (fk k)) atTop (Set.Ico (0 : ℝ) 1) ∧
    Tendsto (fun x => normalizedCount (N k) x-A (fk k) (theta x)) atTop (nhds 0) ∧
    ((∃ d : ℕ, IsTotient d ∧ k*d<ell d) →
      ∃ cMinus cPlus : ℝ, 0<cMinus ∧ 0<cPlus ∧
        (∀ s∈Set.Ico (0 : ℝ) 1, cMinus≤A (fk k) s ∧ A (fk k) s≤cPlus) ∧
        Tendsto (fun x => N k x/(tupleNormalization x*A (fk k) (theta x))) atTop (nhds 1) ∧
        ∀ᶠ x : ℝ in atTop, (cMinus/cPlus)*V x≤N k x ∧ N k x≤V x) ∧
…

theorem OAI.TotientAsymptotic.companion_seeds_one_two line 69
Source documentation
The published explicit least-preimage calculation supplies the two unconditional-in-k positive cases singled out by the manuscript.
```
theorem companion_seeds_one_two
    (hseed : IsTotient (2^18*257)) (hmin : ell (2^18*257)=135268352) :
    ∀ k∈({1,2} : Finset ℕ), ∃ d : ℕ, IsTotient d ∧ k*d<ell d := by
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell
theorem OAI.TotientAsymptotic.conditional_companion_one_two_of_structure line 81
Source documentation
The final assertion for k=1 and k=2, using exactly the published finite least-preimage calculation cited in seeds_one_two_of_published_least_preimage.
```
theorem conditional_companion_one_two_of_structure (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    (hppt : ∀ d : ℕ, IsTotient d → PPTBoundedFiberPropagation d)
    (hseed : IsTotient (2^18*257)) (hmin : ell (2^18*257)=135268352) :
    ∀ k∈({1,2} : Finset ℕ), ∃ c : ℝ, 0<c ∧
      ∀ s∈Set.Ico (0 : ℝ) 1, c≤A (fk k) s := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.fk
theorem OAI.TotientAsymptotic.conditional_companion_positive line 100
Source documentation
The original published-input interface remains available.
```
theorem conditional_companion_positive (hscale : FordScaleBounds)
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    {d k : ℕ} (hk : 1≤k) (hd : IsTotient d) (hseed : k*d<ell d)
    (hppt : PPTBoundedFiberPropagation d) :
    ∃ cMinus cPlus : ℝ, 0<cMinus ∧ 0<cPlus ∧
      (∀ s∈Set.Ico (0 : ℝ) 1, cMinus≤A (fk k) s ∧ A (fk k) s≤cPlus) ∧
      Tendsto (fun x => N k x/(tupleNormalization x*A (fk k) (theta x))) atTop (nhds 1) ∧
      ∀ᶠ x : ℝ in atTop, (cMinus/cPlus)*V x≤N k x ∧ N k x≤V x :=
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.conditional_companion_theorem line 112
theorem OAI.TotientAsymptotic.conditional_companion_one_two line 128