A prime has exactly two divisors, so the Bool primality predicate answers true

`Nat.isPrime n` unfolds to `beq (countRange (fun j => beq (n % (j+1)) 0) n) 2` -- a divisor COUNT, not a trial division. The proof shows that count is exactly two for a prime: `1 | n` supplies the index 0, `Nat.mod_self` supplies the index n-1, and every index between is refuted by primality's own divisor clause (`c = 1` by `succ_ne_zero`, `c = n` by `lt_irrefl` against the range hypothesis). The count is assembled by peeling the last index with `countRange_succ_of_true` and the first with `countRange_split` at 1, leaving `countRange_eq_zero_of_all_false` for the middle: 2 = 1 + 0 + 1. The rendered type is matched in full because the weakening that matters here is invisible to a name check: `Nat.isPrime` is universe- and argument-compatible with any `AxNat -> Bool`, so a checker that read only the name would be satisfied by a theorem about a different predicate entirely.

`nat_axiom_inventory` bounds the footprint by enumerating the whole trusted surface: a theorem cannot depend on a trusted declaration the environment does not contain. All three kinds are covered -- counting `Declaration::Axiom` alone would not suffice, because `Opaque` has no proof body and `Quotient` admits `Quot.sound`. The module's own test `the_prime_counting_shelf_is_admitted_and_axiom_free` additionally asserts `Environment::contains` BEFORE reading the footprint, because `axiom_footprint` returns an empty set for a name that was never declared.