Euler's totient is multiplicative on coprime arguments

The grep pins the WHOLE rendered type, not the name. That matters here in a specific way: 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 two such neighbours that both type-check. Weakening the hypothesis from `Eq (gcd x0 x1) 1` to anything satisfiable-by-more-pairs would make the theorem unsound and is pinned by quoting the hypothesis verbatim; transposing the conclusion to `mul (totient x1) (totient x0)` is a genuinely different theorem (the Rust test asserts `!def_eq` between the two at free variables) and is pinned by quoting the factor order. `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.

Twenty checks, each paired with a negative control the script asserts must GENUINELY fail; any failure exits 1 naming the check. The script separates the four steps of this theorem's proof and reports which of them need the hypothesis: `MapsInto`, the pointwise predicate identity and the Fubini factorization hold at all 26 non-coprime pairs, while the permutation step fails at 26 of 26. Written and run BEFORE any of the Rust, because an earlier traced plan for this same argument asserted the row-major identity was coprimality-independent and 'verified numerically', and it is false at every one of those 26 pairs. Numeric claims in a plan are re-derived here, never inherited. The kernel-side instantiation is `totient_mul_of_coprime_computes_at_coprime_pairs_with_a_non_coprime_control` (nat_prelude_tests.rs), which requires every count to COMPUTE at (2,3) and (3,4) and asserts `!def_eq` for the two sides at m = n = 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.