Multiplying a modulus by one of its own divisors scales the totient exactly

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. Two neighbours matter specifically here. Transposing the right-hand side to `mul x1 (AxNat.totient x0)` or to `mul (AxNat.totient x1) x0` gives different theorems that agree at many numeral pairs; the factor order is quoted verbatim, and the Rust test asserts `!def_eq` against the transposed form at FREE variables, where the two genuinely separate. Weakening the hypothesis `AxNat.dvd x1 x0` to anything satisfied by more pairs would make the theorem unsound, and it too is quoted verbatim.

Thirty-four checks, each positive one exhaustive over its stated range and each negative control asserted to GENUINELY fail; any failure exits 1 naming the check. Checks 4 and 4N are this fact's; 3 and 3N isolate the gcd bridge that is the ONLY place the divisibility hypothesis is spent, and 2/2N the block-counting step, which needs no hypothesis at all. Written and run BEFORE any Rust, because an earlier traced plan in this same area asserted an identity was coprimality-independent and 'verified numerically', and it is false at 26 of 26 non-coprime pairs. Numeric claims are re-derived here, never inherited. The kernel-side instantiation is `totient_mul_of_dvd_computes_at_closed_dividing_pairs_with_a_non_dividing_control` (nat_prelude_tests.rs), which supplies REAL `dvd_mul` witnesses at (4,2) and (6,3), requires every count to COMPUTE, and asserts `!def_eq` for the two sides at the non-dividing (1,2).

`--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.