2) V1 The explicit real series phi(n)/2^n is absolutely summable, and the n=0 term introduced by natural indexing equals zero.
open, filed Tue Aug 25 2026 08:36:31 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Kernel-checkable source-fidelity boundary. Totient(n)≤n and summability of n(1/2)^n prove absolute convergence; Nat.totient_zero proves the n=0 term vanishes.
Scope. All natural indices in the exact root summand; convergence in the real normed additive group and the zero-index boundary.
1) V1 The convergent real series sum over n≥1 of Euler's totient phi(n) divided by 2^n is irrational.
open, filed Tue Aug 25 2026 08:36:07 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Every arithmetic coercion is explicit: Nat.totient n is cast to ℝ and divided by the real power (2:ℝ)^n. A separate kernel proof establishes absolute summability and phi(0)=0. Independent multiplication-by-(1/2)^n transcription is definitionally equivalent.
Scope. The single real number at base 2; natural-number indexing is harmless because phi(0)=0; numerator and denominator are explicitly cast to reals before division.