noncomputable def Hex.Nat.choose : Nat → Nat → Nat

Binomial coefficients on natural numbers, defined by the Pascal recursion.

Equations

• Hex.Nat.choose x✝ 0 = 1
• Hex.Nat.choose 0 n.succ = 0
• Hex.Nat.choose n.succ k.succ = Hex.Nat.choose n k + Hex.Nat.choose n (k + 1)

@[simp]

theorem Hex.Nat.choose_zero_right (n : Nat) : choose n 0 = 1

choose n 0 = 1: the zeroth column of Pascal's triangle.

@[simp]

theorem Hex.Nat.choose_zero_succ (k : Nat) : choose 0 (k + 1) = 0

choose 0 (k + 1) = 0: nontrivial entries vanish in the top row of Pascal's triangle.

@[simp]

theorem Hex.Nat.choose_succ_succ (n k : Nat) : choose (n + 1) (k + 1) = choose n k + choose n (k + 1)

Pascal's recurrence: choose (n + 1) (k + 1) = choose n k + choose n (k + 1).

theorem Hex.Nat.choose_eq_zero_of_lt {n k : Nat} (h : n < k) : choose n k = 0

Entries past the diagonal of Pascal's triangle vanish: choose n k = 0 whenever n < k.

@[simp]

theorem Hex.Nat.choose_self (n : Nat) : choose n n = 1

The diagonal of Pascal's triangle is constantly one: choose n n = 1.

def Hex.Nat.Prime (p : Nat) : Prop

A natural number is prime when it is at least 2 and its positive divisors are trivial. This is the Mathlib-free prime predicate used by downstream modular arithmetic layers.

Equations

• Hex.Nat.Prime p = (2 ≤ p ∧ ∀ (m : Nat), m ∣ p → m = 1 ∨ m = p)

theorem Hex.Nat.Prime.two_le {p : Nat} (hp : Prime p) : 2 ≤ p

Every prime is at least 2.

theorem Hex.Nat.Prime.one_lt {p : Nat} (hp : Prime p) : 1 < p

Every prime is greater than 1.

theorem Hex.Nat.Prime.pos {p : Nat} (hp : Prime p) : 0 < p

Every prime is positive.

theorem Hex.Nat.Prime.ne_zero {p : Nat} (hp : Prime p) : p ≠ 0

Every prime is nonzero.

theorem Hex.Nat.Prime.ne_one {p : Nat} (hp : Prime p) : p ≠ 1

Every prime is distinct from 1.

theorem Hex.Nat.Prime.coprime_of_not_dvd {p a : Nat} (hp : Prime p) (ha : ¬p ∣ a) : p.Coprime a

Build coprimality between a prime and a number it does not divide.

theorem Hex.Nat.Prime.dvd_mul {p a b : Nat} (hp : Prime p) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b

Euclid's lemma for the local prime predicate, in iff form: a prime divides a product iff it divides one of the factors.

theorem Hex.Nat.Prime.dvd_of_dvd_pow {p a k : Nat} (hp : Prime p) (h : p ∣ a ^ k) : p ∣ a

A prime that divides a power divides its base.

theorem Hex.Nat.prime_iff_forall_lt (p : Nat) : Prime p ↔ 2 ≤ p ∧ ∀ (m : Nat), m < p → 2 ≤ m → ¬m ∣ p

Primality as a bounded search: for p ≥ 2, having only trivial divisors is the same as having no divisor strictly between 1 and p. The point of the restatement is that the right-hand side quantifies over a finite range, which is what makes the decidability instance below possible.

theorem Hex.Nat.prime_iff_forall_le_sqrt (p : Nat) : Prime p ↔ 2 ≤ p ∧ ∀ (m : Nat), m < p.sqrt + 1 → 2 ≤ m → ¬m ∣ p

Primality by trial division up to the square root.

A composite has a nontrivial divisor d with d * d ≤ p: of any factor pair p = d * e, the smaller one qualifies. Bounding the search that way is what makes decide practical. The linear form above needs p steps, which is fine for a two-digit modulus and is not fine beyond that — decide on Prime 3221 takes about fourteen seconds through it, and the primes that turn up in p ^ n - 1 for the committed Conway table run to five digits. This form needs about √p steps instead.

