Every natural number at least 2 has a prime divisor

Identifier: F:nat-exists-prime-dvd
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural number m with 2 <= m there is a p with 2 <= p, every divisor of p equal to 1 or to p, and p dividing m. Here `p is prime` is spelled out inline rather than named, because the prelude has no Prime predicate.

Formal statement

theorem Nat.exists_prime_dvd : ((m : AxNat) -> ((hm : AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) m) -> Exists.{1} AxNat (fun (p : AxNat) => And (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) p) (((d : AxNat) -> ((hd : AxNat.dvd d p) -> Or (Eq.{1} AxNat d (AxNat.succ AxNat.zero)) (Eq.{1} AxNat d p))))) (AxNat.dvd p m))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

11 direct dependencies 5 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.exists_prime_dvd

Kind: kernel-term
Status: checked

Supports: For every m with 2 <= m there is a prime p dividing m, with primality spelled inline.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- exists_prime_dvd 2>/dev/null | tr '\t' ' ' | grep -Fc 'Nat.exists_prime_dvd 4 ((x0 : AxNat) -> ((x1 : AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x0) -> Exists.{1} AxNat (fun (x2 : AxNat) => And (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x2) (((x3 : AxNat) -> ((x4 : AxNat.dvd x3 x2) -> Or (Eq.{1} AxNat x3 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x3 x2))))) (AxNat.dvd x2 x0))))')" -ge 1

Evidence notes

The grep pins the WHOLE rendered type, not the name, and that is the point of this row rather than tidiness. `build_nat_prelude` admits the declaration through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type -- so the kernel already refuses a false theorem, and a witness that was not prime (say `m` itself at `m = 6`) never gets in. What the kernel cannot notice is a statement that is WEAKER than intended. Measured 2026-08-17: spelling the primality lower bound `1 <= p` instead of `2 <= p` still type-checks, still admits, still passes every existing test including axiom-freedom and the determinism count -- and is satisfied by `p = 1`, whose only divisor is 1, which closes nothing. That mutation was run: exactly one test died (`every_number_at_least_two_has_a_prime_divisor`, which compares the admitted type against an independently built term) and 288 others passed. A name-only grep would have survived it, so this command greps the `AxNat.succ (AxNat.succ AxNat.zero)` bound inside the existential explicitly. `nat_theorem_inventory` additionally exits non-zero for a name that does not exist.

footprint-Nat.exists_prime_dvd

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty, so this theorem's footprint is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`theorem_axiom_footprint` reports `nat Nat.exists_prime_dvd 0` and `integer Nat.exists_prime_dvd 0` directly, along with 0 for the three supporting theorems `le_of_dvd`, `two_le_succ_or_eq_one` and `least_divisor_search`. `nat_axiom_inventory` bounds all of them at once: the enumeration reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, and a theorem cannot depend on a trusted declaration the environment does not contain. Counting `Declaration::Axiom` alone would NOT suffice -- `Opaque` has no proof body and `Quotient` admits `Quot.sound` -- so the enumeration covers all three, and the flag makes the exit status depend on the finding rather than on the run completing.

Provenance

{
  "date": "2026-08-17",
  "established_by": "axeyum-lean-kernel nat_prelude::primes (nat-prime-divisor lane)",
  "source": "the second of the two ingredients `F:nat-exists-prime-gt` was recorded as missing; statement authored here",
  "prior_art": [
    {
      "who": "Euclid",
      "what": "Elements, Book VII, Proposition 31",
      "year": -300,
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}