Results and open boundaries

Results and limits

This repository formalises theorems, reductions, equivalences, and obstructions related to eight Erdős problem programmes — #68, #243, #249, #251, #257, #269, #1041, and #1049. Each problem has a short paper and a longer reasoning record; the retired combined #249/#257 manuscript is archive/provenance only, not a current gateway. Using the degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement; the separate total-variation bound is also checked. The other seven targets remain open. Independent human review of correspondence with the 1958 wording has not been recorded. Comparator checks only selected exact statements, axioms and kernel acceptance; it does not assess novelty or historical correspondence.

Lean source checked by the pinned Lean kernel is proof authority. The audit log reports the headline declarations below with kernel assumptions [propext, Classical.choice, Quot.sound]. A theorem with hypotheses proves only the displayed implication; it does not prove that its hypotheses occur.

The short version

The front-page #257 example gives a complete irrationality theorem for restricted supports. The other programmes have direct results, exact reductions, conditional routes and counterexamples to tempting methods. The table gives one entry point per problem; the guide below keeps each result beside its missing step. Mathematical importance requires separate judgement.

Problem	A result to start with	Where the result stops
#68	Two exact finite denominator exclusions and a Lean-checked $3 / 2$ lower growth exponent; the paper also gives a finite calculation of attainable factorial moments after prescribed cancellations.	Lean proves irrationality equivalent to cofinally many non-unit factorial carries; no cofinal supply of such carries has been produced, so irrationality is still unproved.
#243	Lean checks irrationality under the precise cubic rate and every nonintegral regular rate above one; the paper transfers these zero-indexed statements to one-based indexing. Signed-error criteria also force eventual Sylvester behaviour under their stated premises.	The unrestricted Sylvester-tail hypotheses remain unproved.
#249	The short paper and Lean classify the fixed-base-two totient-residue series for every positive modulus and every rational-valued observable at dyadic moduli. They also give the exact all-base totient-kernel rank $k^{e} + 1$ .	The original series with unreduced totients remains open; the conditional routes still need their cofinal arithmetic inputs.
#251	Lean checks a rich synthetic prime-gap countermodel, and the paper gives a separate sparse-perturbation obstruction.	These are not actual prime gaps; the prime-specific producer for irrationality remains open.
#257	Lean checks the finite-prime weighted-support theorem at every integer base, including supports with divergent reciprocal sum.	It does not cover every infinite support. Palomar registered version 1 of the exact five-declaration `E257_01` selection.
#269	Both two-prime running-LCM sums are transcendental by the paper’s argument using a cited Hecke–Mahler theorem; Lean checks the formulas and the conditional transfer.	The cited transcendence input is not formalised, and the three-prime irrationality question remains open.
#1041	Ani’s degree-seven polynomial refutes the exact Formal Conjectures path-image-length statement in Lean; Lean also checks positive trinomial and sharp collinear families.	Independent review of correspondence with the 1958 wording is pending; other geometric results have their own hypotheses.
#1049	Lean checks irrationality in Zudilin’s rational-base contour region and exact Hankel orders.	$3 / 2$ and the all-rational-base claim remain open.

To read further, the paper catalogue has each short paper and longer reasoning record; the synthesis paper reads across the eight. To inspect a claim, use the source map, claim registry, prior art and verification dossier; Comparator covers selected formal statements, not every theorem or its novelty. The reproduction guide starts with one claim without Lean. For the system’s design and its open-source collaboration model, read the systems paper. The systems paper index identifies the earlier accounts retained for historical detail. To improve a proof, explanation or the architecture itself, use the contribution route, architecture guide and credit policy.

Problem-by-problem guide

#68. Put $S = \sum_{n \geq 2} 1 / (n! - 1)$ and $L_{N} = {lcm}_{2 \leq n \leq N} (n! - 1)$ . Any rational $S = a / q$ with $q > 0$ satisfies the two incomparable exclusions $q ∤ 299999!$ and $q \geq 2^{39990} > 10^{12038}$ . The first is a factorial divisibility constraint from a fresh exact GMP carry census through $m = 300000$ together with a Lean consumer; that replay matches the previously retained certificate, while an independent replay through $4000$ reproduces the unit-carry prefix. The second is an independent continued-fraction size bound. Neither implication yields the other, and neither proves irrationality. The paper and Lean proof give $lim inf \log L_{N} / (N^{3 / 2} \log N) \geq 2 \sqrt{2} / 3$ . This is a common-denominator theorem: it shows why clearing every summand separately cannot make the positive tail small, but says nothing by itself about the denominator after cancellation. Lean separately checks that irrationality of $S$ is equivalent to cofinally many non-unit factorial carries, and checks a finite quotient-band channel obstruction. The required cofinal carries are not produced. A local exact calculation at the prime $12487$ exhibits two critical roots for gap $12$ , so the earlier small-prime pattern of at most one critical root is not a uniform theorem; those roots have factorial values $442$ and $6300$ , not $1$ . Lean checks the $3 / 2$ theorem as common_denominator_growth_liminf in PaperCompleteLiminf.lean. The separate public Lean release wcook04/plectis-erdos-lean states the $3 / 2$ bound at commit 52f29ad1 as common_denominator_growth in its entry PalomarCorpus/E68 and proves it; that repository’s Linux replay of Palomar’s Comparator stage accepted the entry with both kernels (run 34782407633). Further conditional zero-branch and private-factor carry producers are in the formal evidence; neither supplies the cofinal property for the actual factorial-gap orbit. Read the short paper or long record. The separately prepared E68_05 Comparator selection contains six structural carry, channel and criterion declarations. It does not select the denominator exclusions or the $3 / 2$ growth theorem above. Its caller-side preflight passed at that exact source commit; this is not a Palomar registration.

The channel results have a direct finite use. For a finitely supported integer vector $λ$ on indices $n \geq 2$ , set $M (λ) = \sum n! λ_{n}$ and let $V_{d} (λ)$ be its factorial channel at $d$ , as defined in Section 2 of the short paper. Given a depth $D \geq 2$ , the paper classifies the moments possible when $V_{2} (λ) = \dots = V_{D} (λ) = 0$ . Its tail gcd needs only coefficients through $H = D (2 p - 1) < 2 D^{2}$ for a prime $D / 2 < p \leq D$ ; this makes the minimum positive moment a finite calculation. At $D = 4$ , the minimum is 1380, attained by $λ = (- 15318, 8176, - 710, 1518, - 253, - 88, 11)$ on indices $2, \dots, 8$ . Direct substitution gives $M (λ) = 1380$ and $V_{2} (λ) = V_{3} (λ) = V_{4} (λ) = 0$ ; the coordinate and finite-gcd theorems prove minimality. This certificate answers which moments survive a chosen finite cancellation. It does not establish nonintegrality of the remaining tail or irrationality of $S$ . Run python3 scripts/check_erdos68_channel_moment.py for the exact integer replay of the recurrence, finite gcd, moment and three vanishing channels. The paper’s finite tail-gcd theorem extends the computed gcd to all later indices.

#243. Under the exact cubic rate $a_{n}^{2} / a_{n + 1} = 1 + 3 / n + o (n^{- 3})$ , every strictly increasing positive integer sequence has an irrational reciprocal sum. Lean checks the zero-indexed theorem through a square-specialisation argument using Mathlib’s Dedekind-zeta simple pole; the short paper transfers it to one-based indexing by an ordinary finite-prefix argument. Its printed proof uses classical Chebotarev instead. This rate does not cover the unrestricted Sylvester-tail question.

More generally, the nonintegral regular-rate theorem checks irrationality when $λ > 1$ is nonintegral and $a_{n}^{2} / a_{n + 1} = 1 + λ / n + o (n^{-} λ)$ . Its Lean statement derives convergence for a positive, strictly increasing sequence indexed from zero. The long paper gives the ordinary finite-prefix transfer to one-based indexing. The integer-extraction lemma rules out nonintegral coefficients; the separate cubic argument rules out coefficient three. No rational examples are asserted for the remaining integer coefficients.

The rounded sequence $a_{1} = 8$ , $a_{n + 1} = ⌈ n a_{n}^{2} / (n + 3) ⌉$ has precisely this rate and product-ratio increments of order $n^{2}$ . Thus the separate bounded-increment recurrence criterion below gives no conclusion for it, while the cubic-rate theorem proves its reciprocal sum irrational. Duverney’s Corollary 3.2 supplies an earlier signed recurrence criterion under its printed one-sided growth-defect condition. In the all-positive, absolutely summable specialisation, the product-ratio increments tend to zero. For the rounded example, $a_{n + 1} / a_{n}^{2} - 1 \sim - 3 / n$ , so its signed defect series diverges and that absolutely summable specialisation does not apply. The exact $o (n^{- 3})$ remainder matters to the polynomial-exclusion proof. These comparisons locate the contribution without deciding its novelty or priority; the short paper’s argument and example give the proof and source locators.

The short paper also proves an ordinary original-sequence corollary. Let $a_{1} < a_{2} < \dots$ be positive integers, $a_{n + 1} / a_{n}^{2} \to 1$ , $\sum 1 / a_{n}$ rational, and $P_{n} = \prod_{j < n} a_{j}$ . If $lim sup (P_{n} / a_{n}) (a_{n}^{2} / a_{n + 1} - 1) < + \infty$ , then $a_{n + 1} = a_{n}^{2} - a_{n} + 1$ eventually. The needed limsup bound, or the paper’s alternative weighted record budget, is not proved for the unrestricted problem. Take a positive denominator $q$ of the full reciprocal sum and clear the nth tail by qP_n. The resulting integer error is minus $q$ times the scaled defect, up to a term tending to zero. This cancellation turns the upper bound in the original sequence into the lower bound on the integer error used below. The proof passes through a signed bounded-negative theorem. Lean checks that theorem and the canonical tail transfer described below. Let a,C,D : ℕ → ℕ and E : ℕ → ℤ. Assume $a (n) > 1$ , $C (n) > 0$ , the exact recurrences $C (n + 1) + D (n) = a (n) C (n)$ and $D (n + 1) = a (n) D (n)$ , and that $E (n)$ is the exact centered state with $| E (n) | < C (n)$ . If one constant $B$ satisfies $E (n) \geq - B$ for every $n$ , and for every $K$ one eventually has $K | E (n) | < C (n)$ , then $E (n) = 0$ eventually (boundedNegativePart_eventually_zero). The checked centered-zero theorem then gives the Sylvester recurrence once the exact product-cleared orbit has an eventually nonzero next-tail state. Lean carries that chain to the original denominators in boundedNegativePart_sylvesterNext_eventually, and checks the LCM-weighted bounded-defect corollary from the rational reciprocal sum in original_coordinate_lcm_bounded_defect (ErdosProblems/Erdos243/PaperCompleteR7/LcmDefect.lean:49); the paper derives the displayed $P_{n}$ form from that corollary by $A_{n} | P_{n}$ . For the state-system endpoint, no uniform lower bound on the centered error is proved. Unbounded negative excursions and the full Erdős endpoint remain open. The signed recovery develops Koizumi’s canonical-tail framework under an additional bounded-negative premise. Read the short paper, long record, or selected formal checks.

The long record also proves an exact maximal-gap theorem for a separate static sieve. Let $m_{0} < m_{1} < \dots$ be pairwise coprime integers at least $2$ , with $ℓ (m_{j}) = j + O (1)$ for $ℓ (x) = \log_{2} \log_{2} max (4, x)$ . If $σ = \prod_{j} (1 - 1 / m_{j}) > 0$ and $u_{n}$ lists the positive integers divisible by none of the $m_{j}$ , then $lim sup (u_{n + 1} - u_{n}) / ℓ (u_{n}) = 1 / σ$ . Lean checks the general theorem maximal_gap_limsup_eq_inv_sigma with the convergence to $σ$ stated explicitly. The paper’s finite-product calculation gives $σ = 1 / 2$ and thus coefficient $2$ for the Fermat moduli $m_{j} = 2^{2^{j}} + 1$ . This concerns avoidance of whole moduli, not coprimality to composite moduli or construction of a reciprocal-tail orbit; the unrestricted #243 question remains open.

#249. The short paper and Lean classify the fixed-base-two series with coefficients $φ (n) mod m$ : it is $0$ for $m = 1$ , $3 / 4$ for $m = 2$ , and irrational for every $m \geq 3$ . More generally, for $k \geq 1$ and any rational-valued function $f$ on the residues modulo $2^{k}$ , the series with coefficients $f (φ (n) mod 2^{k})$ is rational exactly when $f$ is constant on the even residue classes. If that constant is $c$ , the value is $3 f (1) / 4 + c / 4$ . For example, at modulus four, the table $f = (5, 7, 5, - 2)$ in residue order $0, 1, 2, 3$ gives $13 / 2$ , while $f = (0, 0, 1, 0)$ gives an irrational sum. The public Lean development checks the irrationality theorem and dyadic classification. The series with unreduced totients remains open.

The short paper also proves the all-base finite-level totient-kernel rank $k^{e} + 1$ for every $k \geq 2$ and $e \geq 1$ , with canonical integral coordinates and a basis of all integral relations; at prime base the rank is exponential in the depth $e$ . A rational $5 / 4$ control that agrees with totient on odd arguments still has tempered carry rank at least $2^{e} - 1$ at every depth, so a generic rationality-driven carry-rank ceiling is false. The strongest checked structural result on the hypothetical rational totient branch is carry anti-compression: one carry would have uniformly eventually-periodic dyadic sections modulo its multiplier while retaining canonical section rank at least $2^{e} - 1$ at every level. No finite-rank upper bound is proved, so this is a necessary consequence rather than a contradiction. Finite denominator exclusions and conditional actual-LCM, first-harmonic and strict natural-prime tail-gap routes remain useful, but none supplies its missing cofinal producer. Coons non-regularity, Martin affine independence, and Yazdani–Shallit CRT–Dirichlet separation are credited antecedents, not new claims of this release. Read the short paper, long record, and selected formal checks. For a concrete use of the basis, the short paper’s base-six example reduces all 43 sections through depth two to 37 coordinates. The exact normal-form tool prints those coordinates, the six relation coefficients, and an integer counterexample at one of the first 37 inputs whenever a proposed identity is false; its determinant check certifies that finite test. For any integer base, the sparse normal-form command reduces only the supplied sections to exact integral coordinates and decides their identity by the all-base basis theorem. For example, --base 12 --term 8:29859840:1 --term 2:10:-1990656 returns an identity without constructing the ambient depth-eight matrix. Its optional --witness-budget searches for a concrete unequal input; exhaustion does not change an exact nonidentity decision. The Python command is an implementation of the paper’s reduction, not a Lean-verified executable artifact.

#251. A public Lean declaration constructs a synthetic sequence of positive even digits bounded by $4 \log (n + 1) + 24$ . Its dyadic sum is exactly $6$ , every complete scaled tail and every tail shift is integral, the values $2$ and $4$ recur arbitrarily late in every residue class, and its increasing odd cumulative positions satisfy $P_{n} / (n \log n) \to 1$ . The reasoning paper states the combined theorem explicitly. This rules out a much richer package of plausible soft inputs than unboundedness or nonperiodicity alone, but these digits are not the actual prime gaps. The declaration is source-backed and does not yet have a curated claim row.