theorem Hex.Nat.prime_of_bounded (p b : Nat) (hp : 2 ≤ p) (hb : p < (b + 1) * (b + 1)) (h : ∀ (m : Nat), m < b + 1 → 2 ≤ m → ¬m ∣ p) : Prime p

Primality from trial division up to a caller-supplied bound.

prime_iff_forall_le_sqrt cannot drive a decide: core's Nat.sqrt is defined by well-founded recursion, so the kernel will not evaluate it. Taking the bound as data instead keeps everything the kernel sees structural. The caller supplies b with p < (b + 1) ^ 2, which decide checks in one multiplication, and then only b + 1 divisors have to be ruled out rather than p of them.

The Decidable instance now routes through isPrimeTrial (defined below), so decide is O (√p) remainder tests; this lemma remains for callers that already hold an explicit bound and want the divisor obligations alone.

theorem Hex.Nat.succ_mul_choose_succ (n k : Nat) : (k + 1) * choose n (k + 1) = (n - k) * choose n k

Within-row multiplicative recurrence (k+1) · choose n (k+1) = (n - k) · choose n k. Reading it left to right computes one Pascal row in a single linear pass, which is what binom exploits.

theorem Hex.Nat.choose_symm {n k : Nat} : k ≤ n → choose n (n - k) = choose n k

Pascal's triangle is symmetric across each row: choose n (n - k) = choose n k for k ≤ n. This is the symmetry the min-optimized binom fold exploits to walk the shorter half of the row.

def Hex.Nat.binom (n k : Nat) : Nat

Linear-time binomial coefficient.

Hex.Nat.binom walks a single Pascal row from choose n 0 = 1 using the multiplicative recurrence Hex.Nat.succ_mul_choose_succ, folding over the shorter half min k (n - k) of the row using Hex.Nat.choose_symm. It therefore costs O(min k (n - k)) natural-number operations. The proof-facing Hex.Nat.choose is the exponential Pascal recursion; the forward correctness theorem binom_eq_choose, registered with @[csimp], makes compiled callers use this linear fold.

Equations

• Hex.Nat.binom n k = if n < k then 0 else List.foldl (fun (acc i : Nat) => acc * (n - i) / (i + 1)) 1 (List.range (min k (n - k)))

theorem Hex.Nat.binom_eq_choose (n k : Nat) : binom n k = choose n k

The min-optimized binom fold agrees with the proof-facing Pascal choose.

@[csimp]

theorem Hex.Nat.choose_eq_binom : choose = binom

@[simp]

theorem Hex.Nat.binom_zero_right (n : Nat) : binom n 0 = 1

Choosing 0 elements always gives 1.

@[simp]

theorem Hex.Nat.binom_zero_succ (k : Nat) : binom 0 (k + 1) = 0

Choosing k + 1 elements from 0 is impossible.

theorem Hex.Nat.binom_eq_zero_of_lt {n k : Nat} (h : n < k) : binom n k = 0

The binomial coefficient binom n k vanishes when n < k.

theorem Hex.Nat.choose_le_succ_left {k j : Nat} (h : 2 * (j + 1) ≤ k) : choose k j ≤ choose k (j + 1)

The row of Pascal's triangle increases up to its centre: choose k j ≤ choose k (j + 1) while 2 * (j + 1) ≤ k.

theorem Hex.Nat.choose_le_center (k fuel j : Nat) : k / 2 - j ≤ fuel → 2 * j ≤ k → choose k j ≤ choose k (k / 2)

Everything on the left half of a row is at most the central entry: choose k j ≤ choose k (k / 2) for 2 * j ≤ k.

theorem Hex.Nat.centralChoose_le_succ (m : Nat) : choose m (m / 2) ≤ choose (m + 1) ((m + 1) / 2)

The central binomial coefficient increases by one row at a time.

theorem Hex.Nat.centralChoose_mono {k n : Nat} (h : k ≤ n) : choose k (k / 2) ≤ choose n (n / 2)

The central binomial coefficient is monotone in the row index.

