English
minFacAux is an auxiliary function that, given a positive number n and a natural fuel, finds the smallest factor of n by inspecting candidate divisors k in increasing order starting from k, using a square bound k^2 and a divisibility test; if n < k^2 then n is prime with respect to k, if k divides n then k is the smallest factor, otherwise continue with k.succ.
Русский
minFacAux — вспомогательная функция, которая, имея положительное число n и лимит по шагам (fuel), ищет наименьший делитель n перебором кандидатов k в порядке возрастания, проверяя условие k^2 и делимость; если n < k^2, то n — простое относительно k; если k делит n, то наименьший делитель — k; иначе продолжаем с k+1.
LaTeX
$$$$\operatorname{minFacAux}(n):\mathbb{N}\to\mathrm{PosNum}\to \mathrm{PosNum} \quad\text{with} \quad \begin{cases} (0,\;k) \mapsto n \\[2mm] (fuel+1, k) \mapsto \begin{cases} n, & n < k^{\!2} \\ k^{\!1}, & k^{\!1} \mid n \\ \operatorname{minFacAux}(n)(fuel)(k+1), & \text{otherwise} \end{cases} \end{cases}$$$$
Lean4
/-- Auxiliary function for computing the smallest prime factor of a `PosNum`. Unlike
`Nat.minFacAux`, we use a natural number `fuel` variable that is set to an upper bound on the
number of iterations. It is initialized to the number `n` we are determining primality for. Even
though this is exponential in the input (since it is a `Nat`, not a `Num`), it will get lazily
evaluated during kernel reduction, so we will only require about `sqrt n` unfoldings, for the
`sqrt n` iterations of the loop. -/
def minFacAux (n : PosNum) : ℕ → PosNum → PosNum
| 0, _ => n
| fuel + 1, k => if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else minFacAux n fuel k.succ
