StrictCofactorSplit.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact totient factorization at a strict gap in the ordered prime list.

lemma OAI.TotientAsymptotic.fordCofactor_largest_exact line 11
theorem OAI.TotientAsymptotic.strict_cofactor_coprime line 15
theorem OAI.TotientAsymptotic.strict_cofactor_totient line 32
theorem OAI.TotientAsymptotic.first_failed_row_totient line 41
lemma OAI.TotientAsymptotic.fordCofactor_comp line 50
lemma OAI.TotientAsymptotic.fordCofactor_length line 56
theorem OAI.TotientAsymptotic.strict_gap_residual_totient line 63
Source documentation
The leading prime may have either totient-extension branch. After its removal, the strict boundary still gives an exact residual-value encoding.
```
theorem strict_gap_residual_totient {n j : ℕ} (hn : 0 < n) (hj : 0 < j)
    (hjlen : j ≤ n.primeFactorsList.length)
    (hgap : fordPrime n j < fordPrime n (j-1)) :
    (n/fordPrime n 0).totient = (fordCofactor n j).totient *
      (∏ i : Fin (j-1), fordPrime n (i.val+1)).totient := by
…
```
Mentions: OAI.TotientAsymptotic.fordPrime, OAI.TotientAsymptotic.fordCofactor