Euler's totient at a prime power

The grep pins the WHOLE rendered type, not the name. The kernel re-derives the type from the proof term and so refuses a FALSE theorem, but it cannot notice a statement that is weaker or transposed, and this one has both kinds of neighbour. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Fc` consumes the whole pipe with the count then tested, rather than `grep -q`, which would SIGPIPE the producer under pipefail. Measured 2026-08-30: `nat_theorem_inventory` consumes only ONE name argument -- given two names in either order it reports on the LAST one only -- so exactly one is passed here. The primality hypothesis is quoted verbatim in its inline spelling (`2 <= p` and the divisor dichotomy) because this prelude has no `Prime` predicate to name, and because dropping or weakening it makes the statement FALSE rather than merely weaker -- the Rust test pins that with a composite base-4 control where the two sides compute to 2 and 3 and are asserted NOT def_eq. The exponent is pinned as `AxNat.succ x1` on the left and `x1` on the right: writing both as `x1` would be the k = 0 case, which is false (totient(1) = 1, not 1 - 1 = 0).

Thirty-four checks, each negative control asserted to GENUINELY fail. Checks 5 and 5N are this fact's; 5M pins the multiplicative form the induction actually builds and 5S the closing Nat.sub step, and 6/6N pin the prime step totient(p*x) = eps(x)*totient(x) that the three remaining ml430 totient mirrors need. The kernel-side instantiation is `totient_prime_pow_computes_at_two_cubed_and_three_squared_with_a_composite_control` (nat_prelude_tests.rs): 2^3 and 3^2 with every value required to COMPUTE, plus the composite base-4 control. Magnitudes are held at 8, 9 and 4 deliberately -- prelude numerals are unary, so a test at 2^10 would cost more than the prelude build.

`--require-axiom-free` exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient -- counting `Axiom` alone would not suffice, since `Opaque` has no proof body and `Quotient` admits `Quot.sound`) is non-empty, and errors rather than passing silently for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty nat surface bounds every declaration in it, including this one. This is a whole-prelude bound, not a per-declaration measurement.