FiberPropagationInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Discharge the fixed-seed fiber propagation input by pruning the actual normal candidate family. Seed one also supplies Ford's lower counting bound.

theorem OAI.TotientAsymptotic.full_fiber_scale_family line 14
theorem OAI.TotientAsymptotic.pptBoundedFiberPropagation line 33
Source documentation
Pollack–Pomerance–Treviño, Lemma 4.1, in the bounded-ratio form used here.
```
theorem pptBoundedFiberPropagation (d : ℕ) (hd : IsTotient d) :
    PPTBoundedFiberPropagation d :=
…
```
Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.PPTBoundedFiberPropagation
theorem OAI.TotientAsymptotic.ford_scale_lower line 37
theorem OAI.TotientAsymptotic.fordScaleBounds line 43
Source documentation
Ford's counting scale, with both bounds proved from the finite families.
```
theorem fordScaleBounds : FordScaleBounds := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds