Mathlib v4.30 source proposition Nat.totient_gcd_mul_totient_mul

Identifier: F:ml430-nat-totient-gcd-mul-totient-mul-2e1d13c7
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The proposition declared as `Nat.totient_gcd_mul_totient_mul` in the pinned Mathlib v4.30 source.

Formal statement

∀ (a b : ℕ), (a.gcd b).totient * (a * b).totient = a.totient * b.totient * a.gcd b

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

kernel-Nat.totient_gcd_mul_totient_mul

Kind: kernel-term
Status: checked

Supports: totient(gcd a b) * totient(a*b) = totient(a) * totient(b) * gcd(a,b), with the whole rendered type pinned.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- totient_gcd_mul_totient_mul 2>/dev/null | tr '\t' ' ' | grep -Fc 'Nat.totient_gcd_mul_totient_mul 2 ((x0 : AxNat) -> ((x1 : AxNat) -> Eq.{1} AxNat (AxNat.mul (AxNat.totient (AxNat.gcd x0 x1)) (AxNat.totient (AxNat.mul x0 x1))) (AxNat.mul (AxNat.mul (AxNat.totient x0) (AxNat.totient x1)) (AxNat.gcd x0 x1))))')" -ge 1

Evidence notes

The grep pins the WHOLE rendered type, not just the name. Verified both directions with /usr/bin/grep -Fc explicitly (not the interactive-shell ugrep): the real name gives count 1, and `totient_gcd_mul_totient_mul_nonexistent_xyz` makes `nat_theorem_inventory` exit 1 with `error: no Nat theorem matches ...` (an absent theorem is a failed check, not an empty report), so `test ... -ge 1` fails as required either way. `nat_theorem_inventory` keeps only the LAST of several name arguments if more than one is passed (measured 2026-08-30), so exactly one name is passed here.

engine-Nat.totient_gcd_mul_aux

Kind: kernel-term
Status: checked

Supports: The measure-generalized family this theorem is a one-line application of: forall d a b, gcd a b = d -> totient d * totient(a*b) = totient a * totient b * d, by strong (well-founded) induction on the gcd value d.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- totient_gcd_mul_aux 2>/dev/null | tr '\t' ' ' | grep -Fc 'Nat.totient_gcd_mul_aux 4 ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : Eq.{1} AxNat (AxNat.gcd x1 x2) x0) -> Eq.{1} AxNat (AxNat.mul (AxNat.totient x0) (AxNat.totient (AxNat.mul x1 x2))) (AxNat.mul (AxNat.mul (AxNat.totient x1) (AxNat.totient x2)) x0)))))')" -ge 1

Evidence notes

Peels one prime q | gcd(a,b) at a time via Nat.exists_prime_dvd, writing a = q*a1, b = q*b1 (Nat.dvd elimination); Nat.gcd_mul_right gives gcd(a,b) = q*gcd(a1,b1), a strictly smaller measure. The prime's status against a1 and b1 is decided INDEPENDENTLY by Nat.coprime_or_dvd_of_prime (not against gcd(a1,b1) or a1*b1 directly), so Nat.euclid_lemma is never consulted on this route -- narrower than ADR-0668's own sketch, which reduces to an eps-identity where Euclid's lemma is load-bearing. Each of the four resulting leaves (dvd/dvd, dvd/coprime, coprime/dvd, coprime/coprime) reduces via Nat.totient_mul_of_dvd / Nat.totient_mul_of_coprime, and the whole identity collapses to a fixed six-factor commutative-monoid rearrangement checked once in a shared helper.

instances-Nat.totient_gcd_mul_totient_mul

Kind: exhaustive-enumeration
Status: checked

Supports: The identity holds over 0<=a,b<26 (check 8), collapses to the already-landed totient_mul_of_coprime at coprime pairs (check 8A), and is STRICTLY STRONGER than plain multiplicativity at 53 non-coprime pairs with 1<=a,b<=12 (check 8N).

Checker command

python3 scripts/tests/check-totient-prime-power-numerics.py

Evidence notes

Checks 8, 8A, 8N, 8E, 8EN, 8G, 8R in the pre-existing suite (re-run, not inherited) cover this target's ADR-0668 sketch route (an eps-identity where Euclid IS load-bearing, check 8EN). The kernel proof landed on a NARROWER route that decides a1/b1 independently and never needs Euclid's lemma; both are correct, and the numeric checks bound the statement itself rather than either specific route.

footprint-nat-prelude

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty, which bounds this theorem.

Checker command

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

Evidence notes

`--require-axiom-free` exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is non-empty. Measured 2026-08-30: `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, exit 0.

Provenance

{
  "date": "2026-08-30",
  "established_by": "axeyum-lean-kernel nat_prelude::totient_gcd_mul (totient-gcd-mul lane)",
  "source": "statement was extracted from Mathlib v4.30.0 (statement-only, no proof value exposed); the proof here is constructed independently in this kernel via a strong induction on gcd(a,b) that peels one prime at a time, per ADR-0668 -- it does NOT reconstruct Mathlib's Euler-product proof, which this kernel cannot state (no List/Finset/product type for unique factorisation).",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.totient_gcd_mul_totient_mul`",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "year": 2026,
      "attribution": "the proposition was read from the pinned statement-only inventory; the proof term and tactic trace were not consulted, and the proof actually built here uses a different route (a prime-peeling strong induction on the gcd value, not the Euler product)."
    }
  ]
}