The Binary Totient Series

The cost of clearing a rational denominator

Clearing a denominator changes the multiplier as well as the fraction. The example $4(5/12)=5/3$ illustrates the divisibility relation below for arbitrary reduced fractions; no totient identity is needed.

Indeed, the hypothesis makes $Hcx=Hca/b$ integral. Since $gcd(a,b)=1$, it follows that $b\mid Hc$, hence $b/H\mid c$. Writing $c=(b/H)t$ also gives $Hcx=ta$; this equality is also proved in Lean (Erdos249257.AdelicHeightObstruction.scalarLocalization_integer_eq_mul_num). If $c\ne 0$, the divisibility implies $|c|\ge b/H$. The nonzero hypothesis is essential for this size bound: $c=0$ has reduced denominator one and satisfies the divisibility, but has no positive size cost. The lemma is about multiplication of one rational value, not arbitrary cancellations among several values.

A related elementary inequality compares a positive numerator with its denominator. If $a>0$, $r\ge 0$, $n\ge 1$, $2^r\mid a$, and $a/b<2/(2^n-1)$, then

Lean proves this Mersenne instance (Erdos249257.AdelicHeightObstruction.positiveRat_mersenne_height) and the version with a general positive denominator parameter (positiveRat_numDivisor_mul_lt_two_mul_den). Positivity of $a$ is what turns numerator divisibility into a lower bound; it cannot be omitted.

The accompanying linear-algebra statement has a one-dimensional quotient. Let $V,W$ be vector spaces over $\mathbb{Q}$, let $\mathrm{ev}:V\to \mathbb{Q}$ and $\mathrm{\Lambda }:V\to W$ be linear, and suppose $\ker \mathrm{ev}\subseteq \ker \mathrm{\Lambda }$. Choose $e\in V$ with $\mathrm{ev}(e)=1$. Then, for every $v\in V$,

This is factorisation through the scalar quotient $V/\ker \mathrm{ev}$ (Erdos249257.AdelicHeightObstruction.linearDescender_eq_smul_eval). A surjection onto a higher-dimensional space would imply only a linear factorisation through that space, not multiplication by one fixed vector.

The denominator calculations use two lemmas proved in Lean (Erdos249257.RationalDenominatorSurvival.divisor_dvd_divInt_den, survivingDivisor_dvd_scaled_divInt_den). For integers $a$ and $D\ge 1$, the reduced denominator of $a/D$ is $D/gcd(|a|,D)$. Hence a divisor of $D$ coprime to $a$ divides the reduced denominator. Coprimality is sufficient, not necessary: $2/8=1/4$ retains the divisor $2$. More generally, if $C$ is a positive divisor of $D$, $gcd(C,a)=1$, and $h\ge 0$ is an integer, then $C/gcd(C,h)$ divides the reduced denominator of $ha/D$. At $h=0$ this assertion retains only the divisor one.

For a nonzero multiplier, a lower bound for $b/H$ therefore gives a lower bound for its absolute value. For an integer $t\ge 5$, the product estimate $2^{\lfloor t/2\rfloor }\le \prod _{p\in {\mathcal{P}}_t}(2^p-1)$ (upperHalfMersenneProduct_lower_bound) can be used when that product is shown to divide $b/H$. Neither the product estimate nor the scalar lemma proves a quadratic growth law for arbitrary approximation schemes.

The finite Farey exclusion for $S$ is a separate use of reduced denominators. Its certified interval contains no rational whose reduced denominator is at most

(tsum_totient_div_pow_two_ne_ratCast_of_den_le_79639646646701375323355774875831053). That numerical exclusion requires the interval and Farey calculation; it is not a consequence of the scalar lemma alone.