Independently, a sparse perturbation of the prime gaps can have a rational dyadic sum while retaining the prime growth scale, every fixed eventual congruence, and asymptotically the same short-block statistics. The later positions are not asserted to be prime. This is complementary to Land’s conditional result, not a refutation. Lean checks the sparse rational-target construction and the polylogarithmic schedule with growing-block transfer in SparsePaperR11.lean. The printed construction additionally gives congruence cutoffs uniform in the target; the linked Lean statement quantifies those cutoffs after the target. The prime-growth corollary uses cited analytic results. This obstruction shows that those coarse statistics alone do not force irrationality. Lean also checks a precise conditional route: for one fixed shift, cofinally many adjacent tail shifts strictly between $- 1$ and $1$ , with unequal actual prime gaps, would prevent eventual integrality of that shift. Those prime-specific mismatches are not proved. The exact prime-gap summation-by-parts equivalence still proves neither the prime-gap series nor the original series irrational. Read the short paper, long record, and selected formal checks.

#257. Fix a finite nonempty set of primes $P$ and let $h (a)$ be the largest divisor of $a$ supported on $P$ . For an infinite support $A$ and an integer base $b \geq 2$ , finiteness of $\sum_{a \in A} h (a) / (a (b^{h (a)} - 1))$ implies irrationality of $\sum_{a \in A} 1 / (b^{a} - 1)$ . The long paper explains the proof: if this sum were rational with denominator $v$ , every positive displacement from an integer would be at least $1 / v$ . Choose a finite part of $A$ and make its exponents divide an observation modulus $Q$ , so their displacements vanish. For the remaining exponents, a complete residue orbit gives the weighted main term. Averaging over a finite block of dyadic observation lengths charges the incomplete orbits by weighted reciprocal mass, uniformly over finite subfamilies; this uniform bound permits the passage to the infinite support. The short paper then chooses the modulus and block length so that its error charged to the whole weighted mass tends to zero. The Lean proof first makes the remaining tail weight small and uses a different block-length schedule. Both produce a positive displacement below $1 / v$ ; their parameter schedules should be read with their respective error bounds. Lean proves this as divisibilityWeightedClaim in WeightedReturn.lean. The short paper gives a shorter proof and an explicit support with divergent reciprocal sum satisfying the criterion. The comparison is with Erdős’s earlier reciprocal-summable condition, which he stated for every integer base after proving the pairwise-coprime case. For $P = {2}$ , write $a = 2^{k} m$ with $m$ odd: the weighted summand is $1 / [m (b^{2^{k}} - 1)]$ . In the short paper’s example $A^{⋆} = {2^{k} m : k \geq 1, m odd, m \leq 2^{2^{k}}}$ , dyadic blocks show that the odd reciprocals in the $k$ th layer sum to between $2^{k} / 4$ and $2^{k}$ . The layer therefore contributes at least $1 / 4$ to $\sum_{a \in A^{⋆}} 1 / a$ , but at most $2^{1 - k}$ to the base-two weighted sum. The ordinary reciprocal sum diverges while the weighted sum converges. The theorem gives irrationality at every integer base for every infinite subset of $A^{⋆}$ . It does not cover full support, all odd exponents, or the full prime support; Tao–Teräväinen prove the latter at base two by another method. The #257 reader exercise tests how changing a layer cutoff alters this certificate, and why a failed weighted test is not a rationality result. A second test shows why a prime set fitted separately to each finite prefix cannot certify the infinite hypothesis. The weighted-support transfer exercise gives the complementary fixed-host phenomenon: for any prescribed finite nonempty prime set, its binary weighted certificate can require every prime in that set. This is a calculation about the sufficient criterion, not a claim that each infinite subset needs the same witness or that the example has been formalised separately in Lean. The comparison identifies the added class and proof mechanism, but does not settle independent novelty or priority assessment. See the short paper’s theorem, example and sources. One host realises any finite monotone witness rule, checked in Lean as finite_monotone_witness_rule_realised. Given a finite set $E$ of primes and a nonconstant upward-closed rule on its subsets, a finite union of prime-cofactor blocks has divergent reciprocal sum, its weighted test converges at every base exactly when the witness primes in $E$ satisfy the rule, and every infinite subset has irrational subseries at every integer base. For three primes, any two suffice and none is individually mandatory. The worked variants compare this host with a different required-prime construction. The construction is AI-assisted and its novelty has not been independently assessed. At base two, the weighted condition can also be combined with the positive divisor-cover criterion: the long paper proves that a common finite averaging window makes both displacements small. Every infinite subset of their union then has irrational subseries at every integer base. Lean proves this as mixedSupportClaim in the same module. Neither theorem establishes the separately proposed hosts separating the two classes. Every infinite reciprocal-summable support satisfies it, yielding the coprimality-free extension stated by Erdős. Full-support irrationality at every integer base is classical (Erdős 1948) and Lean-checked here, as are pairwise-coprime summable-reciprocal support and Lebesgue measure one for the base-2 achievement set. Irrationality for every infinite support and the $1 / 2$ and $1 / 21$ branches remain open. The weighted theorem is Lean-checked. The exact five-declaration PalomarCorpus/E257_01 entry, which includes divisibilityWeightedClaim, passed Palomar mechanical verification for source commit b85ed30805188eb4390a686b111294b24363418e. Palomar registered version 1 as PALOMAR-2026-09-25-000009 on 25 September 2026. The immutable record binds that version to submission gid0ym5uu910, the pinned source, and the five selected declarations. Registration and mechanical verification cover the selected interface, not every claim in the paper or the unrestricted Erdős problem. Read the short paper, long record, and separate Comparator verification status.

#269. For three pairwise distinct primes, the threshold-column argument produces nonsingular selected kernel minors of every order and excludes every finite rational separated kernel representation. The arbitrary-order theorem is present in the compiled public Lean source, but the Wave-A receipt’s named axiom audit does not audit that rank declaration; Comparator checks only the displayed rank-two minor $- 1 / 15$ . For the actual ${2, 3, 5}$ series, Lean checks the rationality-to-positive-reduced-carry bridge. Cofinal local-window escape then extinguishes such carries; under the explicit cap hypotheses recorded in the claim registry, that escape statement is equivalent to irrationality. This is an exact interface, not an easier theorem whose premise has been proved. The source-specific escape and three-prime irrationality remain open.

For every pair of distinct primes, both the repeated running-LCM reciprocal sum and the version retaining one term at each distinct LCM value are transcendental. The ordinary proof expresses them as nonconstant quadratic and affine polynomials in one transcendental Hecke–Mahler value. Steve Fan posted the repeated-sum two-prime factorisation, reduction and transcendence conclusion first, on the problem’s forum on 26 June 2026; the note credits his priority, gives a proof found independently, derives the de-duplicated formula, and uses the cited Hecke–Mahler transcendence theorem. Lean also checks the two-prime affine and quadratic formulas and derives transcendence from the cited Hecke–Mahler result as an explicit named hypothesis; that external theorem itself is not formalised here. Read the short paper, long record, and selected formal checks.

#1041. A source-backed ordinary theorem covers monic degree- $n$ polynomials, $n \geq 3$ , whose distinct zeros lie on a circle of radius $ρ$ and satisfy $2 ρ^{n} \leq 1$ : two adjacent zeros have chord length at most $2 ρ \sin (π / n) < 2$ , and their straight chord lies in ${| f | < 1}$ . A repeated zero is an immediate short connection. The reasoning record explains the alternation and chord argument. The proof is outside Lean; an exact finite checker tests load-bearing identities and configurations, and the theorem does not yet have a curated claim row. At each fixed degree, the sharp arc constant $2$ leaves radii sufficiently close to $1$ outside this method.

Every monic trinomial with roots in the open unit disc also has radial root-to-origin segments inside ${| f | < 1}$ , so any two roots join through the origin with length less than $2$ ; Lean checks the complete displayed trinomial statement. For collinear roots, Lean checks a sharp Chebyshev segment bound and the resulting $< 2$ connector when the roots lie in the open unit disc. These are solved families, not a general connector theorem. For a squarefree monic polynomial, write $μ = min_{f^{'} (c) = 0} | f (c) |$ . An ordinary theorem gives a connector of length less than $2$ in the open unit lemniscate whenever $μ \leq 13 / 25$ , with no root-location hypothesis; scaling gives a connector of length less than $(5 / 2) μ^{1 / n}$ in ${| f | < (25 / 13) μ}$ . The sharp critical-value mean on the closed unit disc is Lean-checked with source-bound audit evidence, and the paper also gives an ordinary proof. The mean controls critical values, not connectors.

A further ordinary theorem gives a connector of length less than $2$ in every degree $n \geq 3$ when a simple nonzero critical value admits the stated separated critical-value disk at radius $4 / 3$ ; it asserts no existence of such a disk. On the generic stratum where simple nonzero critical values have pairwise distinct arguments and moduli, an ordinary slit-sheet theorem identifies the inverse-ray root-connection tree but gives no uniform length bound. Lean checks Newton-flow decay, ray-separating translations, and perturbative root retention. Using one degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set joining two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement and the separate total-variation formulation; correspondence with the 1958 wording remains unreviewed. The short paper also gives a cubic showing why a two-root first merger alone does not force a capacity gap; its Lean capacity clause assumes the classical transfinite-diameter formula. Read the short paper, long record, and selected formal checks.

#1049. For positive integers $0 < b < a$ in the exact Zudilin contour region, Lean checks irrationality and the stated irrationality-exponent bound for $F (a / b)$ , including every positive integral power of $31 / 4$ . The short paper also gives an ordinary proof for coprime $a, b$ under $\log b / \log a < θ^{*}$ , where $θ^{*} \approx 0.4056830214$ , using Zudilin’s 2004 forms and estimates. Zudilin’s prior work is credited; formalisation does not establish novelty. Lean also checks the normalized Hankel determinant’s order and leading coefficient at every rank. Separately, for each real $p > 1$ and $1 \leq N \leq 8$ , the Lean-checked finite coefficient pencil has a positive definite first matrix, real roots strictly below $F (p)$ , and non-strict interlacing at adjacent ranks. The eight unshifted determinant certificates are kernel checked; the shifted eight and 76 cyclotomic residue witnesses remain finite computations. These results give no all-rank coefficient positivity or irrationality at $3 / 2$ , which lies outside the contour region. The universal rational-base question remains open. Read the short paper, long record, and selected formal checks. The prepared E1049_01 Comparator selection contains 25 rational-base contour and measure declarations, including rational_base_threshold. It does not select the later Hankel determinant or finite coefficient-pencil results in the same paper. The caller-side preflight passed at that exact source commit; no registry intake is claimed.

This guide is not a new result ranking. PALOMAR_RESULT_SHOWCASE.json records a scoped candidate ranking for a possible Palomar submission; it does not rank mathematical importance across the whole corpus. Exact public statuses and open propositions live in claims.json.

For a narrative account, open the relevant item in the eight-paper portfolio. For exact declarations and assumptions, use the source map. The sections below retain the complete technical inventory, including result-family dispositions, semantic census data, finite measurements, and retractions; operational procedures live in the agent workbench.

Open the complete technical results inventory

Technical verdict

Using the degree-seven polynomial constructed by erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set joining two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement; the separate total-variation bound is also checked. The other seven targets remain open. Independent human review of correspondence with the 1958 wording has not been recorded. Comparator checks only selected exact statements, axioms and kernel acceptance; it does not assess novelty or historical correspondence. The development is neither an empty collection of restatements nor a claim to settle the seven unresolved targets or the unadjudicated historical #1041 formulation. For a first mathematical pass, the high-signal spine is:

#257, finite-prime weighted supports and a completed full-support case. The checked divisibilityWeightedClaim proves irrationality at every integer base under the stated base-two weighted mass condition for a finite nonempty prime set. Some qualifying supports have divergent reciprocal mass; full support does not satisfy this criterion, and arbitrary support remains open. Separately, the checked divisor-block proof combines a bounded Bertrand/CRT first block, middle-window divisor-pair averaging, weighted tail control, and parameter closure (irrational_erdosSum_full_support). It proves the canonical full-support series irrational in every integer base $b \geq 2$ , but not universal #257. A distinct adaptive-CRT certificate proves irrationality for every infinite pairwise-coprime support with summable reciprocal mass; those structured-support hypotheses likewise leave arbitrary support open. A deeper, genuinely distinct conditional route proves the base-2 support series under a finite-core orthogonal-petal bouquet plus the uniform SunflowerForcedSlotTailSelection predicate (irrational_erdosSupportSeries_of_orthogonalPetalBouquet, Erdos249257/SupportSunflowerDichotomy.lean:540); the selector and bouquet are not constructed for arbitrary supports. A separate direct result covers nonnegative rational eventually periodic coefficient sequences with a positive periodic-tail value: one common denominator reduces the claim to the periodic divisor-orbit sieve (irrational_ratWeightSeries_eventuallyPeriodic, Erdos249257/CertificateKernel.lean:12811); mixed-sign coefficients and arbitrary supports remain outside its hypotheses. Separately, the full base-2 Mersenne achievement set has Lebesgue measure exactly one, while the supported-set theorem gives exact finite-complement measure or zero for an infinite complement (volume_mersenneAchievementSet, Erdos249257/GreedyAchievementSet.lean:996; volume_supportedMersenneAchievementSet_dichotomy, ErdosProblems/Erdos257/MersenneSubseriesRigidity.lean:397). This is consequential global geometry, not a classification of rational points or a universal irrationality theorem.
#1049, irrationality throughout a rational-base region. The Lean-checked rational_base_region theorem constructs the required polynomial forms and analytic estimates for bases in the stated Zudilin contour region. It proves irrationality of $F (a / b)$ there and an irrationality-exponent bound; in particular, $F ((31 / 4)^{r})$ is irrational for every positive integer $r$ . This formalises a stated region, not the universal rational-base claim. The base $3 / 2$ lies outside that region and remains unresolved here.
#1041, ani’s degree-seven counterexample. For ani’s explicit polynomial, the checked erdos1041_counterexample_hausdorff theorem shows that every preconnected strict-lemniscate set joining distinct roots has one-dimensional Hausdorff measure greater than two. It refutes the exact Formal Conjectures path-image-length statement; a separate total-variation bound is checked. Ani supplied the polynomial. The reported family is not formalised, and correspondence with the 1958 wording awaits independent human review.
A second-layer Boolean–Möbius normal form is now an executable rationality equivalence: any $p / q$ support value ( $q > 0$ ) is represented by a positive, square-root-bounded integer carry orbit whose quotient reconstructs the support. This is a change of coordinates for hypothetical rational support, not a contradiction or a universal #257 proof; arbitrary infinite support and the $1 / 2$ membership boundary remain open.
Degree-restricted #1041 positive routes remain open. The source frontier’s parent carrier is $min_{c} L (c) \leq 2$ over admissible hubs on the ray-separated locus. Its Corollary G, with Theorem L and Corollary S, ordinary proofs in the research corpus with no human review, shows that the carrier in degree $n$ gives the degree- $n$ case of #1041, so ani’s example makes the carrier fail in degree seven. Its degree-five SPOKE-5 instance would settle degree five. This is source-only research evidence with no Lean counterpart: hub choice, path containment, and the SPOKE-5 supply remain open, and the earlier minimum-critical and aggregate shortcuts are explicitly refuted (research_corpus/Erdos1041/FRONTIER.md).
#249, one open bound. Lean proves that $S = \sum φ (n) / 2^{n}$ is irrational if, for every shift $h \geq 1$ , there are arbitrarily large $X$ at which the real part of the first-harmonic sum over the good indices is at most $603 X / 1000$ , at $s = 26$ , $η = 1 / 1000$ and minimal depth (irrational_totient_series_of_goodBase_gap, ArgumentGraph/Results/Erdos249Endpoint.lean). For all large $X$ more than $67 X / 100$ of the indices in $[X, 2 X)$ are good (eventually_card_pivotGoodBases_gt), so the bound asks for the average first-harmonic cosine over them to stay below $9 / 10$ . At these parameters the four pivot budgets imply it, and it asks less than the prime-number-theorem route’s $11 X / 20$ . The bound is open. The actual-LCM orbit route is a second sufficient route: an explicit approximation of the orbit by an odd-rank raw block, with an error radius, turns cofinal distance at least $1 / 32$ plus that radius from every integer into the existing signed-margin producer. The exact source calls this PowerTwoActualLcmOrbitSeparationSupply and then derives irrationality from it, but this is a sufficient route, not an equivalence to the separate non-integrality criterion. The supply itself is not proved; neither divisibility nor irrationality alone supplies the required anti-concentration. Separately, the dyadic totient-kernel rank $2^{e} + 1$ and its odd-core basis are an unconditional finite-level structural result, and so are the all-base rank $k^{e} + 1$ and its explicit basis for every $k \geq 2$ and $e \geq 1$ : AllBaseTotientKernel.lean discharges the affine-independence premise of the reusable all-base wrapper. The actual-LCM, diagonal, and phase/prime producers remain open, so neither structural spine solves the binary totient endpoint.
A distinct orbit-level carry anti-compression result is now checked: under hypothetical rationality, one positive multiplier supplies a tempered integral carry whose dyadic sections share an eventual modular period, while the canonical carry-kernel rank is at least $2^{e} - 1$ for every $e$ . The hard friction is that modulo a divisor of the multiplier the totient forcing vanishes and the carry becomes geometric, so this gives no finite-rank contradiction or irrationality proof (ExternalVerification/Challenge.lean:137; Erdos249257/TotientTailCarryPeriod.lean:224).
#68, an exact endpoint reduction. Irrationality is equivalent to cofinally many strict factorial-top divisibility misses, equivalently to cofinally many non-unit carries. The equivalence transfers the hard producer question exactly; it does not supply that producer.
#243 and #251, boundary results that diagnose the missing input. Fresh pairwise-coprime moduli obstruct bounded rises, while periodic/vanishing negative-error regimes are excluded; for #251, unbounded prime gaps and an exact prime-gap irrationality equivalence still leave the concrete tail bridge open. A public Comparator-backed abstract denominator classifier reduces a dyadic tail’s rationality to eventual integrality of one positive shift. Its companion normal form says, for a RealDyadicTailRecurrence, irrationality is equivalent to every positive tail shift being nonintegral; neither classification supplies the prime-specific producer.
#269 structural checks and further #1049 diagnostics. Running-LCM height and rank-two obstructions, plus a distinct weighted-phase observer that separates a finite residue digit from an uncontrolled integral coboundary, isolate the #269 mechanism without claiming its endpoint. For #1049, the growing-rank four-jet/Padé kernel says that when $0 < R$ and $4 R + 2 S \leq n$ , fewer finite endpoint signatures than binary selectors force a collision; row-content divisors remain as a second barrier. A separate explicit rectangular two-function Hermite–Padé model has a sharp no-go under $0 \leq ρ$ and $1 + ρ \leq σ$ , but neither route constructs approximants/remainders or proves irrationality at $3 / 2$ .

The finite #249 certificate band, Stern–Brocot and gcd-moment identities, #257 measure/noncollapse geometry, and the cited-only ladders remain useful supporting routes. They are deliberately secondary to the mechanisms above: finite ranges do not become cofinal theorems, and cited analytic inputs do not become Lean results by appearing in the same paper.

Signal-audit dispositions

The problem-by-problem guide above gives the current result selection, including stronger ordinary-paper results. This table records an earlier scoped review of selected mechanisms and their supporting roles; it does not rank the full current corpus. The detailed sections retain the exact statements and evidence boundaries.

That review compared consequence, endpoint proximity, mechanism depth, distinctness, usefulness, evidence certainty, and the remaining burden. Its dispositions are editorial judgments, not novelty, priority, or proof-status claims.

Disposition	Reader-facing treatment	Mathematical reason
promote	#257’s full-support irrationality theorem, pairwise-coprime extension, orthogonal-petal reduction, and nonnegative rational eventually-periodic coefficient theorem, together with #249’s actual-LCM separation reduction, led that scoped review.	The full-support row is an unconditional endpoint case for each $b \geq 2$ ; the pairwise CRT and periodic denominator-clearing rows are distinct direct mechanisms; the bouquet and actual-LCM rows add unusually deep endpoint-facing conditional structure, with their unproved supplies kept adjacent rather than hidden.
retain	#257’s achievement-set measure geometry, Boolean–Möbius exact-row conditional route, and sublogarithmic zero-window constraint, #68’s exact carry equivalence, #249’s diagonal full-target and foreign-residue reductions, finite kernel rank/basis, orbit-level carry anti-compression, and fixed-precision valuation/unit no-go, #243’s bounded-rise, negative-orbit, and signed centered-recovery boundaries, #251’s equivalence and countermodel, #269’s height/rank obstruction and weighted-phase observer, #1041’s admissible-hub/SPOKE-5 source frontier and Lean ray/root inputs, and #1049’s recurrence, rectangular-threshold, and four-jet/no-go boundaries remain useful supporting mechanisms and open routes.	The measure rows give consequential global geometry without classifying rational points; the Boolean–Möbius exact-row route gives a concrete local-to-cofinal half-membership mechanism under an unproved positive-skip supply, so it is useful endpoint-facing structure but not a contradiction; the sublog row gives a rationality-conditional coverage bound with a support/numerator-dependent constant, not a contradiction; the #68 and #249 rows are exact endpoint-adjacent or infinite-dimensionality results without their missing producers, while the #249 diagonal row makes integrality a full-target foreign-defect hit, the foreign-residue row adds an exact finite foreign/divisor split and closed geometric tail bound, and the orbit conjunction exposes modular periodicity alongside rank growth and its forcing-erasure friction; the fixed-precision row gives a prefix-locked centred completion for every finite compatible odd-unit word at fixed positive precision, so bounded local signatures cannot exclude every finite endpoint; its unrestricted high quotient is synthetic rather than actual totient arithmetic, and no #249 endpoint follows; the foreign row still needs the unproved `ControlledForeignProjection` bridge and unbounded separated-projection supply; the signed #243 recovery forces a centered defect to zero under exact displayed dynamics and bounded-negative hypotheses but leaves the unbounded mixed-sign branch open; the #269 observer exposes a finite residue/uncontrolled-coboundary split and a conditional finite-span criterion, but no finite-state quotient or endpoint; the source-only #1041 selector remains the direct degree-five/unrestricted socket while its local Lean inputs do not supply the global topology or metric selection; the #1049 rectangular threshold is sharp only for its explicit two-function model and the four-jet collision remains finite, so neither supplies an approximant/remainder bridge; the other rows rule out named regimes or supply exact identities without the missing universal, cofinal, topological, or irrationality bridge.
consolidate	The adjacent #249 gcd-moment, Stern–Brocot, finite-denominator, scalar-height, and synthetic LCM-shift results form one supporting arithmetic route; #257’s finite-period, state, and defect results form one supporting universal-boundary route.	These results reuse finite-level or finite-support interfaces and share the same endpoint gap; the scalar-height lemma transfers denominator information but is not an irrationality criterion. Grouping these mechanisms preserves their reuse value without making repeated local identities look like separate endpoint advances.
demote	Citation-only #249 context and other classical formalised variants follow the local checked mechanisms; the canonical #257 full-support theorem stays promoted.	Provenance and known formalised cases establish context or a restricted theorem, not a new #249 conclusion; the completed full-support mechanism is the explicit exception because it is a direct checked endpoint case.
replace	That review replaced a citation-first/problem-order presentation with a comparison of selected mechanisms; the current problem guide above now supplies the result selection.	Consequence and load-bearing mechanism are more informative to a first reader than paper order, while the per-problem sections preserve complete coverage and exact source routes.
long-tail-only	Finite searches, measurement logs, routine certificate shards, and unselected conditional predicate stacks remain discoverable through the source maps, but do not lead the reader.	A finite range, routine shard, or unconstructed antecedent cannot establish a cofinal family or universal endpoint, so it is evidence for follow-up rather than first-contact signal.

The project also audits its conditional routes for endpoint equivalence. Some named hypotheses are exact restatements of an open endpoint rather than smaller subproblems; that diagnosis prevents a reformulation from being mistaken for progress.

Only after those theorem-level facts comes the corpus census. The current semantic graph provides three diagnostic views across every indexed Erdős problem:

View	#243	#249	#257	#1049	shared	total
mechanically nonrecurring candidates	3	90	169	5	20	287
classical/prior-art formalisations	1	36	23	1	40	101
bare open-problem equivalences	0	15	15	0	2	32

The nonrecurring view contains 185 unconditional object theorems, 56 scoped barriers, and 46 reductions or transports after aliases, open antecedents, bare equivalences, finite/generated instances, infrastructure, classical results, and routine corollaries are removed.

The internal adjudicated frontier shortlist contains 11 nodes; it is distinct from the 7-node public prior-art review queue. 232 nonrecurring candidates remain unassessed for prior art. The live authored open-antecedent surface has 52 clusters, of which 10 are marked endpoint-equivalent. None of these populations is a novelty census.

Agents use the live owners rather than a frozen restatement sample:

python3 scripts/query_corpus.py --overview --format card for reviewed claim status and exact registered Lean interfaces;
python3 scripts/query_corpus.py --route <route_id> --format card for one problem programme and its open boundary;
python3 scripts/query_semantic.py node <node_id> and family-relations <family_id> for cross-paper statement and relation navigation;
docs/PALOMAR_RESULT_SHOWCASE.json for the current candidate universe and screening dispositions; and
scripts/residual_evaluator.py for a kernel-backed comparison of one proposed reduction with its target.

The claim registry covers selected registered claims, not every sentence in every paper. Semantic relations and Palomar screening are navigation and review surfaces; neither is proof, novelty, significance or peer review.

The large #249 denominator exclusion is a direct, kernel-checked instantiation of the classical neighbouring-fraction/mediant method. That method supplies the displayed bound exactly (numerical delta $0$ ). The local addition is the checked arithmetic instance, its transfers, and its sharp first failure.

Strongest checked results by problem

This is a high-signal orientation by problem, not a one-result roster: it gives the strongest checked statements, their exact status, and where to verify them. Each item carries the independent labels used across this repository: what Lean checked, what the statement changes, and its literature relationship. formalised here renders known mathematics; proved here makes no novelty claim — that judgement is a human number theorist’s, and no query here supplies it. Reduction targets are named with their own status in the same sentence. The claim registry and generated verification projection are supporting navigation; they do not replace the source declaration or enlarge its claim ceiling. The per-problem sections below are the human reading map, with evidence, attribution, and surviving boundaries kept together.

#68 — is $\sum_{n \geq 2} 1 / (n! - 1)$ irrational?

Irrationality is equivalent, with no hypotheses, to one integer divisibility test on exact rational prefixes failing infinitely often — irrational_factorialGapSeries_iff_cofinal_strictFacTopRat_misses, ErdosProblems/Erdos68/FactorialGapPlateauCore.lean:986. Checked theorem; exact equivalence, transporting the difficulty without reducing it; registry: none.
A separate finite quotient-band obstruction is now explicit. For a finite coefficient family whose indices all satisfy $k d \leq i_{j} < (k + 1) d$ , the factorial moment factors as $M = (d!)^{k} C_{d}$ ; in the first band, channel cancellation $C_{d} = 0$ therefore forces $M = 0$ . More generally, if all indices are at least $d$ , channel cancellation with $M \neq 0$ forces some index to be at least $2 d$ (ErdosProblems/Erdos68/ChannelBreakpointRigidity.lean; paper discussion in erdos-68-factorial-denominator-irrationality.pdf). Registry: channel_quotient_band_breakpoint (res:bandbreakpoint); its source and evidence boundary are the authority. This is a finite-family breakpoint only: it supplies no cancelling family, simultaneous-channel control, residual estimate, or cofinal non-unit carry.
The kernel-internal denominator bound is $q \geq 67$ (ErdosProblems/Erdos68/FactorialZeroPlateauCertificates.lean:136); the $300000$ exclusion is a checked implication (ErdosProblems/Erdos68/FactorialGapPlateauCore.lean:812) whose evaluation is an external computation, not a kernel result.
Open: produce infinitely many non-unit carries.
A parallel carry form makes the same boundary explicit: irrationality is equivalent to cofinally many non-unit carries (irrational_factorialGapSeries_iff_cofinal_nonunit_carries, ErdosProblems/Erdos68/FactorialGapPlateauCore.lean:945). The equivalence supplies no cofinal carry producer, so #68 remains open.

#243 — does rationality force eventual Sylvester recurrence?

A divergent natural sequence with upward steps bounded by $B$ cannot stay coprime to an infinite family of fresh pairwise-coprime moduli — no_boundedRise_of_tailAvoidance, ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:897. Checked theorem; reusable obstruction; claims registry: bounded_rise_fresh_modulus_barrier (res:barrier).
Normalised vanishing for the canonical orbit is derived in PaperCompleteR7/CanonicalState.lean from the original growth and rationality hypotheses. The paper credits Koizumi (Integers 26 (2026), A28). With this vanishing, a bounded negative part or finite normalised negative mass forces the error to vanish and the Sylvester recurrence to begin (ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:2177, ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:2264; ErdosProblems/Erdos243/SparseResetRecovery.lean:155, ErdosProblems/Erdos243/SparseResetRecovery.lean:175). Checked conditional theorems; the note concedes its absorption and descent lemmas as Koizumi prior art.
A separate no-go rules out an eventually periodic negative-error orbit when the phase growth is positive (no_eventuallyPeriodicNegative_orbit, ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:796; claims registry: eventually_periodic_negative_no_go). Its exact hypotheses include $2 \leq a (n)$ , $0 < e (N + n) < a (N + n)$ , the denominator, tail, and shape recurrences, and positive-period/positive-drift equations. It does not cover unbounded upward excursions of the unreduced numerator, so the open boundary remains.
A separately declared Comparator interface no_cofinallyBoundedNegative_of_normalizedVanishes restates another conditional no-go under a fixed axiom budget: with $a (n) > 1$ , positive $C$ and magnitude, the coupled recurrences $C (n + 1) + D (n) = a (n) \cdot C (n)$ and $D (n + 1) = a (n) \cdot D (n)$ , a bounded rise $C (n + 1) \leq C (n) + B$ , normalized vanishing K·magnitude(n) < C(n) eventually for every $K$ , and a cofinally bounded negative part, the hypotheses are inconsistent (ErdosProblems/Erdos243/ReciprocalTailRigidity.lean). Every dynamical, positivity, bounded-rise, and vanishing assumption remains explicit; this does not close unbounded upward excursions of the unreduced numerator (claims registry: bounded_negative_exclusion; source coordinate: ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:1748). The interface is not a fresh passing receipt for this release commit.
A distinct signed recovery family makes the centered mechanism executable: boundedNegativePart_eventually_zero assumes $a (n) > 1$ , $C (n) > 0$ , the exact natural dynamics $C (n + 1) + D (n) = a (n) C (n)$ and $D (n + 1) = a (n) D (n)$ , $E (n) = D (n) - (a (n) - 1) C (n)$ , strict $| E (n) | < C (n)$ , a uniform lower bound $E (n) \geq - B$ , and division-free normalized vanishing; it forces $E = 0$ eventually. With centered zero and an eventually nonzero next tail, sylvesterNext_eventually_of_centered_zero recovers the Sylvester recurrence. The latter two declarations are mechanism evidence for this one family, not separate rows. Lean carries the chain to the original denominators in boundedNegativePart_sylvesterNext_eventually (ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:2412), and checks the LCM-weighted bounded-defect corollary from the rational reciprocal sum in original_coordinate_lcm_bounded_defect (ErdosProblems/Erdos243/PaperCompleteR7/LcmDefect.lean:49). The frontier profile of a counterexample is checked in canonical_frontier (ErdosProblems/Erdos243/PaperCompleteR7/Frontier.lean:151). This is not reciprocal-tail irrationality: unbounded upward excursions of the unreduced numerator remain open. The selected statement has a separately declared Comparator interface; that is not a fresh passing receipt for this release commit (Comparator wrapper: ExternalVerification/Challenge.lean:96-109; source ErdosProblems/Erdos243/ReciprocalTailRigidity.lean:2265, with supporting declarations at :1837 and :1799).
Open: unbounded upward excursions of the unreduced numerator.

#249 — is $\sum φ (n) / 2^{n}$ irrational? (reviewed core)

Cited-only source ceiling: Nesterenko’s 1996 Corollary 2 gives algebraic independence of the Ramanujan values at algebraic $q$ with $0 < | q | < 1$ . At $q = 1 / 2$ , its exact identity $P (1 / 2) = 1 - 24 \sum_{n \geq 1} σ (n) / 2^{n}$ makes the divisor-sum series $\sum_{n \geq 1} σ (n) / 2^{n}$ transcendental by an elementary affine rewrite (source closure). This is a distinct $σ$ -coefficient ladder rung, not the Euler-totient constant $S$ ; Nesterenko’s analytic proof is not formalised here, and no #249 irrationality or novelty claim follows.
Cited-only q-zeta antecedent: Postelmans and Van Assche prove that $1$ , $ζ_{q} (1)$ , and $ζ_{q} (2)$ are linearly independent for $q = 1 / p$ with integer $p > 1$ (Theorem 1.3). At $q = 1 / 2$ , the release’s separately formalised identity $L_{2} (1) = ζ_{1 / 2} (2) - ζ_{1 / 2} (1)$ therefore gives an irrational constant-weight squared-Lambert value (source closure). This does not transfer to the Möbius-weighted totient constant $S$ , and the source supplies no #249 or #257 solution.
A nearby cited-only sparse criterion of Kaneko, Suzuki, and Tachiya gives irrationality of $\sum f (n) / t^{σ (n)}$ and $\sum f (n) / t^{φ (n)}$ under explicit nonnegative infinite-support and growth hypotheses (source closure). Here $φ (n)$ is a denominator exponent, not the coefficient of $2^{- n}$ ; this result does not transfer to $S$ , arbitrary-support #257, or the release’s gcd-moment identities.
Unconditional: the dyadic sections $n \mapsto φ (2^{j} n + r)$ of Euler’s totient have an explicit rational basis. The canonical family $φ (n)$ , $φ (2 n)$ and $φ (2^{j} n + r)$ with $1 \leq j \leq e$ and $r$ odd spans a space of dimension exactly $2^{e} + 1$ — finrank_canonicalTotientKernel_eq, Erdos249257/TotientMahlerDefect.lean:989; basis object at Erdos249257/TotientMahlerDefect.lean:1392. For every $e \geq 1$ this is the span of all sections through level $e$ ; at level zero that span is $φ (n)$ alone, of dimension one. A theorem about the coefficient sequence, not about irrationality of $S$ ; it quantifies the known qualitative fact that $φ$ is not 2-regular (Coons 2008, arXiv:0810.3709, via ζ zero-density — no exact rank appears there). Claim dyadic_totient_certificate_interface (the basis declarations at Erdos249257/TotientMahlerDefect.lean:1265, Erdos249257/TotientMahlerDefect.lean:1380, Erdos249257/TotientMahlerDefect.lean:1392 — registry: dyadic_totient_certificate_interface).
The Comparator interfaces make the rank frontier precise: for every $e \geq 1$ , finrank_totientKernelThroughLevelFamily_eq gives dimension $2^{e} + 1$ for the actual finite truncation, while exists_totientDyadicSectionBasis supplies the explicit odd-core-indexed basis. The full-kernel interface not_finiteDimensional_span_fullTotientKernel proves that the rational span is not finite-dimensional. These are coefficient-space facts, not a rationality-to-finite-rank bridge or an irrationality proof.
For every base $k \geq 2$ and level $e \geq 1$ , an all-base extension has an explicit canonical spanning family. Its reusable conditional theorem gives dimension $k^{e} + 1$ under a linear-independence hypothesis (finrank_allBaseTotientKernelThroughLevelFamily_eq_of_linearIndependent, Erdos249257/TotientKernelConditional.lean:215; claims registry: all_base_totient_kernel_conditional_rank). The separate AllBaseTotientKernel.lean proof discharges that hypothesis and gives the unconditional rank and basis stated in the table below. This remains a coefficient-space result, not an irrationality proof for $S$ .
A scalar-localisation height lemma transfers, rather than discards, denominator information: under its displayed divisibility hypotheses, scalarLocalization_complement_dvd bounds the complementary factor of a reduced denominator by the multiplying integer, with the integer-coordinate identity supplied by scalarLocalization_integer_eq_mul_num (Erdos249257/AdelicHeightObstruction.lean:23,56; claims registry: adelic_height_obstruction). This is supporting arithmetic, not an irrationality criterion.
A distinct actual-LCM orbit reduction makes the next analytic obligation explicit. With $H_{a} = lcm (1, \dots, 2^{a})$ and R_a = totientTail(2H_a) − totientTail(H_a), the source defines PowerTwoActualLcmOrbitSeparationSupply as a cofinal supply of canonical odd ranks whose $R_{a}$ stays at least 1/32 + actualLcmRawErrorRadius a q from every integer. The checked raw-block approximation and its explicit error bound then force the existing half-word/signed-margin producer, and irrational_totientSeries_of_actualLcmOrbitSeparationSupply derives irrationality from that hypothesis. This is a new sufficient, non-equivalent quantitative bridge, not a proof of its supply: the module explicitly leaves that anti-concentration question open, and the earlier sign/top-edge result does not establish it. See Erdos249257/TotientActualLcmOrbitSeparation.lean:254-310 and the transported consumer ExternalVerification/Challenge.lean:159.
The public support transport keeps the boundary from collapsing into a sign argument. actualLcmTailDiff_shift_pos gives the positive corridor under $8 \leq a$ and its shortness inequality; actualLcm_trueEndpointSurvivor_neg shows that the true translated survivor can still be negative under the corresponding integer-difference hypothesis; and actualLcm_integral_forces_topEdgeResidue puts an integral orbit in the exact top-edge residue strip under its additional room inequality (ExternalVerification/Challenge.lean:198-239). These three declarations are support for the single actual_lcm_orbit_separation family, not three independent routes: positivity does not exclude the survivor, and neither row supplies cofinal separation or top-edge exclusion.
A complementary diagonal pincer exposes the exact full-target coordinate: diagonal_int_iff_foreignDiagonalDefect_hits_fullTarget says that diagonal integrality is equivalent to the foreign defect hitting the complete reduced target (Erdos249257/DiagonalPincerDecomposition.lean:215). Its companion irrational_totientSeries_of_full_target_avoidance_supply would turn cofinal misses into irrationality (:290), but that full-target avoidance supply is open. This is one exact reduction subordinate to the actual-LCM frontier, not a new endpoint theorem or a second producer.
A separate public first-harmonic pivot route is represented in the Comparator roster through its transported decomposition, budget, and conditional endpoint in ExternalVerification/Challenge.lean. The exact four-term decomposition of one block is windowFirstExp_sum_eq_pivot_decomposition; under the explicit room inequality, PivotBudgetAt bounds the centred real part by $14 X / 25$ and the other three norms by $X / 100$ , $X / 100$ , and $8 X / 25$ . The exact first_harmonic_gap_of_pivotBudgetAt consequence records the resulting real first-harmonic gap of $9 X / 10$ and hence a finite certificate (Erdos249257/FirstHarmonicPivot.lean:514-552). The cofinal socket DTWPivotResidualDecorrelation would imply irrationality, but its supplier decorrelation budgets are unproved. The supporting image_pivotSupplierPrimes_eq_pivotFiber identity and supplierPrime_not_globally_isolated_counterexample counterexample expose the exact support boundary: at $X = 16, L = 20, s = 1, m = 2, N = 18$ , a supplier prime is not globally isolated (:394, :569-588). Comparator exposes this conditional route, but the supplier decorrelation budgets are unproved, so the unbounded certificate supply remains open.
A separate source-current strict_prime_tail_orbit_gap family is retained below the actual-LCM and first-harmonic frontiers. Its Comparator wrapper irrational_totient_series_of_naturalPrimeTailOrbitStrictGap has one coherent two-branch interface. The subordinate tailOrbitFirstExp_succ identity records the exact squaring evolution of each tail-orbit phase; it clarifies the phase mechanism but supplies neither the $(11 / 100)$ density nor the cofinal-prime producer. The later tailOrbitFirstExp_add and tailOrbitFirstExp_eq_initial_pow_two identities reduce every future phase to a power-of-two iterate of its initial phase; not_naturalPrimeTailOrbitStrictGap_of_dyadic_root shows that entering a dyadic root blocks the strict-gap producer. These are contrary-mechanism constraints, not density or cofinal-prime supply. In the block branch, for every $h > 0$ and cutoff $X_{0}$ , TotientTailOrbitNonpositiveBlockDensity assumes a late block with at least $(11 / 100) * X$ nonpositive values of Re(tailOrbitFirstExp h N); unit norm gives an $89 / 100$ block saving, and a single $1 / 100$ truncation budget gives the finite $9 / 10$ certificate gap. In the prime branch, for every $h > 0$ and $N_{0}$ , DTWNaturalPrimeTailOrbitStrictGap assumes a prime $p \geq max (N_{0} + h + 1) (h + 5)$ with Re(tailOrbitFirstExp h (p − h − 1)) < 9/10; its positive margin feeds exact natural pivot-fibre escape. The phase-density, cofinal-prime, and uniform-margin producers are all open for the actual totient orbit, and nonintegrality alone gives no fixed distance from the integers. This is producer-side conditional evidence, distinct from the actual-LCM and first-harmonic routes and not an #249 proof, novelty, or priority claim (ExternalVerification/Challenge.lean; ErdosProblems/Erdos249/TotientStrictPrimeEscape.lean:25-233).
Irrationality of $S$ has six checked exact characterisations, from tail-difference certificates through the lcm-diagonal form to window-separated pairs — Erdos249257/LcmConeFlatness.lean:316–426, Erdos249257/PivotAntiReconstruction.lean:1775; claims certificate_completeness, certificate_reduction.
Finite: the classical Farey/mediant window at $K = 240$ excludes reduced denominators through $7.96 \times 10^{34}$ — improvement over the classical bound: zero (claim denominator_exclusion) — and diagonal certificates exist at every $t \leq 82$ , with the plateau broken at $t = 83$ and a proved depth floor of $125$ there (ErdosProblems/Skip/LadderT67.lean:71264, ErdosProblems/Skip/LadderT67.lean:71285, ErdosProblems/Skip/LadderT67.lean:71294; claim certified_kill_instances; no certificate at $t = 83$ is claimed).
Open: the unbounded certificate supply, which is equivalent to #249 itself; a checked splice construction shows no finite inspection can settle it.
A separate Comparator-transported fixed-precision no-go, fixedPrecisionTropicalNoGo, gives every finite compatible valuation/unit word at fixed $u > 0$ a bounded prefix-locked centred completion by varying an unrestricted high quotient (ExternalVerification/Challenge.lean:150-158; Erdos249257/TropicalCurvatureCarry.lean:69-142). This is synthetic finite- word evidence: it blocks bounded local signatures alone, but does not encode actual totient differences or supply growing precision, global correlation, a #249 endpoint, or irrationality.
A checked synthetic no-go shows that, for every $t \geq 3$ , a nonzero dyadic coboundary can survive every finite integer shift polynomial while retaining the period-LCM totient factor ideals, exact cleared-prefix cancellation, and uniform state and letter bounds (Erdos249257.TotientTailPeriodKiller.lcm_factorIdeal_finiteRank_shiftAlgebra_not_sufficient, Erdos249257/LcmFactorIdealPulseObstruction.lean). This obstructs that finite shift-algebra route only: the forcing letters are synthetic rather than actual totient differences, nonlinear combinations are not covered, and no unbounded certificate supply follows.
Two additional checked #249 families are directly inspectable: an exact squared-Lambert gcd-moment transfer at base $1 / 2$ — tsum_totient_div_mersenne_sq_eq_gcd_moment_series identifies the totient-weighted squared-Mersenne Lambert series with the dyadic series of Pillai’s gcd-sum function minus $n$ — and the Comparator-transported runHeight_defect_fib_sum_lower (Erdos249257/SternBrocotRunGeometry.lean). For every finite defect list $e$ , this theorem bounds the height of its positive Stern–Brocot run word from below by $(F_{r + 3} + F_{r + 1}) \cdot \sum e_{i}$ , where $r$ is the number of runs. These finite identities/inequalities do not establish analytic denominator survival or the unbounded family, so #249 remains open.
At every positive Stern–Brocot node $(a, b)$ , cylinderMass_split exactly decomposes the closed cylinder mass into the node’s stop mass and the two child-cylinder masses (Erdos249257/GcdMomentCalculus.lean). This telescoping recursion and its geometric interpretation do not establish denominator survival, irrationality, or novelty; the #249 endpoint remains open.
The same gcd-moment source gives the exact visible-coprime lattice normalization $\sum 1 / (2^{n} - 1) = 1$ over positive coprime pairs (tsum_pos_coprime_inv_mersenne_eq_one). It supplies the reduced-direction mass behind the fair-coin form of the totient constant, but is a rational normalization identity, not an irrationality result.
A newly executable #249 complement-noncancellation reduction is deliberately subordinate to the actual-LCM frontier. The exact finite Möbius-residue split finiteResidueDiagonal_eq_projectedForeign_add_divisor separates foreign and divisor channels, while abs_foreignTailWindow_le_foreignComplementBound gives each omitted stable window a closed geometric budget. The consumer scaleFullTarget_miss_of_projected_separation then rules out a full-target hit when ControlledForeignProjection holds and the projected state is farther from every integer than that budget (ExternalVerification/Challenge.lean:280-295; Erdos249257/ActualForeignResidueProjection.lean:276-417). The analytic bridge identifying the actual complement with this bound, and any unbounded separated-projection supply, remain unproved: this sharpens the reduction, not #249 irrationality.

#251 — is $\sum p_{n} / 2^{n}$ irrational?

Unconditional: $p_{n} \leq 1250 (n + 1)^{4}$ by an elementary argument, so the series is summable and equals $2 +$ the prime-gap dyadic series with no external input (ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:360, ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:379, ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:427); and for any sequence obeying the checked integer-digit dyadic tail recurrence, irrationality is exactly equivalent to cofinal non-integral tail shifts (irrational_initial_iff_cofinalNonintegralTailShifts, ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:1572) — the identification of the concrete prime tail with that recurrence is paper-level. Claims registry: prime_gap_unboundedness_and_nonperiodicity (unconditional progress), prime_gap_irrationality_equivalence (formalised here: Lean iff plus elementary polynomial summability, not PNT), and prime_gap_identity_tao (cited only: Tao, 7 October 2025). The actual prime-tail bridge remains open.
The Comparator-facing boundary is also explicit: exists_primeGap0_gt proves that consecutive prime gaps are unbounded, while irrational_tsum_primeDyadicTerm_iff_primeGap is the named iff under a Summable hypothesis; summable_primeDyadicTerm discharges that hypothesis by $p_{n} \leq 1250 (n + 1)^{4}$ . Unbounded coefficients and this equivalence alone prove irrationality of neither series.
A separate public Comparator transport makes the arithmetic boundary explicit. For a DyadicTailRecurrence, tailShift_integral_iff_den_dvd_mersenne and tailShift_integral_iff_two_pow_modEq_one classify an integral shift by the current reduced denominator and the congruence $2^{h} \equiv 1$ ; the source-level tailShift_integral_iff_scaledTail gives the equivalent integrality of $(2^{h} - 1) * T_{N}$ . The transported not_irrational_initial_iff_exists_eventually_integral_positive_tailShift says that an integer-digit dyadic tail is rational exactly when one positive shift is eventually integral, while irrational_initial_iff_all_positive_tailShifts_nonintegral gives the exact companion normal form: under the same real recurrence, every positive shift at every index is nonintegral (ExternalVerification/Challenge.lean:245-269; source ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:802-807,1279-1295,1525-1556). The classifications are abstract even though their normal form is now in the Comparator screen; they supply no prime-specific eventual-small or cofinal-mismatch producer.
The exact finite carry identity and non-eventual-periodicity theorem close the coefficient-only periodicity implication at the Lean level (carryPartialSum_natCast_eq, carryCoeff_natCast_not_eventually_periodic, ErdosProblems/Erdos251/PrimeGapDyadicTail.lean:1154-1173). The accompanying rational-sum countermodel is an authored paper-level inference from the endpoint decay using the standard exponential-dominance limit; the Comparator interface does not assert that infinite limit. Its coefficients are synthetic, not actual prime gaps, so this is a methodological no-go and not an unconditional #251 refutation.
A sparse congruence-preserving perturbation of the actual prime gaps can make the dyadic sum rational while retaining the prime growth scale, eventual fixed-modulus congruences, and short-block statistics at the stated scale. Lean checks the finite core, the sparse rational-target construction, and the growing-block transfer (SparseAmbientR9.lean, SparsePaperR11.lean, GrowingBlocksR11.lean). The support, interval and support-count bound precede the target; the formal congruence cutoffs follow it. The paper proves common congruence cutoffs for its different triple construction. Keep that quantifier distinction when citing Proposition 1.1; the source links do not verify every printed strengthening. The proposition has no Comparator entry, and there is no separately published SparseRationalisation.md. The later positions are not asserted to be prime, and the construction does not refute Land.
Open: cofinally many adjacent index pairs with small tail shifts and differing gaps; each smallness condition constrains a complete infinite tail.

#257 — is $\sum_{n \in A} 1 / (2^{n} - 1)$ irrational for every infinite $A$ ? (reviewed core)

Native unconditional: for every finite nonempty support $F$ of positive exponents and every base $b \geq 2$ , the reduced denominator of $\sum_{n \in F} 1 / (b^{n} - 1)$ is coprime to $b$ and has multiplicative order exactly $lcm F$ — finite_period_noncollapse (Comparator interface finite_period_noncollapse_rat_den_interface), Erdos249257/CertificateKernel.lean:5246, with no witness-supply hypothesis. Checked theorem; claims registry: finite_period_noncollapse (res:period). It is a finite-support denominator result, not an irrationality theorem for arbitrary infinite supports.
Formalised known results: the full-support series is irrational in every base $b \geq 2$ (Erdős 1948; claim eb_full_support), as are pairwise-coprime supports with summable reciprocals (Erdős 1968) and eventually periodic supports.
The committed Comparator interface irrational_erdosSupportSeries_pairwise_coprime makes the pairwise-coprime row exact: for every base $b \geq 2$ , infinite support $A$ , pairwise Nat.Coprime elements of $A$ , and summable reciprocal indicator Set.indicator A (fun a : ℕ => 1 / a), the support series erdosSupportSeries b A is irrational (Erdos249257/CertificateKernel.lean; independent statement wrapper in ExternalVerification/Challenge.lean). At base $2$ this is a dedicated non-dilation family inside #257, not the universal infinite-support claim.
Historical source boundary: Chowla’s 1947 paper defines the ordinary Lambert series $f (x) = \sum x^{n} / (1 - x^{n})$ and a sine-twisted companion, conjectures irrationality for both at nonzero rational arguments, but expressly says he cannot prove the ordinary $f (x)$ case. It proves only the sine-twisted $g (1 / t)$ case for integer $t \geq 5$ , via long zero blocks in sums of two squares (source closure). Thus Chowla is historical context for the full-support $x = 1 / 2$ Lambert value, not evidence for arbitrary-support #257 or a new release theorem.
A distinct periodic-support antecedent is due to Luca and Tachiya: for a nonzero purely periodic integer coefficient sequence, their Theorem A gives irrationality of the associated divisor-convolution Lambert value at every integer base with absolute value greater than one; their stronger Theorem 1 gives linear independence for nonnegative periodic coefficients, including full- and odd-support examples (source closure). The hypotheses are periodic and coefficient-specific, so this is not a theorem for arbitrary infinite supports and remains distinct from the release’s periodic-divisor certificate and mixed-sign boundary.
The base-2 Mersenne achievement set — all subsums of $\sum 1 / (2^{n} - 1)$ — is compact, perfect, totally disconnected, nowhere dense, and of Lebesgue measure one (strict-tail Cantor structure after Kovač–Tao, Remark 4.1; the measure clause is proved here; positive measure was asserted informally by Kovač on the erdosproblems.com #257 discussion page in August 2025, and no published source computes the exact value) — the Comparator theorem volume_mersenneAchievementSet, Erdos249257/GreedyAchievementSet.lean:996, Erdos249257/GreedyAchievementSet.lean:1633–1658; claim greedy_achievement_geometry. Membership of $1 / 2$ is equivalent to infinitely many greedy skips (Erdos249257/GreedyAchievementSet.lean:2527) and to the absence of a fatal half-gap (Erdos249257/HalfCutLocator.lean:654); the dyadic membership question was posed publicly by Kovač in the same discussion, and a positive answer would refute universal #257.
Historical topological source boundary: Kakeya’s 1914 paper proves perfectness for subsum sets of absolutely convergent real or complex series, gives the real interval enclosure, and states the exact term-versus- remaining-tail criterion for filling that interval. It also states nowhere density when the criterion fails, but explicitly leaves the “infinitely many failures” necessary-and-sufficient refinement unproved (source closure). This is classical subsum-set context only: it does not prove an arithmetic statement about Mersenne denominators, rational points, or universal #257.
The Comparator theorem seven_le_of_intBand_odd adds a local two-adic band exclusion: for positive odd integers $p$ , $D$ , and $q$ satisfying the stated IntBand inequalities, $7 \leq p$ (Erdos249257/HalfGreedyTwoThirdsBand.lean). Thus numerator classes $1$ , $3$ , and $5$ are excluded in that band, while $p = 7$ is sharp. The theorem does not show that an actual half-greedy orbit reaches or avoids the band, and does not decide half-membership.
A newly transported conditional reduction makes the rational-support boundary concrete: if the support has a positive seed and its base-2 value is $p / (2^{c} \cdot v)$ with $v > 0$ , then a positive natural shifted-tail state exists with the exact binary recurrence and modular orbit (exists_shifted_odd_tail_nat_states_of_support_fraction, Erdos249257/RationalSupportCarrySkeleton.lean). This exposes structure under a rationality hypothesis; it does not exclude rational infinite supports or settle universal #257.
For a support restriction $J$ , the transported measure dichotomy volume_supportedMersenneAchievementSet_dichotomy (ErdosProblems/Erdos257/MersenneSubseriesRigidity.lean) gives exact measure ((2 : ℝ≥0∞) ^ F.card)⁻¹ when J = (↑F)ᶜ for a finite $F$ , or measure zero when Jᶜ is infinite. This classifies the restricted achievement-set measure, not its rational points, so it does not settle universal #257.
A separate unconditional composite-dilation identity now exposes the lower-rank defect rather than hiding it in a prime-only adapter: supportCoeff_mul_eq_add_defect (Erdos249257/CompositeDilationDefect.lean). For $a \in A$ , $0 < a$ , and $0 < x$ , it states supportCoeff A (a·x) = supportCoeff A x + (if a ∣ x then 0 else 1) + compositeDilationDefect A a x. The exact defect is not bounded for arbitrary supports and supplies no tail selector or irrationality theorem; the separate bouquet budget remains conditional on its structural hypotheses.
Methodological: a formalised squarefree-support no-go theorem is shown to be an artefact of normalisation — adjoining $1$ to the support shifts the value by a rational and flips the divisor-incidence parity, and the finite-change principle is itself checked (ErdosProblems/Erdos257/SquarefreeSupportIncidence.lean:94, ErdosProblems/Erdos257/SquarefreeSupportIncidence.lean:111, ErdosProblems/Erdos257/SquarefreeSupportIncidence.lean:140; Erdos249257/CertificateKernel.lean:9467, Erdos249257/CertificateKernel.lean:9476). The squarefree value itself is settled at power-of-two bases in the literature (Duverney–Tachiya 2019; cited, not formalised). Registry: none.
Open: universal #257, and the $1 / 2$ and $1 / 21$ memberships.

#269 — are reciprocal sums of running lcms irrational?

For every pair of distinct primes, both the de-duplicated and the repeated running-lcm reciprocal sums are transcendental by a paper argument using Loxton–van der Poorten 1977, quoted in the modern Bugeaud–Laurent form (Theorem 1.1). Lean checks the exact affine and quadratic formulas and derives transcendence under the explicit BugeaudLaurentTranscendence hypothesis; the cited external theorem itself is not formalised (TwoPrimeSums.lean). Independently found and not first: the same reduction and conclusion were posted by Steve Fan on the erdosproblems.com #269 discussion page on 26 June 2026, before the note was finalised, with follow-ups there extending it to arbitrary coprime pairs; the note acknowledges this.
Lean-checked: the exact Comparator interface smoothPrefixLcm_eq_threePrimeHeight states that, for primes $p$ , $q$ , and $r$ with $p \neq q$ , $p \neq r$ , $q \neq r$ , and $x \neq 0$ , the running lcm of the three-prime smooth prefix is exactly threePrimeHeight p q r x (ErdosProblems/Erdos269/ThreePrimeRunningLcm.lean:123; formalisation of a classical identity). The same source also gives the four-letter block alphabet ${2, 6, 10, 30}$ (ErdosProblems/Erdos269/ThreePrimeRunningLcm.lean:699), and a rank-two kernel obstruction (ErdosProblems/Erdos269/ThreePrimeRunningLcm.lean:479, ErdosProblems/Erdos269/ThreePrimeRunningLcm.lean:721): the Comparator theorem kernel_235_minor_eq_neg_one_fifteen identifies the smallest displayed $2, 3, 5$ kernel minor as exactly $- 1 / 15$ . This rules out the displayed rank-one route only; it does not imply irrationality. The stronger arbitrary-order minor and finite-nonseparation theorems are proved in KernelCarryRank.lean, whose exact source bytes belong to the successfully compiled public closure in the Wave-A validation record. That record’s named axiom audit covers the Wave-A declarations; it is not a separate rank-declaration audit. Comparator covers the finite minor, not the arbitrary-order theorem. The paper gives the threshold-column proof.
Open: any three-prime case. The actual-series reduction is given; the source-specific cofinal escape remains unproved.
The finite residue contradiction and conditional cofinal-window carry extinction are indexed as three_prime_finite_residue_contradiction and three_prime_cofinal_window_carry_extinction in docs/claims.json, with paper routes res:consumer and res:windowconsumer.
A separate Comparator-transported family in ErdosProblems/Erdos269/WeightedPhaseCarry.lean keeps one coherent observer mechanism visible. For B : ℤ with $0 < B$ and the displayed carry recurrence, carry_eq_residueDigit_add_coboundary gives the exact residue-digit plus integral-quotient-coboundary identity (WeightedPhaseCarry.lean:109); carryResidue_mem_interval and residueDigit_mem_interval give the finite intervals under their explicit positivity and canonical-reduction hypotheses (:150, :157). The separate finite_realisedSpan_of_factorisation theorem gives finite-dimensional realised span only for DivisionRing modules with finite-dimensional observer space and an explicit linear factorisation realise = readout.comp C (:334). The quotient coboundary remains uncontrolled: no finite-state quotient, literal infinite realised span, scalar-evaluation implication, or #269 rationality/irrationality conclusion follows. This is now Comparator-transported evidence, with the same boundary, and is distinct from the three-prime cell, rank-two no-go, and conditional carry-escape families.
A separate typed consumer makes the conditional carry-escape boundary concrete: no_positive_reducedCarry_of_cofinalLocalWindowEscape derives False from CofinalLocalWindowEscape, $B > 0$ , Nat.Coprime B 30, positivity of an integer-valued carry, the exact multiplier recurrence, and its denominator-dependent short bound (ExternalVerification/Challenge.lean:498-509; ErdosProblems/Erdos269/RestrictedFloorSum.lean:629-654). Its hard step is the cofinal window expansion against that bound. The actual-series reduction is given; the source-specific cofinal escape remains unproved, so this is no #269 endpoint or irrationality proof; it is distinct from the finite residue and weighted-phase observers. #1041 — short connections inside polynomial lemniscates?
Lean-checked all-degree theorem: every monic trinomial $z^{n} + a z^{m} + b$ with roots in the open unit disc has each root-to-origin segment inside ${| f | < 1}$ , so any two roots join through the origin with length less than $2$ . This is coefficient-restricted, not a solution of the unrestricted path problem (PaperTrinomialWholeR21.lean).
Lean checks a sharp Chebyshev bound on a segment between collinear roots of a monic polynomial and the $< 2$ connector corollary for roots in the open unit disc (CollinearDiameterWhole.lean). A separate cubic shows that a first merger joining two roots need not give a normalised capacity gap; the Lean capacity clause assumes the named classical transfinite-diameter formula (ArityNotCapacity.lean).
Lean-checked sharp critical-value mean: for monic degree- $n \geq 2$ polynomials with zeros in the closed unit disc, $\sum_{j = 1}^{n - 1} | f (c_{j}) |^{2 / (n - 1)} \leq n - 1$ , with equality for $z^{n} - λ$ when $| λ | = 1$ , counting critical points with multiplicity. The complete theorem also gives $\sum | f (c_{j}) |^{1 / n} \leq (n - 1) R$ for roots in any closed disc of radius $R \geq 0$ . See paper_critical_value_mean and the successful source-bound audit, whose directly audited adapter is ReturnV5.critical_value_mean_exact_target. The paper supplies an ordinary proof too. These moment bounds alone do not construct a connecting curve or bound its length.
Ordinary separated-value connector theorem: let $f$ be monic of degree $n \geq 3$ , let $c$ be a simple critical point with $0 < | v | < 1$ , where $v = f (c)$ , and suppose some real $w_{0} \in [0, 1]$ satisfies $| f (d) / v - w_{0} | \geq 4 / 3$ for every other critical point $d$ . Then two roots have a connector of length $< 2$ inside ${| f | < 1}$ . The long paper gives the two-sheeted uniformization, Bergman length estimate and component-capacity argument; the numerical coefficient bound has a separate Lean kernel. No existence of such a separated critical-value disk is asserted.
Ordinary generic topology theorem: in a unit-sublevel component, simple critical points with nonzero critical values of pairwise distinct arguments and moduli give a slit-sheet tree of inverse-ray root connections. This identifies the topology on that stratum; it provides no uniform length bound and does not resolve simultaneous critical levels.
Lean checks supporting Newton-flow inputs: quantitative root retention under constant perturbation (constant_perturbation_roots_in_unitDisk, ErdosProblems/Erdos1041/NewtonFlowRaySeparation.lean:287) and arbitrarily small translations separating all pairwise ray arguments. More precisely, exists_small_translation_separating_arguments gives every finite injective complex family, for each $ε > 0$ , a common shift of norm $< ε$ making every value nonzero and every positive-ray argument distinct (:197). The exponential-decay connection equation is a hypothesis of the local ray-separation consumer, not a theorem (:315).
A Cassini example refutes the printed global tree budget of a March 2026 manuscript’s Proposition 12; that obstruction is not a disproof of Erdős #1041. The source-only frontier records hub selection on the ray-separated locus as a parent carrier; by its Corollary G the carrier fails in degree seven, so only degree-restricted versions stay open (research_corpus/Erdos1041/FRONTIER.md).
Checked counterexample: using the explicit degree-seven polynomial of erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure greater than two. The path-image case refutes the exact Formal Conjectures statement, and the separate total-variation bound remains checked. The formal proof covers one polynomial, not ani’s reported small-parameter family. Independent human review of correspondence with the 1958 curve-length wording remains open.
Current-source boundary: the committed research_corpus/Erdos1041/FRONTIER.md is the dated route for later source-only research evidence. Read it before the generated STRONGEST_RESULTS.json: it records certified refutations of several proposed strategies, surviving carriers, and the gaps open at that snapshot. It predates the checked total-variation counterexample and is not the owner of the current #1041 status. These rows are not reviewed claim entries, peer review, priority, novelty, or significance findings; the frontier itself flags priority/novelty as unchecked for named new rows.

#1049 — Lambert series at rational bases, beginning with $3 / 2$ ?

Checked exclusions at $3 / 2$ , each of one named mechanism only: the coordinatewise clearing scheme is impossible for all parameters (threeHalves_no_coordinatewiseCorridor, ErdosProblems/Erdos1049/RationalBaseLambert.lean:155), scalar content is neutral for the local-to-Archimedean balance, and unit endpoints exclude both $2$ and $3$ from a common divisor (ErdosProblems/Erdos1049/ZudilinConeArithmetic.lean:293). Claims registry: three_halves_coordinatewise_corridor_no_go (res:nocorridor) and rational_base_cleared_tail_recurrence (res:tailrec); both are exact formal boundaries. Separately, Lean constructs the polynomial forms and analytic estimates for the stated Zudilin contour region, then proves irrationality and an irrationality-exponent bound there, including $F ((31 / 4)^{r})$ for every positive integer $r$ (ErdosProblems/Erdos1049/PaperR17/SourceConsumers.lean). This formalises a known region; $3 / 2$ lies outside it.
The elementary height inequality used by Bundschuh–Väänänen’s external irrationality criterion at $7 / 2$ is checked (ErdosProblems/Erdos1049/RationalBaseLambert.lean:83); the analytic theorem itself remains external. Formalisation of known inputs.
A separate exact rational-base state recurrence is checked under $r \neq 0$ : rationalBaseClearedTailQ_succ gives $Q (N + 1) = r \cdot Q (N) - B \cdot coeff (N + 1) \cdot s^{N + 1}$ for the denominator-cleared tail state (ErdosProblems/Erdos1049/RationalBaseLambert.lean). The $s^{N + 1}$ forcing term records the denominator-base tax; this recurrence is not itself a rationality contradiction, so it yields no #1049 endpoint. The companion forcing bound is indexed as rational_base_forcing_growth (res:forcing): for $s \geq 2$ and positive data it gives a lower bound $2^{N + 1}$ , while $s = 1$ collapses exactly to $B \cdot coeff (N + 1)$ .
A distinct source-level four-jet/Padé obstruction is deferred outside the Comparator screen. When $0 < R$ and $4 R + 2 S \leq n$ , the four-jet target has cardinality $(3^{R})^{2} * (2^{S})^{2} < 2^{n}$ , forcing two distinct binary selectors to share a four-jet signature (ErdosProblems/Erdos1049/ZudilinConeArithmetic.lean:129-167). The accompanying Padé exterior determinants retain their row-content divisors (ErdosProblems/Erdos1049/RationalPadeArithmetic.lean:80-220), so the package exposes finite collision and content barriers without supplying an analytic remainder, nonvanishing, or irrationality theorem. It is distinct source evidence, not a Comparator result or an endpoint closure.
A source-faithful rectangular Hermite–Padé threshold family is now exposed through the external consumer. In the explicit two-function exponent model, $0 \leq ρ$ and $1 + ρ \leq σ$ imply hpClearedGap_nonpos and hpClearedGap_eq_zero_iff; equivalently, rectangular_hp_threshold_le_classical and rectangular_hp_threshold_eq_classical_iff give hpThreshold ≤ 1/2 − 1/π², with equality only at $(ρ, σ) = (0, 1)$ (ErdosProblems/Erdos1049/HermitePadeNoGo.lean:58-129; ExternalVerification/Challenge.lean:399-420). This is a sharp no-go for the displayed model, not a universal Padé result: no approximating polynomials or analytic remainders are constructed, and no #1049 irrationality conclusion follows.
The Van Assche moving diagonal fails the Amdeberhan–Zeilberger scalar recurrence already at $n = 0$ : its exact residual is $- p (p - 1)^{2} (p + 1) (p^{5} + 2 p^{4} + 2 p^{3} + 2 p^{2} + 2)$ , strictly negative for every real $p > 1$ (ErdosProblems/Erdos1049/QAperyDiagonalNonEquivalence.lean:67,94). This finite obstruction proves only non-transfer of that recurrence; it supplies no general recurrence, endpoint, lattice, valuation, denominator, or irrationality theorem. Claims registry: van_assche_qapery_diagonal_no_go; its source-bound ceiling is recurrence non-transfer at $n = 0$ , not an endpoint or irrationality result.
Open beyond the proved contour region: irrationality at $3 / 2$ ; the primitive noncollapsed construction; and analytic remainder control for that route. The short paper proves irrationality in Zudilin’s rational-base region, and the pinned Lean source checks rational_base_region, thirtyone_four_powers, and rational_base_measure. Those theorems do not cover $3 / 2$ .

The semantic corpus marks exactly eight statements candidate_new_statement — the only machine novelty marks in this release, against 5,505 of 6,089 statement nodes still not_assessed. They concentrate in the #249/#257 core (the totient Möbius-numerator normal form, a rank-one overshoot barrier, and the $1 / 2$ tail-escape and middle-producer family). Reproduce the list from docs/semantic_corpus.json.gz (statement_nodes[].prior_art_state); candidate status is a search outcome recorded for triage, not a novelty claim.

What is proved

Settled support families for Problem 257

The universal problem is open, but several infinite supports are settled. The formal source proves irrationality in every integer base $b \geq 2$ for the full support, factorials, powers of two, multiples of a fixed positive integer, residue classes, the odd numbers, eventually periodic supports, and pairwise coprime supports with summable reciprocals. The relevant declarations include:

irrational_erdosSum_full_support;
erdos257_family_factorial_instance and erdos257_family_two_pow_instance;
irrational_erdosSupportSeries_multiples, irrational_erdosSupportSeries_residueClass, and irrational_erdosSupportSeries_odd;
irrational_erdosSupportSeries_eventuallyPeriodic; and
irrational_erdosSupportSeries_pairwise_coprime.

These declarations are in Erdos249257/CertificateKernel.lean. The later reciprocal-summable, finite-prime weighted and mixed-support theorems remove some of these restrictions; their exact hypotheses appear in the programme summary. Cited prime and prime-power results retain their literature attribution.

A distinct second-layer rationality normal form is now a typed public consumer: exists_normalized_support_fraction_iff_exists_booleanMobiusCarry (ExternalVerification/Challenge.lean:363, source Erdos249257/BooleanMobiusCarry.lean:949). For p : ℤ and $q > 0$ , it is an existence-level equivalence between a support omitting $0$ , containing a positive index, and having value $p / q$ , and a map U : ℕ → ℤ with U 0 = p, positivity, the square-root bound $U N \leq q (2 \sqrt{N} + 4)$ , divisible carry differences, and a Boolean–Möbius quotient; the quotient reconstructs the support. This is genuinely distinct from the shifted-natural-tail state: it is quotient-level and reconstructs literal support. It is only a characterisation, not a contradiction or a universal irrationality theorem; it does not produce cofinally nonintegral shifts for the actual recurrence, settle arbitrary infinite support, or settle the $1 / 2$ membership boundary.

A separate Comparator-backed conditional row route makes the half-membership mechanism executable: under CofinalPositiveHalfGreedySkips, a positive rational-greedy remainder below the next Mersenne weight yields an exact local half row; cofinally many such skips give (1 / 2 : ℝ) ∈ mersenneAchievementSet (half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips, ExternalVerification/Challenge.lean:400, source Erdos249257/BooleanMobiusSkipRowCofinal.lean:22,73). The cofinal supply is unproved, and finite exact rows do not establish it, so this is a conditional counterexample route rather than an unconditional #257 result; it does not settle the universal problem.

A separate necessary-condition family controls coverage under a hypothetical rational support value. supportCoeffZeroWindow_length_le_eps_logb_add forces every zero window in the divisor-count coefficient to have length at most $ε \cdot \log_{2} (N + 1) + B$ ; the additive constant is built after the support and numerator, so it is not uniform across supports (SublogDivisorCoverage.lean:392; claims registry: sublog_zero_windows). This is a genuine restriction on a possible rational support, not a contradiction or a proof of universal #257.

The squarefree-support value is already known to be irrational at every power-of-two base $2^{j}$ by Duverney–Tachiya (2019, cited here, not formalised); their cited result does not decide the other integer bases. Its divisor incidence is proved to be $2^{ω (n)} - 1$ , hence odd at every $n \geq 2$ . The certificate engines in this development begin by selecting an even-incidence block, so they cannot act on that support at any block position. The checked declarations card_squarefreeDivisors, squarefreeIncidence_eq, and odd_squarefreeIncidence are in ErdosProblems/Erdos257/SquarefreeSupportIncidence.lean. This is a limitation of the named engines, not a statement about the value’s irrationality or the universal #257 question.

The reduction chain for the one-half test case of Problem 257

The Mersenne achievement set consists of subsums of $1 / (2^{n} - 1)$ . If $1 / 2$ belongs to it, its support gives an infinite set with a rational subseries, which would refute the universal statement in Problem 257. The repository does not prove this membership.

The chain includes the declarations below. Public CI does not compile the files cited here under ErdosProblems/Skip, Bit, Decl or Hlow; the two Erdos249257 files are in the default build.

half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite in Erdos249257/GreedyAchievementSet.lean: membership of $1 / 2$ is equivalent to infinitely many skips in its greedy expansion.
half_mem_mersenneAchievementSet_iff_unboundedTerminalFalse in Erdos249257/HalfCylinderHalfMembershipClassification.lean: the same membership is equivalent to terminal false bits beyond every bound.
half_mem_iff_unboundedLargestSkipLate in ErdosProblems/Skip/D2.lean: membership is equivalent to late largest skips beyond every bound.
exists_largestSkipLateAt_of_remainder_le_two_pow in ErdosProblems/Bit/R2.lean: a row with remainder at most $2^{N}$ produces a late largest skip in the explicit interval $[N + 1, 2 N + 1]$ .
half_mem_of_remainderReachesHalfPointCofinally in ErdosProblems/Bit/R2.lean: remainders at most $2^{s}$ cofinally are sufficient for membership.

The final two bullets are one-way sufficient criteria. They are not equivalences and are not known to hold cofinally.

The proposed universal hlow side condition is false: not_hlow_seven_five in ErdosProblems/Decl/D4.lean and not_hlow_of_hhigh in ErdosProblems/Hlow/H1.lean give the counterexample $(s, d) = (7, 5)$ . Its failure is useful rather than obstructive: seamRemainder_lt_two_pow_of_not_hlow and seven_is_a_hit_from_failure in ErdosProblems/Hlow/H2.lean convert that failure into a hit certificate.

Exact ranks for dyadic sections of Euler’s totient

For $j \geq 0$ and $0 \leq r < 2^{j}$ , let $φ_{j, r} (n) = φ (2^{j} n + r)$ . The family consisting of $φ_{0, 0}$ , $φ_{1, 0}$ , and all $φ_{j, r}$ with odd $r$ is a rational basis for the span of all dyadic sections. At level $e$ , the span has dimension exactly $2^{e} + 1$ .

Lean names and sources:

linearIndependent_oddCoreTotientKernelFamily, span_range_fullTotientKernel_eq_span_range_oddCore, and totientDyadicSectionBasis in Erdos249257/TotientMahlerDefect.lean;
finrank_canonicalTotientKernel_eq in the same file.

These are theorems about the coefficient sequence $φ$ . They do not prove that $\sum φ (n) / 2^{n}$ is irrational.

A finite diagonal certificate band for Problem 249

Let periodLcm t = lcm(1,…,t). The predicate certifiedKill h N L is a finite modular-arithmetic certificate showing that a specific binary totient-tail difference at shift $h$ and position $N$ is not an integer.

exists_diagonalKill_le_82 proves

for every t ≤ 82, there is an L such that
certifiedKill (periodLcm t) (periodLcm t) L.

Lean name and source:

exists_diagonalKill_le_82 — ErdosProblems/Skip/LadderT67.lean

The exact least depths at the new boundary scales are:

Scale $t$	Least depth $L$	Lean name	File
67	100	`t67_minimal_depth`	`ErdosProblems/Lift/Recon67.lean`
71	105	`t71_minimal_depth`	`ErdosProblems/Lift/CertT67.lean`
73	113	`t73_minimal_depth`	`ErdosProblems/Skip/LadderT67.lean`
79	120	`t79_minimal_depth`	`ErdosProblems/Skip/LadderT67.lean`
81	120	`t81_minimal_depth`	`ErdosProblems/Skip/LadderT67.lean`

The same file proves

periodLcm 79 = 32433859254793982911622772305630400,

a 35-digit modulus, as periodLcm_79_value.

The source-backed checked_diagonal_depth_roster.json covers all 33 distinct periodLcm scales whose plateaux fill the positive band $t \leq 82$ . Every recorded working depth lies $0 \dots 4$ above the arithmetic admissibility floor (median $1$ , mean $40 / 33$ ). Only the five boundary scales $t = 67, 71, 73, 79, 81$ have separate theorems proving their recorded depths least; for the other 28 scales, the excess is only an upper bound on the least-depth excess. Its reproducibility route is maintained with the other operational checks, not part of the mathematical claim.

This is a bounded result. The reduction for Problem 249 requires certificates at arbitrarily large scales. The theorem says nothing at $t = 83$ .

Finite off-diagonal certificates

The source-bound roster records 125 verified rows at positions not constrained to equal periodLcm t; “verified” is the lean_verified flag of the source log lean/ErdosProblems/FreePosition/data.jsonl. Two pairs of rows repeat the same $(h, N, L)$ triple, so the roster contains 123 distinct certificates matched to 123 public Lean theorems across 122 files. Public CI does not compile the ErdosProblems/FreePosition files. The source-bound reproduction plan in scripts/run_source_bound_reproduction.py includes a focused recompilation of FreeKill64OneHundredFifteenDI.lean; no receipt of a run is committed. Its largest recorded position is:

freeKill_64OneHundredFifteenDI :
  certifiedKill 1 135960691671824579163806583999 101

Source: ErdosProblems/FreePosition/FreeKill64OneHundredFifteenDI.lean.

The generated off_diagonal_certificate_roster.json retains all selected source rows and their hashes, identifies both duplicate groups, and binds each distinct triple to its exact theorem, line, and source hash. It is a navigation and evidence projection, not a replacement for the theorem statements.

The source log also contains 54 later verified certificate triples above the historical position cutoff. The roster exposes that excluded census without silently changing the historical result.

The relevant sufficient theorem for Problem 249 is irrational_totient_series_of_multiple_window_kill_supply in Erdos249257/CertificateKernel.lean. Its hypothesis requires, for every positive base shift and every lower bound on the position, a later certificate at some positive multiple of that shift. A finite list of 123 instances does not establish that quantified supply.

Direct Farey comparison

The denominator exclusion is exactly the standard Farey/mediant bound for the two committed finite windows. The arithmetic below was recomputed from

V_{K} = (\sum_{r = 1}^{K} φ (r + 1) 2^{K - r}) mod 2^{K}

and from the explicit neighbouring fractions in Erdos249257/GapFareyBound.lean.

$K$	Interval width	Delta
120	$123 / 2^{120}$	$0$
240	$243 / 2^{240}$	$0$

The exact denominators of each window are:

K = 120
  Farey neighbour denominators b, d   41326538792622579
                                      207345787569745331
  b+d-1                               248672326362367909
  formal exclusion bound              248672326362367909
  first failing denominator           248672326362367910

K = 240
  Farey neighbour denominators b, d   66013429300517684370587633721421187
                                      13626217346183690952768141154409867
  b+d-1                               79639646646701375323355774875831053
  formal exclusion bound              79639646646701375323355774875831053
  first failing denominator           79639646646701375323355774875831054

For each window, the recomputation gives determinant $1$ for the two neighbours, verifies both interval brackets, verifies the displayed bound, and verifies failure at the next denominator. The corresponding proved declarations are farey_gap, gap_check_window_1_120_le_248672326362367909, gap_check_window_1_120_first_failure, gap_check_window_1_240_le_79639646646701375323355774875831053, and gap_check_window_1_240_first_failure.

The division of credit is exact: Farey supplies the bound directly; formalisation supplies a checked arithmetic instance and proves it is sharp for that window. Neither finite window proves that the exclusion bounds are unbounded, so neither proves Erdős #249.

The magnitude is also a tunable window output, not an invariant measure of progress. scripts/check_farey_denominator_scaling.py independently reproduces the two formalised constants and cross-checks the producer by brute force on six small windows. On this run, choosing $K = 16000$ produced a 2,406-digit bound in $0.08$ seconds for the scaling row ( $0.18$ seconds for the complete script). Every fixed $K$ still gives only a finite exclusion, and increasing $K$ does not supply the unbounded theorem required by #249.

Scoped no-go theorems

These theorems rule out particular proof mechanisms. They do not rule out other arguments. Public CI compiles none of the Lift, Half, Rem, Three and Decl files cited in this list.

no_lift_from_lower_totient_data, ErdosProblems/Lift/AngleA5.lean — no universal lift of the displayed form can follow only from the stated lower totient data, pointwise bound, and a lower certificate.
no_window_local_lift, ErdosProblems/Lift/InduceLaw.lean — for prime multipliers $p \geq 3$ , agreement on the lower diagonal window does not force any certificate in the lifted window.
exists_certifiedKill_antitone, ErdosProblems/Lift/AngleA4.lean — a certificate at a larger position gives one at a smaller position; the implication runs opposite to a forward lift.
consecutiveFail_iff, ErdosProblems/Half/FreeWalk2.lean — under its explicit depth inequality, a run of $K$ failures at depth $L$ is equivalent to failure at depth $L + K$ at the base position.
no_absolute_bound_on_consecutive_failures, ErdosProblems/Half/FreeWalk1.lean — the abstract admissible-run model permits arbitrarily long failure runs under its stated budget.
exists_persistent_surplus_model, ErdosProblems/Rem/C1.lean — the listed row recurrence and ceiling inequalities admit a sequence that stays above the target forever.
rowLaw_blind_at_16, ErdosProblems/Rem/C1.lean — at one concrete row, every listed row-level trigger is silent although the next row has a late skip.
IntervalCeiling.four_pow_le, ErdosProblems/Three/T1.lean — every ceiling satisfying the stated branch-blind rank-recursion obligations must grow on the $4^{s}$ scale.
two_pow_mul_y, ErdosProblems/Three/T2.lean — the normalised state used in the doubling route is dyadic at every finite row.
exists_persistent_odd_surplus_model, ErdosProblems/Three/T3.lean — adding parity to the listed row-level constraints still admits a persistent surplus model.
PairCeiling.terminal_ge_of_splits, ErdosProblems/Decl/D1.lean — in the stated two-sided abstraction, a failed branch prediction forces the terminal upper bound above the target scale.

Other standalone exact obstructions

These five registry claims are not restatements of either endpoint. Each has a separate limitation, and none settles an Erdős problem.

Orbit-level carry anti-compression — the checked consumer not_irrational_totientSeries_implies_mod_period_and_unbounded_rank exposes one positive multiplier $v$ and tempered integral carry $u$ under hypothetical rationality: every dyadic section is eventually periodic modulo $v$ , while its canonical carry-kernel rank is at least $2^{e} - 1$ for every $e$ (ExternalVerification/Challenge.lean:137; Erdos249257/TotientTailCarryPeriod.lean:224). This is one orbit-level conjunction, not the coefficient-side rank-only family. Natural friction: modulo a divisor of $v$ , totient forcing disappears and $u$ is geometric, so quotient periodicity cannot yield a finite- $Q$ -rank upper bound. Boundary: necessary consequence of rationality only; no contradiction or #249 irrationality proof follows. Claims registry: totient_carry_kernel_anti_compression.
primitive_coordinate_index_obstruction — clearing $(φ * μ) (n) / n$ through level $N$ forces a two-tier primorial divisor; no fixed positive index clears every level. Boundary: finite Euler-coordinate obstruction, not an irrationality criterion.
lcm_factor_ideal_anchor_pulse_no_go — for every $t \geq 3$ , a synthetic survivor satisfies the factor-ideal and whole-ray-anchor constraints and survives every finite integer shift polynomial. Boundary: its letters need not be actual totient differences; nonlinear fresh-divisor arguments remain possible.
reciprocal_mass_bound — a rational support value with odd denominator part $v$ forces reciprocal mass at least $1 / {ord}_{v} (2)$ , or divergence; a dyadic-rational infinite support forces divergence or mass greater than one. Boundary: does not exclude every rational value.
unbounded_carry_states — every infinite support with rational series value has an unbounded positive carry state. Boundary: rules out finite-state interpretations, not rationality itself.

Their registry identifiers lead to the declarations and current source coordinates; operational lookup details live in the agent workbench.

Current relation and residual routes

Cross-paper conjectures and reductions are not assigned a score from a frozen #249/#257 sample. Use python3 scripts/query_semantic.py node <node_id> for one current statement, python3 scripts/query_semantic.py family-relations <family_id> for its registered family relationships, and scripts/residual_evaluator.py when a proposed reduction needs a kernel-backed comparison with its target. Public claim status and exact registered Lean interfaces remain owned by docs/claims.json and python3 scripts/query_corpus.py --claim <claim_id>.

Finite evidence policy

A finite measurement belongs on this page only when the release preserves its sample identities, executable owner and rerunnable validation route. Historical scans without that chain are omitted; a prose summary is not a substitute for the missing evidence. Current registered finite-evidence claims are reached through python3 scripts/query_corpus.py --overview --format card and their emitted source and receipt handles.

Historical corrections retained in source

The current Lean module headers and declarations retain the operative boundaries. Public CI compiles none of the files listed below. The principal corrections were:

Lift/AngleB2.lean no longer says that the survivor set is empty. Its theorem is conditional on a false hcof instance at each surviving class and on an unobserved seamExcess = 2 hypothesis.
Lift/AngleB3.lean no longer presents ratchetOrbit_above_universal_barrier as a live universal barrier. Its intended hypothesis fails at the initial row, and the proved nonrecurrence result covers only offsets $b \geq Q + 2$ , not offsets $1, \dots, 9$ . The file now uses an actual Lean bridge to Recon257.
Skip/D1.lean and Skip/Wire1-3.lean no longer claim to exclude residue classes. Their existential threshold exceeds every case admitted by their own hypotheses, and the same unobserved seam-excess premise remains.
Rem/C6.lean no longer says the residual invariant is empirically true on $s = 6, \dots, 3000$ . It is false at $(13, 7)$ .
Rem/C3.lean now distinguishes the branch it proved from the branch it only measured at the time, and points to Three/T2.lean, where the latter branch was subsequently proved.
Bit/R2.lean labels badRun_pins_remainder as a conditional statement with no observed instance: it needs at least 12 consecutive bad rows, while the measured maximum was 3.
Three/T4.lean and Bit/Corr1.lean no longer call hlow open. It is false at $(7, 5)$ , and that failure supplies a hit certificate.

No theorem was weakened or removed to make these corrections. The claims were narrowed to the theorem types and the recorded counterexamples.

What is open

Exact questions for a human expert

The validated handoffs form a bounded set of exact questions. Each requested input is OPEN; the consumer named under each question is a checked theorem. The classification matters: the first question is the endpoint in exact normal form, the next two are sufficient analytic producers for #249, and the last two would produce a counterexample to universal #257 rather than prove its positive statement. Their complete packets are indexed from the agent workbench.

No checked strictly weaker handoff currently implies the universal positive statement of #257 for every infinite support. Named support families, half-value analysis, reciprocal-mass bounds, and sublogarithmic zero-window constraints are partial; treating any one as a universal proof route would overstate what its checked consumer establishes.

The packet does not make an expert start cold. Every ask also carries a low-confidence current hypothesis, enumerated alternatives, current evidence, and the observation or theorem that would distinguish them; both are recorded with each question below.

`XQ249-lcm-diagonal-supply` — diagonal supply

Exact OPEN input: for every $t_{0}$ , find $t \geq t_{0}$ and $L$ with a diagonal certificate at $(lcm (1, \dots, t), lcm (1, \dots, t))$ .

Payoff and boundary: equivalent to #249. A proof closes #249; until then this is a restatement, not intermediate progress.

Current working guess: certificates occur beyond every scale, equivalently #249 is true.

Evidence that would change the guess: a rational representation or an eventual-failure theorem decides the opposite branch. The exact rectangle has first-depth excess $0 \dots 11$ ; across all 33 distinct checked diagonal scales covering $t \leq 82$ , working-depth excess is $0 \dots 4$ (median $1$ , mean $40 / 33$ ). Only five diagonal depths are proved least, and finite low upper bounds neither prove bounded excess nor decide the cofinal quantifier.

PROVED consumer:

irrational_totient_series_iff_lcm_diagonal_certificate_supply

`XQ249-pivot-decorrelation` — pivot decorrelation

Exact OPEN input: cofinally supply the exact four pivot budgets: centred real correlation $\leq 14 X / 25$ , supplier mean and bad-supplier norms $\leq X / 100$ each, and non-supplier norm $\leq 8 X / 25$ , with overlap $h \leq L - s$ and room $16 (2 X + h + L + 2) \leq 2^{L}$ .

Payoff and boundary: sufficient for #249. The missing input is a prime-distribution or residual-decorrelation estimate, not another certificate reformulation.

Current working guess: for every shift, fixed $s, η$ permit cofinally many blocks satisfying overlap, room, and all four budgets; the centred real term is likely the hard budget.

Evidence that would change the guess: exact failure requires one shift for which every $s, η$ eventually loses at least one clause. Infinitely many bad blocks do not suffice. An exact four-budget producer proves #249.

PROVED consumer:

irrational_totient_series_of_pivotResidualDecorrelation

`XQ249-adjacent-phase-separation` — adjacent phases

Exact OPEN input: for every $h > 0$ and $X_{0}$ , find $X \geq max (X_{0}, 1)$ , a depth $L$ , and adjacent $N, N + 1 \in [X, 2 X)$ such that $16 (2 X + h + L + 2) \leq 2^{L}$ and their first-harmonic phases have squared chordal separation at least $19 / 25$ .

Payoff and boundary: sufficient for #249. Finite scans or average separation do not meet the cofinal quantifiers.

Current working guess: qualifying adjacent separation occurs cofinally for every shift.

Evidence that would change the guess: one shift and a cutoff beyond which no admissible block, depth and adjacent pair reaches $19 / 25$ kill this route; infinitely many bad blocks alone do not. A cofinal adjacent-discrepancy theorem at that threshold proves #249.

PROVED consumer:

irrational_totient_series_of_adjacentPhaseSeparation

`XQ257-second-channel-separation` — second channel

Exact OPEN input: prove HalfSecondChannelSeparatedRat n for every $n \geq 7$ , i.e. that the exact rational second-channel phase stays at least $1 / 6 + (37 / 56) 2^{- n}$ from $1 / 3$ ; Lean checks $1, \dots, 6$ , and an independent exact probe finds no failure through $n = 1000$ .

Payoff and boundary: proves $1 / 2$ attainable. The finite-support exclusion then forces the witness to be infinite, giving a rational counterexample to universal #257. The finite probe does not move the quantifier; failure of this route would not prove universal #257.

Current working guess: the separation continues for all $n \geq 7$ ; confidence remains low despite an empty exact failure set on $1 \leq n \leq 1000$ .

Evidence that would change the guess: the least measured margin on the open range is $1033253069 / 8193024$ at $n = 7$ , but $n = 1001$ onward is unmeasured. One failed level closes only this socket; a global reachability invariant or uniform sign estimate proves membership and, with finite-support exclusion, a counterexample.

PROVED consumers:

half_mem_mersenneAchievementSet_of_secondChannelSeparationRat_from_seven
positiveMersenneSupportValue_coe_finset_ne_half
positiveMersenneSupportValue_eq_erdosSupportSeries

The source-bound second-channel measurement re-evaluates the rational greedy recurrence and the complete failure set for $1 \leq n \leq 1000$ from the definitions in Erdos249257/GreedyAchievementSet.lean. The generated artifact is docs/measurements/second_channel_separation_probe.json. Its status is MEASURED, not PROVED; in particular, the empty finite failure set does not establish the all- $n$ hypothesis consumed by the Lean theorem.

`XQ257-middle-producer-tail-escape` — middle producer

Exact OPEN input: at every actual middle transition from rank $13$ , write $C$ for the checked producer carry and $Θ$ for its nonnegative coefficient tail. Prove $C = - 3$ or $(1 \leq C and Θ < C)$ .

Payoff and boundary: also proves $1 / 2$ attainable; at the putative last-false row the checked $- 3$ theorem removes the first disjunct, and the finite-support exclusion then forces an infinite witness. The socket must exclude every actual $C \leq 0$ , $C \neq - 3$ , and control $Θ < C$ for every positive cell.

Current working guess: every actual middle row lies in the $C = - 3$ branch or has $1 \leq C$ and $Θ < C$ .

Evidence that would change the guess: one actual nonpositive cell other than $- 3$ , or one positive cell with $Θ \geq C$ , refutes this socket. A proof of the displayed disjunction at every actual row proves membership; the final $- 2$ sieve alone does not.

PROVED consumers:

half_mem_mersenneAchievementSet_of_middleProducerTailEscapeExceptNegThree
positiveMersenneSupportValue_coe_finset_ne_half
positiveMersenneSupportValue_eq_erdosSupportSeries

Cold-reader review boundary

The repository cannot certify its own human legibility. It therefore exposes a second OPEN question: can an independent reader, starting from a fresh clone, recover the current eight-problem scope, authority and #1041 credit boundary in at most ten minutes? The request is exact, including the response schema, its consumer, payoff, and boundary.

The reader replays the current overview, #1041 and semantic-relation routes; reports that ani’s degree-seven counterexample refutes the exact Formal Conjectures path-image-length statement and the total-variation formulation, while the historical curve-length correspondence remains unreviewed; identifies the claim registry as selected rather than exhaustive; and summarises checked results from at least three distinct problems. This replaces the retired protocol built around a frozen #249/#257 binder sample.

A structurally accepted response from an identified independent reader returns an explicit rubric for its result summaries, evidence paths and verdict. A second identified evaluator binds a final review to the response digest. The validator cannot authenticate either person or the elapsed time, and does not pretend to judge free prose by itself. Neither receipt validates the mathematics or establishes priority or novelty. The same query without a domain filter returns this systems question beside the five theorem-connected mathematical questions; respondent-facing output omits the evaluator’s scalar answer key.

Erdős Problem 249

The irrationality of

\sum_{n \geq 1} φ (n) / 2^{n}

is not proved in this release; Lean proves it from one open bound, a real part at most $603 X / 1000$ for the first-harmonic sum over the good indices at arbitrarily large $X$ (irrational_totient_series_of_goodBase_gap). The short paper proves all-base finite-level rank $k^{e} + 1$ for $k \geq 2, e \geq 1$ , with canonical integral coordinates and all integral relations; at prime base the rank is exponential in the level $e$ . A rational $5 / 4$ control agreeing with totient on odd arguments has tempered carry rank at least $2^{e} - 1$ at every depth, so a generic rationality-driven carry-rank ceiling is false, and that control is distinct from the bounded $3 / 2$ parity-and-aperiodicity analysis. The finite band through $t = 82$ and the 123 historical off-diagonal certificates do not supply a cofinal diagonal or an all-ray seed. Coons non-regularity, Martin affine independence, and Yazdani–Shallit CRT–Dirichlet separation are credited antecedents, not new claims of this release.

Erdős Problem 257

The statement that

\sum_{n \in A} 1 / (2^{n} - 1)

is irrational for every infinite $A$ is open. In particular, membership of $1 / 2$ in the Mersenne achievement set is not proved.

At level $d$ , the rational compared with the remaining tail changes with $d$ . A naive common-denominator construction gives an upper height bound of the form $2^{O (d^{2})}$ , but the repository proves neither a matching lower bound nor a Theta(d^2) law for the reduced denominator along the actual greedy support. The displayed separation boundary has an explicit correction proportional to $2^{- d}$ . No registered theorem controls the required sign uniformly at this moving boundary, and there is no fixed rational approximation target to which a fixed-number theorem applies directly.

Irrationality alone is insufficient because the open branch asks for the sign of a nonzero tail difference, not merely for non-equality.

Verification and continuation

The exact build, query, replay, contribution, and source-bound reproduction routes are maintained in the agent workbench, where they can stay current without interrupting the mathematical account here. The historical isolated-tree timings were a dated manual record, not a machine-revalidated receipt for the present source tree. Lean checks certify the displayed formal statements; they do not certify novelty, priority, significance, or the still-open Erdős endpoints.

Problem statements, verification and status

Questions generated from docs/problem_index_source.json.

Problem	Question
#68	Is the series sum_{n >= 2} 1/(n! - 1) irrational?
#243	Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually?
#249	Is the binary Lambert series sum phi(n)/2^n irrational?
#251	Is the dyadic series of consecutive primes irrational? Equivalently, is the corresponding consecutive-prime-gap dyadic series irrational?
#257	Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational?
#269	For a finite set of at least two primes, is the sum of reciprocals of the running least common multiples of the smooth numbers irrational? This library treats the three-prime case.
#1041	Must two roots of a monic polynomial in the open unit disc be joined by a sub-two-length curve inside its unit lemniscate? Ani’s degree-seven example refutes the exact Formal Conjectures statement; correspondence with the 1958 wording awaits human review.
#1049	For which rational bases is the corresponding series irrational? The first resistant explicit base is three halves.

The questions above are readable here: no query is required, and this page does not require a private repository. The problem papers explain the eight questions. Scope records the public claim boundaries and status labels; external verification lists the selected Comparator interfaces, axioms and replay limits. The claim registry owns source identity and current status. These are generated from their owners.

The claim registry pins the immutable formal-source checkpoint; this is not a new tagged release. Its release tag is the latest tagged release and citation anchor, kept separate from the source currently under validation.

What the formal source establishes

Farey’s method supplies the number directly; it is not an improvement on the classical bound.

The labels describe evidence. Formalised here means known mathematics rendered and kernel-checked in Lean; it makes no priority claim. Proved here means the argument is this project’s. Unconditional progress marks a theorem that does not settle the open problem and asserts neither novelty nor prior knowledge. Verified finite instance means Lean checked only the listed inputs; conditional reduction means the conclusion depends on a named open condition.

Status	Result
formalised here	For every integer $b \geq 2$ , the full-support series $\sum 1 / (b^{n} - 1)$ is irrational; Erdős (1948) is a checked rendering rather than a new result. Several named infinite-support families are also formalised; this does not cover every infinite support.
formalised here	The base-2 Mersenne achievement set is compact, perfect, totally disconnected, nowhere dense, and has Lebesgue measure one. Membership is equivalent to greedy survival at every level.
proved here	For the #257 test value $1 / 2$ , achievement-set membership is equivalent to infinitely many greedy skips and would produce an infinite support of rational sum, refuting universal #257. Under the last-skip schema’s hypotheses (a rank floor, a carry condition, and a strict middle-cell inequality), the upper branch and the middle coordinate $- 3$ are impossible.
conditional reduction	Within that same last-skip contradiction schema, the two still-unexcluded middle coordinates, $- 2$ and $- 1$ , would also be ruled out if one current contribution were larger than the sum of all later possible contributions. That inequality is not proved.
formalised here	The dyadic sections of Euler’s totient have an explicit rational basis; for $e \geq 1$ the level- $e$ span has dimension exactly $2^{e} + 1$ . The Lean proof is an independent constructive route to an independence consequence of Martin’s stronger theorem; this is a theorem about the coefficient sequence, not the irrationality of $S$ .
unconditional progress	For every integer $k \geq 2$ , the sections through level $e \geq 1$ have rank $k^{e} + 1$ , with an explicit basis and complete scalar relation normal form. AllBaseTotientKernel.lean proves canonical-family independence by CRT and Dirichlet, and the complete rank theorem discharges the reusable conditional wrapper’s independence premise. Martin’s broader affine-independence theorem remains an external antecedent, not an axiom of that Lean proof.
formalised here	Applying the classical Farey/mediant bound directly to the committed $K = 240$ interval excludes rational denominators through $79 639 646 646 701 375 323 355 774 875 831 053$ (about $7.96 \times 10^{34}$ ). This is exactly the Farey bound, not an improvement on it; Lean also checks that the next denominator fails this finite window.
proved here	$S$ is irrational exactly when every positive binary tail difference is non-integral, equivalently when every fixed pair has a finite certificate. Finishing the argument would require certificates at arbitrarily large stages; that step is not proved.
verified finite instance	Lean proves a diagonal certificate at every $t \leq 82$ . Historical free-position audit: 125 verified log rows represent 123 distinct off-diagonal $(h, N, L)$ certificates in 122 Lean files. This finite evidence does not prove successful cases beyond every fixed cutoff.

Other exact mathematics in the corpus

Package	Exact checked content	Boundary
Fair-coin coprimality	$S = 1 / 2 + P (gcd (X, Y) = 1)$ for independent $P (X = n) = 2^{- n}$ .	Irrationality remains open.
Squared-Lambert gcd moments	Two exact divisor-sum identities for squared Lambert denominators.	No transfer to the open Möbius row.
Stern–Brocot cylinder law	Exact stop/child splitting; depth error at most $(2 / 3)^{d}$ .	Probability law, not irrationality.
Fibonacci/continuant run stability	Height at least $F_{r + 3}$ with exact defect expansion.	No analytic denominator-clearing theorem.
Tempered binary tail rigidity	Exact rationality/carry-orbit classification for $c (n) \leq n$ .	Needs problem-specific orbit control.
Exact Möbius-shadow denominator	Exact reduced denominator and an explicit divisor lower bound.	No unbounded avoidance supply.
Scalar-localisation height obstruction	If `H ∣ x.den` and `(c·x).den ∣ H`, then `x.den/H ∣ \|c\|`.	Local obstruction only.

Typed routes expose sources: probabilistic_gcd_geometry for the first four rows, boolean_mobius_constraints for tail rigidity, and arithmetic_obstruction_interfaces for the last two. Orientation also lists eventually-periodic nonnegative weighted irrationality, a signed irrational-or-base-terminating dichotomy, five binary-carry criteria/consequences, and two scoped #249 no-go countermodels. Five further obstructions are stated with their limits in RESULTS.

An exact final-skip band formula does not show that the actual orbit avoids an unsafe band.

Orientation routes claims; the retained mathematics paper preserves the joint #249/#257 exposition.

What remains open

Each problem’s section in the problem-by-problem guide states its own open questions. For the two problems with working records:

Prove that $S = \sum φ (n) / 2^{n}$ is irrational without placing a bound on a possible rational denominator.
Prove the single #249 bound: for every shift, a real part at most $603 X / 1000$ for the first-harmonic sum over the good indices at arbitrarily large $X$ , which Lean turns into irrationality.
Produce the unbounded certificate supply required by the exact #249 reduction.
Prove irrationality of $\sum_{n \in A} 1 / (2^{n} - 1)$ for every infinite $A \subseteq N$ , rather than only the named support families formalised here.

The #249 and #257 working records each close with a section titled “The wall”: every attempted argument class is stopped by a stated bound, recorded with what it does not rule out.

docs/SCOPE.md is the short boundary statement. The exact expert handoffs state what input is requested, current guess, alternatives, discriminating evidence, checked consumer, and endpoint-or-counterexample boundary. See RESULTS and python3 scripts/query_expert_handoffs.py. A refuted route is withdrawn in the next edition and the refutation credited.

Results and limits

The short version

Problem-by-problem guide

Technical verdict

Signal-audit dispositions

Strongest checked results by problem

What is proved

Settled support families for Problem 257

The reduction chain for the one-half test case of Problem 257

Exact ranks for dyadic sections of Euler’s totient

A finite diagonal certificate band for Problem 249

Finite off-diagonal certificates

Direct Farey comparison

Scoped no-go theorems

Other standalone exact obstructions

Current relation and residual routes

Finite evidence policy

Historical corrections retained in source

What is open

Exact questions for a human expert

XQ249-lcm-diagonal-supply — diagonal supply

XQ249-pivot-decorrelation — pivot decorrelation

XQ249-adjacent-phase-separation — adjacent phases

XQ257-second-channel-separation — second channel

XQ257-middle-producer-tail-escape — middle producer

Cold-reader review boundary

Erdős Problem 249

Erdős Problem 257

Verification and continuation

Problem statements, verification and status

What the formal source establishes

Other exact mathematics in the corpus

What remains open

`XQ249-lcm-diagonal-supply` — diagonal supply

`XQ249-pivot-decorrelation` — pivot decorrelation

`XQ249-adjacent-phase-separation` — adjacent phases

`XQ257-second-channel-separation` — second channel

`XQ257-middle-producer-tail-escape` — middle producer