Mathlib v4.30 source proposition Nat.eq_or_eq_of_totient_eq_totient

Identifier: F:ml430-nat-eq-or-eq-of-totient-eq-totient-d4d154c7
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

∀ {a b : ℕ}, a ∣ b → a.totient = b.totient → a = b ∨ 2 * a = b

Dependencies

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

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

Evidence

kernel-Nat.eq_or_eq_of_totient_eq_totient

Kind: kernel-term
Status: checked

Supports: a | b -> totient a = totient b -> a = b \/ 2*a = b, with the whole rendered type pinned.

Checker command

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

Evidence notes

The grep pins the WHOLE rendered type. Verified both directions with /usr/bin/grep -Fc explicitly (not the interactive-shell ugrep): the real name gives count 1; a fabricated name (`eq_or_eq_of_totient_eq_totient_nonexistent_xyz`) gives count 0 (the tool prints nothing and exits nonzero for an absent name), so `test ... -ge 1` fails as required. Exactly one name is passed, since `nat_theorem_inventory` silently keeps only the LAST of several name arguments (measured 2026-08-30).

engine-Nat.totient_mul_cofactor_bound

Kind: kernel-term
Status: checked

Supports: The multiplier-tracking bound this theorem is built from: for cofactor k >= 2, either totient(a*k) >= 2*totient(a) outright, or k = 2 and totient(a*k) = totient(a) exactly.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- totient_mul_cofactor_bound 2>/dev/null | tr '\t' ' ' | grep -Fc 'Nat.totient_mul_cofactor_bound')" -ge 1

Evidence notes

By well-founded induction on the cofactor k, reusing the prime-peeling chain of Nat.totient_dvd_totient_mul plus a single-prime-step case analysis (coprime vs dividing, per Nat.coprime_or_dvd_of_prime) showing the per-step multiplier can be exactly 1 only in the coprime branch at q = 2. `totient_mul_cofactor_bound` does not collide with any other declared name as a substring (unlike `totient_dvd_totient_mul`/`totient_dvd_totient_mul_prime`), so a name-only grep is sufficient here -- verified by inspecting nat_theorem_inventory's output directly.

instances-eq_or_eq_of_totient_eq_totient

Kind: exhaustive-enumeration
Status: checked

Supports: Holds for every 0 <= a, b < 60; both hypotheses are load-bearing; the second disjunct is reachable ONLY at cofactor k = b/a = 2, and only when a is odd; no chain of length >= 2 ever reaches it.

Checker command

python3 scripts/tests/check-totient-dvd-chain-numerics.py

Evidence notes

Checks 3 through 6. Check 3 is the bound lemma itself (k>=2 -> totient(a*k)>=2*totient(a) OR (k=2 AND equal)), with check 3N showing the k>=2 guard is load-bearing (k=1 always gives equality, which is neither disjunct as stated for k!=2). Check 4 is the target statement itself with both hypotheses' controls (4N-dvd, 4N-eq) shown load-bearing. Check 5 confirms every genuine '2a=b' witness has a ODD -- a even would force the single prime step's multiplier to 2, not 1. Check 6 confirms the second disjunct is reachable ONLY at cofactor k=2 (checked over every witness with 1<=a,b<60), which is the numeric form of the well-founded induction's own case analysis (depth-2-or-more chains always land in the first disjunct).

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_dvd_chain (totient-dvd-chain 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 well-founded induction tracking the totient multiplier along a prime-peeling chain, per ADR-0668 -- it does NOT reconstruct Mathlib's proof, whose route was not consulted.",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.eq_or_eq_of_totient_eq_totient`",
      "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 multiplier-tracking well-founded induction, not Mathlib's)."
    }
  ]
}