A prime is its own least prime factor

Identifier: F:nat-min-fac-eq-self-of-prime
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural n, if n is prime -- spelled inline as 2 <= n and every divisor of n is 1 or n, this kernel having no Prime predicate -- then Nat.minFac n = n. With its converse Nat.prime_of_min_fac_eq_self (2 <= n and minFac n = n imply n prime) this turns the propositional primality condition into a COMPUTABLE Bool test, `Nat.beq (Nat.minFac n) n`, which is what a product or a count over the primes needs in order to be a fold rather than a choice. This is a kernel term with an empty axiom footprint.

Formal statement

theorem Nat.min_fac_eq_self_of_prime : ((x0 : AxNat) -> ((x1 : And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x0) (((x1 : AxNat) -> ((x2 : AxNat.dvd x1 x0) -> Or (Eq.{1} AxNat x1 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x1 x0))))) -> Eq.{1} AxNat (AxNat.minFac x0) x0))

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

kernel-Nat.min_fac_eq_self_of_prime

Kind: kernel-term
Status: checked

Supports: Nat.min_fac_eq_self_of_prime is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example nat_theorem_inventory -- min_fac_eq_self_of_prime 2>/dev/null | grep -Fc 'Nat.min_fac_eq_self_of_prime	4	((x0 : AxNat) -> ((x1 : And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x0) (((x1 : AxNat) -> ((x2 : AxNat.dvd x1 x0) -> Or (Eq.{1} AxNat x1 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x1 x0))))) -> Eq.{1} AxNat (AxNat.minFac x0) x0))')" -ge 1

Evidence notes

No new induction: `Nat.min_fac_dvd` gives `minFac n | n` (its `2 <= n` premise is primality's left conjunct), primality's right conjunct turns that into `minFac n = 1 \/ minFac n = n`, and `Or.resolve_left` discharges the left disjunct by transporting `Nat.min_fac_two_le` along `minFac n = 1` into `Le 2 1`, refuted by `Nat.not_succ_le_self`.

statement-Nat.min_fac_eq_self_of_prime

Kind: kernel-term
Status: checked

Supports: The DECLARED type is `forall n, prime_condition n -> minFac n = n`, and not the trivial `minFac n = minFac n`; the converse's declared type concludes primality of `n`, not of `minFac n` (which is Nat.min_fac_prime, already in the environment).

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- nat_prelude::primorial_tests:: --test-threads=4

Evidence notes

Both directions take a Prop-typed hypothesis, so the test compares the DECLARED type against a hand-rebuilt statement rather than inferring an application: `pi_fv` abstracts the bound variable to a de Bruijn index, so the fresh-fvar id is irrelevant to the comparison. Each direction carries a negative control naming a specific weaker statement of the same shape -- without the converse's control the test would pass for a duplicate of `Nat.min_fac_prime`.

footprint-Nat.min_fac_eq_self_of_prime

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- the Nat environment admits no trusted declaration

Checker command

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

Evidence notes

`the_primorial_shelf_is_admitted_and_axiom_free` asserts `Environment::contains` FIRST for each name and only then an empty `Kernel::axiom_footprint`, because the footprint of an absent name is also empty. `nat_axiom_inventory` bounds it independently over the whole trusted surface.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane chebyshev-pi",
  "source": "theorem name and canonical type read directly via nat_theorem_inventory, which prints render_lean of the admitted type."
}