theorem Hex.Nat.choose_prime_dvd {p k : Nat} (hp : Prime p) (hk : 0 < k) (hk' : k < p) : p ∣ choose p k

Every nontrivial binomial coefficient in the pth row of Pascal's triangle is divisible by p when p is prime. This is the binomial-divisibility fact used to erase the middle terms in add_pow_prime_mod.

theorem Hex.Nat.add_pow_prime_mod {p : Nat} (hp : Prime p) (a b : Nat) : (a + b) ^ p % p = (a ^ p + b ^ p) % p

Freshman's dream modulo a prime: (a + b)^p is congruent to a^p + b^p modulo p, because all middle binomial terms vanish.

theorem Hex.Nat.pow_prime_mod {p : Nat} (hp : Prime p) (a : Nat) : a ^ p % p = a % p

Fermat's little theorem in the residue form used by downstream modular arithmetic code: raising a natural number to the pth power preserves its residue modulo a prime p.

def Hex.Nat.isPrimeTrialAux (n : Nat) : Nat → Nat → Bool

Balanced trial division over the 2 ^ fuel candidates starting at k. The square guard is checked before descending into an interval, so no candidate with n < k * k is tested. Splitting the interval in half keeps kernel reduction depth logarithmic in the number of candidate divisors. This helper is a primality test only with a range large enough to cover every small divisor; isPrimeTrial is the supported entry point.

Equations

• Hex.Nat.isPrimeTrialAux n 0 x✝ = if n < x✝ * x✝ then true else decide (n % x✝ ≠ 0)
• Hex.Nat.isPrimeTrialAux n fuel.succ x✝ = if n < x✝ * x✝ then true else Hex.Nat.isPrimeTrialAux n fuel x✝ && Hex.Nat.isPrimeTrialAux n fuel (x✝ + 2 ^ fuel)

def Hex.Nat.isPrimeTrial (n : Nat) : Bool

Executable bounded trial-division primality test. Returns true exactly when n is prime. Candidate divisors start at 2, and the loop stops before testing the first k whose square exceeds n; thus it performs at most ⌊√n⌋ - 1 remainder tests. It remains pure Lean so emitted primality certificates can be replayed by the kernel without Mathlib, native_decide, or a fixed prime table.

Equations

• Hex.Nat.isPrimeTrial n = (decide (2 ≤ n) && Hex.Nat.isPrimeTrialAux n (n.log2 + 1) 2)

theorem Hex.Nat.exists_trial_divisor {n m : Nat} (hn : 0 < n) (hm : m ∣ n) (hm1 : m ≠ 1) (hmn : m ≠ n) : ∃ (d : Nat), 2 ≤ d ∧ d * d ≤ n ∧ d ∣ n

A nontrivial divisor yields a divisor at most the square root: of m and its cofactor, the smaller one squares to at most n.

theorem Hex.Nat.isPrimeTrial_isPrime {n : Nat} (h : isPrimeTrial n = true) : Prime n

Soundness of the trial-division primality test against the Mathlib-free Hex.Nat.Prime predicate. It turns a successful runtime test into explicit primality evidence without relying on a hardcoded prime table.

theorem Hex.Nat.isPrimeTrial_of_prime {n : Nat} (h : Prime n) : isPrimeTrial n = true

Completeness of the executable trial-division test: every project-local prime witness makes the Boolean checker return true.

@[instance_reducible]

instance Hex.Nat.instDecidablePrime (p : Nat) : Decidable (Prime p)

Primality is decidable through isPrimeTrial, so decide costs O (√p) remainder tests with kernel reduction depth logarithmic in the candidate count.

Equations

• Hex.Nat.instDecidablePrime p = decidable_of_iff (Hex.Nat.isPrimeTrial p = true) ⋯

theorem Hex.Nat.exists_prime_dvd {d : Nat} (h : 2 ≤ d) : ∃ (q : Nat), Prime q ∧ q ∣ d

Every natural number at least 2 has a prime divisor.

theorem Hex.Nat.exists_prime_le_sqrt {n : Nat} (h : 2 ≤ n) (hcomp : ¬Prime n) : ∃ (p : Nat), Prime p ∧ p ∣ n ∧ p * p ≤ n

A composite number has a prime divisor whose square is at most the number. This is the small-divisor witness the Pocklington argument finishes with.