Eventual Jordan-Cototient Records

Abstract

Eventual strict Jordan-cototient records are exactly one and the even naturals.

Definition 1.1 (The real-parameter Jordan totient).

$$\forall k\in \mathbb{R},n\in \mathbb{N},J\left(k,n\right)=\mathrm{val}{\left(n\right)}^k\cdot \prod _{p\in \mathrm{primeFactors}\left(n\right)}(1-\mathrm{val}{\left(p\right)}^{-k})$$

Formalization. D5/S3/Factorization/JordanCototientRecordLimitInfinity.J (✓ std3).

Source. Repository-derived.

Commentary.

For a real parameter k and a natural number n, J(k,n) is exactly n^k times the product over p in primeFactors(n) of 1-p^(-k). The function val shown in the formula is the coercion from natural numbers to real numbers. This is the definition stated in the OEIS A004277 comment.

Definition 1.2 (The Jordan cototient).

$$\forall k\in \mathbb{R},n\in \mathbb{N},\mathrm{CoJ}\left(k,n\right)=\mathrm{val}{\left(n\right)}^k-J\left(k,n\right)$$

Formalization. D5/S3/Factorization/JordanCototientRecordLimitInfinity.CoJ (✓ std3).

Source. Repository-derived.

Commentary.

For real k and natural n, CoJ(k,n) is defined exactly as the real power n^k minus J(k,n), matching the OEIS source comment.

Definition 1.3 (Strict records among positive predecessors).

$$\forall k\in \mathbb{R},n\in \mathbb{N},\mathrm{StrictRecord}\left(k,n\right)\iff \left(\forall m\in \mathbb{N},1\le m\Rightarrow \left(m<n\Rightarrow \mathrm{CoJ}\left(k,m\right)<\mathrm{CoJ}\left(k,n\right)\right)\right)$$

Formalization. D5/S3/Factorization/JordanCototientRecordLimitInfinity.StrictRecord (✓ std3).

Source. Repository-derived.

Commentary.

StrictRecord(k,n) means that every natural predecessor m with 1 <= m and m < n has strictly smaller Jordan cototient at the same parameter k.

Lemma 1.4 (The minimum-prime-factor lower bound).

$$\forall k\in \mathbb{R},n\in \mathbb{N},0<k\Rightarrow \left(1<n\Rightarrow \mathrm{val}{\left(Nat.div\left(n,\mathrm{minFac}\left(n\right)\right)\right)}^k\le \mathrm{CoJ}\left(k,n\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For k > 0 and n > 1, the k-th real power of the natural Euclidean quotient Nat.div(n,minFac(n)) is at most CoJ(k,n). Nat.div is the integer quotient before the displayed real coercion; it is not field division. The proof singles out the minFac(n) term in the finite Euler product.

Lemma 1.5 (The minimum-prime-factor upper bound).

$$\forall k\in \mathbb{R},n\in \mathbb{N},0<k\Rightarrow \left(1<n\Rightarrow \mathrm{CoJ}\left(k,n\right)\le \mathrm{val}\left(\mathrm{card}\left(\mathrm{primeFactors}\left(n\right)\right)\right)\cdot \mathrm{val}{\left(Nat.div\left(n,\mathrm{minFac}\left(n\right)\right)\right)}^k\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_upper_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For k > 0 and n > 1, CoJ(k,n) is at most the real coercion of the number of distinct prime factors times the k-th power of Nat.div(n,minFac(n)). Nat.div again denotes natural Euclidean division. A finite-product union bound compares every reciprocal prime scale with the minimum-prime-factor scale.

Lemma 1.6 (Prime inputs have cototient one).

$$\forall p\in \mathbb{N},k\in \mathbb{R},\mathrm{Prime}\left(p\right)\Rightarrow \mathrm{CoJ}\left(k,p\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_prime (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every natural prime p has CoJ(k,p)=1 for every real k. This bind-only evaluation is consumed by the two-versus-three tie in not_strictRecord_three.

Lemma 1.7 (The cototient of one vanishes).

$$\forall k\in \mathbb{R},\mathrm{CoJ}\left(k,1\right)=0$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real k, CoJ(k,1)=0 because primeFactors(1) is empty. This bind-only evaluation supplies the m=1 predecessor case in the even record theorem.

Theorem 1.8 (Every positive even input is eventually a strict record).

$$\forall n\in \mathbb{N},1\le n\Rightarrow \left(\mathrm{Even}\left(n\right)\Rightarrow \left(\exists K\in \mathbb{R},\forall k\in \mathbb{R},k>K\Rightarrow \mathrm{StrictRecord}\left(k,n\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.eventual_strictRecord_of_even (✓ std3). ∎

Source. Repository-derived.

Commentary.

If n is positive and even, there is a real threshold K after which n is a strict record. The proof combines the two public bounds with the strict base gap m/minFac(m) <= m/2 < n/2 and real exponential domination. Each slash in this prose is real division after coercion, whereas the Lean bounds themselves use the named Nat.div quotient.

Theorem 1.9 (Odd inputs at least five eventually lose to their predecessor).

$$\forall n\in \mathbb{N},5\le n\Rightarrow \left(\left(\neg \mathrm{Even}\left(n\right)\right)\Rightarrow \left(\exists K\in \mathbb{R},\forall k\in \mathbb{R},k>K\Rightarrow \mathrm{CoJ}\left(k,n\right)<\mathrm{CoJ}\left(k,Nat.sub\left(n,1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.eventual_loses_to_predecessor_of_odd (✓ std3). ∎

Source. Repository-derived.

Commentary.

If n is odd and at least five, a real threshold K makes CoJ(k,n) smaller than CoJ(k,Nat.sub(n,1)) for every k > K. Nat.sub is truncated natural subtraction. The proof uses n/minFac(n) <= n/3 < (n-1)/2 and the same real exponential-domination lemma.

Lemma 1.10 (Three is never a strict record).

$$\forall k\in \mathbb{R},\neg \mathrm{StrictRecord}\left(k,3\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.not_strictRecord_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real k, three is not a strict record: the preceding prime-value lemma gives CoJ(k,2)=CoJ(k,3)=1, so the required strict predecessor inequality is impossible.

Theorem 1.11 (The eventual record set is one together with the even naturals).

$$\forall n\in \mathbb{N},1\le n\Rightarrow \left((\exists K\in \mathbb{R},\forall k\in \mathbb{R},k>K\Rightarrow \mathrm{StrictRecord}\left(k,n\right))\iff (n=1\vee \mathrm{Even}\left(n\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/JordanCototientRecordLimitInfinity.a004277_eventual_record_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n >= 1, there exists a real threshold K after which n is always a strict Jordan-cototient record exactly when n=1 or n is even. The threshold is chosen separately for each n; no uniform threshold over all even inputs is asserted.

The forward direction excludes three by the prime tie and every odd n >= 5 by its eventual loss to Nat.sub(n,1). The reverse direction is vacuous at one and uses the live even-input theorem otherwise. Thus the two-sided min-factor estimates remain on the proof path to the final characterization.

References

• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.CoJ
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.J
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.StrictRecord
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.a004277_eventual_record_iff
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_lower_bound
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_one
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_prime
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.coJ_upper_bound
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.eventual_loses_to_predecessor_of_odd
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.eventual_strictRecord_of_even
• Truth anchor: D5/S3/Factorization/JordanCototientRecordLimitInfinity.not_strictRecord_three