Mathlib v4.30 source proposition Nat.coprime_iff_isRelPrime

Identifier: F:ml430-nat-coprime-iff-isrelprime-0c08eb25
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

∀ {m n : ℕ}, m.Coprime n ↔ IsRelPrime m n

Dependencies

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

5 direct dependencies 0 direct dependents

Evidence

kernel-Nat.coprime_iff_isRelPrime

Kind: kernel-term
Status: checked

Supports: m.Coprime n <-> IsRelPrime m n, where IsRelPrime m n := forall d, d|m -> d|n -> d=1 is a new Definition (rel_prime.rs), Mathlib's generic `forall d, d|x -> d|y -> IsUnit d` specialized to Nat's only unit, 1

Checker command

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

Evidence notes

`build_nat_prelude` admits `Nat.IsRelPrime` (a `Definition`) and `Nat.coprime_iff_isRelPrime` (a `Theorem`) through the trusted `Kernel::add_declaration` gate. Route, mirroring Mathlib's own proof at `Mathlib/Data/Nat/GCD/Basic.lean:218-220` (`simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ..., isUnit_iff_dvd_one]`) without needing any of Mathlib's `IsUnit`/`Monoid` machinery, since `Nat`'s only unit is spelled directly as `= 1`: forward (`gcd m n = 1 -> IsRelPrime m n`) takes an arbitrary `d | m` and `d | n`, combines them with `dvd_gcd` into `d | gcd m n`, transports along the hypothesis to `d | 1`, and closes with `eq_one_of_dvd_one`; backward (`IsRelPrime m n -> gcd m n = 1`) applies the hypothesis directly at `d := gcd m n`, discharged by `gcd_dvd_left`/`gcd_dvd_right` -- no case analysis in either direction, and neither direction unfolds `Nat.gcd`'s own recursion (which carries `Quot.sound`), only its divisibility characterisation. `nat_theorem_inventory` exits non-zero for a name that does not exist, and the `grep -c` requires the admitted declaration to be printed.

footprint-Nat.coprime_iff_isRelPrime

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 [].

compute-Nat.coprime_iff_isRelPrime-mp-mpr

Kind: kernel-term
Status: checked

Supports: the forward direction genuinely produces IsRelPrime and the backward direction genuinely produces gcd m n = 1, not merely that the folded Iff type-checks

Checker command

cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::coprime_iff_is_rel_prime_round_trips_at_a_concrete_coprime_pair

Evidence notes

At m=3, n=5 (gcd 3 5 computes to 1 by def_eq): `.mp` applied to the computed proof of `gcd 3 5 = 1` infers a type defeq to `IsRelPrime 3 5`, and round-tripping that result through `.mpr` lands back on a type defeq to `Eq (gcd 3 5) 1` -- the same swap-detecting technique as the existing `coprime_two_left` test, which fails if `mp`/`mpr` were passed to `iff_intro` in the wrong order.

compute-Nat.IsRelPrime-refuted-non-coprime

Kind: kernel-term
Status: checked

Supports: IsRelPrime m n is false of a genuine non-coprime pair, discriminating it from a predicate that is accidentally true of every pair

Checker command

cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::is_rel_prime_is_refuted_at_a_concrete_non_coprime_pair

Evidence notes

A genuine kernel-checked proof of `Not (IsRelPrime 4 6)`: gcd 4 6 computes to 2, so applying an assumed `IsRelPrime 4 6` at d := gcd 4 6 (via gcd_dvd_left/gcd_dvd_right) forces `Eq 2 1`, refuted by succ_injective + succ_ne_zero. This is the discriminating negative control for the predicate itself (not merely for the theorem): a mis-stated IsRelPrime that dropped, say, the `d|n` premise would let a wrong pair through this exact shape of construction, and (4,6) is chosen because 2 genuinely divides both.

Provenance

{
  "date": "2026-08-29",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane nat-minfac-relprime",
  "source": "statement-only extraction of `Nat.coprime_iff_isRelPrime` from Mathlib v4.30.0 (see prior_art), independently proved here as `Nat.coprime_iff_isRelPrime` (`crates/axeyum-lean-kernel/src/nat_prelude/rel_prime.rs`) and admitted through `Kernel::add_declaration`",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.coprime_iff_isRelPrime`, and the definition `IsRelPrime` it uses (`Mathlib/Algebra/Divisibility/Units.lean:150`, `def IsRelPrime [Monoid α] (x y : α) : Prop := forall d, d|x -> d|y -> IsUnit d`)",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "year": 2026,
      "attribution": "the proposition was read from the pinned statement-only inventory; the mirror flip was verified honest by reading Mathlib's own source for `IsRelPrime` at the pinned commit -- Mathlib DEFINES it as `forall d, d|x -> d|y -> IsUnit d`, and for Nat's only unit `1` this specializes to exactly `Nat.IsRelPrime m n := forall d, d|m -> d|n -> d=1`, the Definition landed here. Our proof of the Iff is independently constructed."
    }
  ]
}