Mathlib v4.30 source proposition Nat.totient_coprime_totient_iff

Identifier: F:ml430-nat-totient-coprime-totient-iff-3932cf83
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

∀ (m n : ℕ), m.totient.Coprime n.totient ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Dependencies

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

18 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.totient_coprime_totient_iff

Kind: kernel-term
Status: checked

Supports: Iff (gcd (totient m) (totient n) = 1) ((m=1 or m=2) or (n=1 or n=2))

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- totient_coprime_totient_iff 2>/dev/null | grep -Ec '^Nat\.totient_coprime_totient_iff[[:space:]]')" -ge 1

Evidence notes

`build_nat_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the constructed proof term against the stated type. Route (`nat_prelude/totient_lemmas.rs::declare_totient_coprime_totient_iff`): `mpr` is unconditional composition -- whichever disjunct holds forces one side's totient to `one` (`totient_eq_one_iff`), and `gcd 1 x = 1` / `gcd x 1 = 1` regardless of the other argument (`coprime_one_left_iff`/`coprime_one_right_iff`, unconditional). `mp` splits `m` via `trichotomy(two, m)`: `m<2` splits again into `m=0` (rewrites the hypothesis to `gcd zero (totient n) = 1`, giving `totient n = 1` via `gcd_zero_left`, then `totient_eq_one_iff.mp`) and `m=1` (immediate); `m=2` is immediate; `2<m` gives `Even (totient m)` via `totient_even`, then splits `n` the same way, with `n=0` bridging through `gcd_comm`+`gcd_zero_left` (this prelude has no named `gcd_zero_right`) to `totient m = 1`, contradicting `Even (totient m)` via `even_not_odd`; the hard case `2<m, 2<n` gives `Even (totient m)`, `Even (totient n)`, and derives `False`: each is divisible by 2 (`succ_mul`/`one_mul` turn the `Even` witness `k+k` into `mul two k`), `dvd_gcd` forces `2 | gcd (totient m)(totient n) = 1`, `eq_one_of_dvd_one` gives `Eq two one`, refuted by transporting `le_refl two` along it and peeling one `succ` to `not_succ_le_zero`. `nat_theorem_inventory` exits non-zero for a name that does not exist, and the `grep -c` requires the admitted declaration to be printed (confirmed 1 for the real name, 0 for a fabricated one).

footprint-Nat.totient_coprime_totient_iff

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

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

Evidence notes

`nat_axiom_inventory --require-axiom-free nat` enumerates the built Nat environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration. A theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds every individual theorem's footprint by [].

Provenance

{
  "date": "2026-08-30",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane totient-mult-finish (building on totient-even-finish)",
  "source": "statement-only extraction of the Mathlib proposition from Mathlib v4.30.0 (see prior_art), independently proved here as `Nat.totient_coprime_totient_iff` and admitted through `Kernel::add_declaration`",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.totient_coprime_totient_iff`",
      "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"
    }
  ]
}