Is the binary Lambert series sum phi(n)/2^n irrational?
Statements and boundaries are copied from the corpus record. Registry status: not_registered; the claim registry does not carry these declarations and kernel checking them does not promote them into reviewed public claims
For every e >= 1, the complete dyadic totient kernel through level e has rational span dimension 2^e + 1.
This does not prove irrationality of the totient series.
The rational span of the full dyadic totient kernel is not finite-dimensional.
The declaration is kernel-checked locally, but full-kernel infinite-dimensionality is not an independent contribution of this release; no rationality-to-finite-rank bridge is proved.
The full dyadic totient kernel span admits the explicit odd-core-indexed basis.
The basis theorem does not connect rationality to finite kernel rank.
Prove any one of these and the corresponding reduction above becomes unconditional.
strict_prime_tail_orbit_gap Prove the cofinal strict 9/10 real-part gap for the exact natural prime-tail orbit, or replace it with another producer for the reviewed pivot-escape endpoint.hankel_denominator_fan_in Prove eventual nonvanishing or a usable denominator obstruction for the Möbius-Mersenne power ladder and connect it to the target value.euler_sieve_limit_theorem Control the infinite Euler-sieve limit strongly enough that finite-stage quasimodularity yields a valid arithmetic obstruction.prime_ray_resultant_supply Realise the layer system by cyclic resultants and prove prime-support escape with the growth estimates needed to contradict a rational carry orbit.stern_brocot_arithmetic_bridge Prove the sharp cusp asymptotic and then supply a non-formal bridge from the geometric parameter regime to the exact totient value.The returned strict-orbit packet reports an exact finite deposit at parameters (147,23), verified through harmonic height 5022. It is research evidence, not a Lean-checked unbounded certificate.
| Module | Lines | Declarations | Theorems |
|---|---|---|---|
ErdosProblems.Erdos249.TotientStrictPrimeEscape |
211 | 8 | 5 |
ErdosProblems.Erdos249.FiniteEulerSieve |
69 | 6 | 4 |
ErdosProblems.Erdos249.PrimeRayCyclotomicCurvature |
215 | 14 | 9 |
The Comparator replays selected exact interfaces against a pinned toolchain. It never widens what Lean proved.
Statement and type parity replayed against the pinned toolchain.
An explicit odd-core basis and relation normal form for the full dyadic totient kernel.
The basis theorem does not connect rationality of the series to finite kernel rank.
totient_kernel_basis · targeted
An independent constructive proof of exact finite-level dyadic rank 2^e+1, together with a kernel-checked full-kernel infinite-dimensionality corollary already implied by Coons's non-2-regularity theorem.
Only the finite-level rank is presented as an additional result; full-kernel infinite-dimensionality is prior-art context, and no rationality-to-finite-rank bridge is proved.
totient_kernel_rank · targeted
Covered through a neighbouring selected interface, not replayed one-to-one.
The totient series is rewritten as a Lambert series with explicit nonnegative, unbounded prime-power coefficients.
The coefficient identities do not prove irrationality.
totient_lambert_coefficients · represented_by_basis_and_rank_targets
Stated in the corpus; not part of the replayed interface set.
For every base k at least 2, Lean checks the arithmetic reduction, exact nonmultiple-residue coordinates, unconditional canonical spanning, and exact rank k^e+1 conditional on canonical-family linear independence.
Lean does not prove all-base affine-section independence or formalise Martin's theorem. The unconditional basis and rank conclusions in the paper use that external input.
totient_kernel_all_base_index · not_selected_external_independence_boundary
A Farey denominator exclusion through 7.96e34, sharp for its selected window, and diagonal certificates through t=82.
The selected finite window and certificate ceiling do not imply an unbounded producer.
totient_finite_denominator_exclusion · not_selected_finite_family_has_separate_receipt
Rationality forces a tempered integral tail orbit with unbounded finite-level carry rank.
This is a necessary consequence, not a contradiction.
totient_carry_rank · not_selected_deep_orbit_vocabulary
Eventually periodic nonnegative rational weights give an irrational Lambert series.
The totient-derived weights are not eventually periodic.
eventually_periodic_lambert · not_selected_prior_result
Pointwise, cofinal, lcm-diagonal, and separated-window certificate supplies are exact or sufficient reformulations.
Equivalent producer statements are as hard as the unresolved target.
totient_certificate_equivalences · not_selected_deep_certificate_vocabulary
One review unit is prepared for the Palomar lane: cmp:249:finrank_totient_kernel, status prepared_without_public_outcome. Preparation is not a submission, a review, or any recorded outcome. Route description
A Basis for the 2-Kernel of Euler's Totient
The dyadic sections of Euler's totient have an explicit rational basis: the true truncation has dimension 1 at level 0 and exactly 2^e + 1 for e at least 1, so the full span is infinite-dimensional. A 240-bit Farey window excludes every reduced denominator through 79,639,646,646,701,375,323,355,774,875,831,053, and exact diagonal certificates exist for every t through 82. No t = 83 certificate, cofinal supply, or matching rank upper bound is proved; Erdős #249 remains open.