PPTSquareWitness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Prune squares in a selected bad preimage and in its totient. Injectivity of the chosen preimages, rather than of the totient values, preserves the cardinality bound required by the PPT construction.

theorem OAI.TotientAsymptotic.ppt_square_witness_count line 17
lemma OAI.TotientAsymptotic.ppt_seed_squarefreeAbove line 58
Source documentation
Multiplication by a seed with no prime above the cutoff preserves the squarefree-above-cutoff property. This supplies the actual left product condition after pruning squares from the candidate totient.
```
lemma ppt_seed_squarefreeAbove {d m : ℕ} {Z : ℝ} (hd : d ≠ 0)
    (hseed : (largestPrimeFactor d : ℝ) ≤ Z) (hsq : SquarefreeAbove m Z) :
    SquarefreeAbove (d*m) Z := by
…
```
Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.SquarefreeAbove