Prior art

Browse all source credits

The source attribution index connects named literature, public Erdős Problems contributions, and software sources to exact paper and Lean locations. It includes anonymous credit for implemented private advice until the correspondent confirms public naming. The machine-readable view records citation coverage, source locators, content digests, and unresolved matches; the authored registry owns the credit decisions. These records complement the principal-source comparisons below and the separate accepted-contribution receipts in Research Commons.

Bounded comparison route

Start with python3 scripts/query_corpus.py --route trace_prior_art, then select the exact local claim with python3 scripts/query_corpus.py --claim <claim_id>. Read its registry status, statement, assumptions, remaining-open links, and Lean declarations before interpreting any row below. A status such as proved here or formalised here is an evidence statement, not a novelty statement.

For a theorem-level comparison, record the source statement, assumptions, conclusion, specialisation map, proof mechanism, and residual difference against that selected local claim. Failure to identify a matching source is not evidence of novelty. Lean source checked by the pinned Lean kernel remains proof authority; this bibliography and its search history are authored attribution evidence only.

Erdős #249: attribution update, 16 September 2026

The finite-level result is an explicit basis, rank $k^e+1$ for $k\ge2,e\ge1$, and an integral basis of all relations among the totient sections. Coons’s non-regularity theorem and Martin’s affine-independence theorem are antecedents, not new claims of this release. For composite bases the retained condition is $k\nmid r$.

Yazdani’s Theorem 2 and proof (2001, pp. 652–653) use CRT–Dirichlet separation and explicitly credit Shallit; this is the method antecedent of the evaluation-matrix proof. Yazdani’s Corollary 4 (p. 654) already gives non-automaticity of totient residues modulo every m≥3 in every base. Allouche–Shallit–Yassawi’s survey (published 2022; arXiv v1 2021, Theorem 3, Example 4 and Remark 7) explains that result. Wong’s earlier base-equals-modulus theorem remains credited.

Residue series, adjudicated 28 September 2026. The first assertion of the short paper’s residue theorem (res:residueseries: $\sum_{n\ge1}(\varphi(n)\bmod m)2^{-n}\notin\mathbb Q$ for every $m\ge3$) is implied, in every integer base $t\ge2$, by Erdős 1957 (Indag. Math. 19, 212–219). His Lemma 1 (printed p. 213) makes $\sum_k a_kt^{-k}$ irrational when the integers $a_k\ge0$ have bounded averages and infinitely many, but density-zero, nonzero terms; Erdős states it as known and notes that it is the case $b_k=0$ of his Lemma 4 (stated pp. 215–216, proved pp. 216–218). The least residue $\varphi(n)\bmod m$ is nonzero only when $n$ has no prime factor $p\equiv1\pmod m$, a set of density zero since $\sum_{p\equiv1\,(m)}1/p$ diverges, and equals $m-2$ at every prime $p\equiv-1\pmod m$. Lemma 4′ (p. 218, proof omitted by Erdős) and Theorem 3 of Kaneko–Suzuki–Tachiya (arXiv:2601.20743v1, PDF p. 5; they prove Lemma 4′ as their Theorem A, pp. 2 and 18) give the same. The same criteria cover the dyadic classification (the theorem’s second assertion), its integer-base form (long record prop:radixresidue) and the finite-dilation independence (prop:dilations) only when the relevant values $f(r)-f(0)$, or relation coefficients, have one sign; with both signs Lemmas 4 and 4′ and KST Theorem 3 need a spacing condition on the negative terms, which was not checked. The isolated-coefficient proof in the papers needs none. KST Theorem 3 with $b=0$ also gives the irrational direction of the long record’s slowly-growing-modulus dichotomy (prop:slowmoduli, ordinary proof), subject to a density bound for $n$ with small $v_2(\varphi(n))$ that the record does not write out. No novelty claim is made for the residue-series irrationality; the papers cite Erdős 1957 and KST at the result. Page references are to the Rényi scan of Erdős 1957 and to the KST PDF recorded in its source closure.

Bell–Smertnig (2026 preprint, Theorem 1.3) proves that a characteristic-zero Mahler series with multiplicative coefficients is regular, and explicitly excludes the totient series from every Mahler base. Bell–Bruin–Coons (2012, Theorems 1.5–1.6) supplies the earlier algebraic and D-finite classification context. These are generating-function statements, not proofs about the value at 1/2. Adamczewski–Drmota–Müllner (2022; arXiv v2 2021, Theorem 1.4 and Remark 1.5) provides the automatic-prime density context, with local conditions rather than unconditional positive density for every state.

Primary sources: Yazdani; Allouche–Shallit–Yassawi; Bell–Smertnig; Bell–Bruin–Coons; Adamczewski–Drmota–Müllner; Martin. No priority claim for the local normal form is certified by this comparison.

Principal sources

Each entry gives the source, then its relationship to this release, then the boundary of that relationship.

• P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory (1980) (read source closure); P. Erdős, On the irrationality of certain series: problems and results (1988) (Renyi scan; read source closure)

  The 1980 monograph records the full-support divisor Lambert value $\sum_{n\ge1}d(n)/2^n$ as irrational (printed p. 61), states that the analogous binary totient series could not then be proved irrational (p. 61), and identifies the full-support Mersenne identity $\sum_{n\ge1}(2^n-1)^{-1}=\sum_{n\ge1}d(n)/2^n$ (p. 62). It also records the squarefree reciprocal question as open (p. 63). Erdős’s 1988 article, printed p. 105, explicitly asks whether every increasing support gives an irrational $\sum_k(2^{n_k}-1)^{-1}$; its density/LCM irrationality theorem is a separate result on pp. 106–108.

  Boundary. The 1980 full-support identity and the 1988 p. 105 subseries statement do not prove universal #257; the separate LCM theorem does not automatically apply to Mersenne denominators. The 1980 source explicitly leaves the binary totient irrationality question unresolved, so neither source proves #249, the release’s Lean, Comparator, Palomar, geometry, finite-certificate, or totient-kernel claims.

• S. Chowla, On Series of the Lambert Type which assume Irrational Values for Rational Values of the Argument (1947) (read source closure)

  Historical conjectural predecessor: its rational-argument Lambert question contains the full-support specialisation $x=1/b$.

  Boundary. Chowla’s source is a conjecture in this relation, not the proof source; the theorem formalised here is credited to Erdős (1948).

• P. Erdős, On arithmetical properties of Lambert series (1948) (read source closure)

  Full-support divisor row. Printed p. 63 states irrationality of $f(1/t)=\sum _{r\ge 1}d(r)/t^r$ for every integer $|t|>1$, the Erdős–Borwein divisor-weighted Lambert theorem used for the full-support row.

  Boundary. Printed p. 66 explicitly says the analogous Euler-totient series $\sum \phi (n)/t^n$ “seem[s] to present difficulties.” This source therefore does not support irrationality of the #249 totient series, any totient-kernel rank/basis, or the release’s Lean/Comparator claims; no novelty or priority claim is made.

• P. Erdős, On the irrationality of certain series (Math. Student 36, 1968) (read source closure)

  Pairwise-coprime support theorem. Printed p. 222 states that if $n_1<n_2<\dots$ are pairwise coprime and $\sum 1/n_i<\mathrm{\infty }$, then $\sum _{i}1/(t^{n_i}-1)$ is irrational for every integer $t\ge 2$; the proof occupies printed pp. 223–225.

  Boundary. Printed p. 222 says the pairwise-coprimality condition can be removed only by more complicated arguments and gives no details, and that $\sum 1/n_i<\mathrm{\infty }$ could be replaced by an unstated weaker but more complicated condition; printed p. 226 suggests $\sum _{n_i<x}1/n_i=o(\log \log x)$ via Brun’s method for pairwise coprime supports and says the all-primes case is not handled. The source therefore states the coprimality-free reciprocal-summable extension without proof; the #257 note credits that stated extension to Erdős and gives a complete proof of it. The source does not settle universal #257 or supply the release’s Lean/Comparator proofs, and the note does not identify Erdős’s unstated weaker condition with its weighted criterion. No novelty or priority claim is made.

• D. Duverney and Y. Tachiya, Refinement of the Chowla–Erdős method and linear independence of certain Lambert series (2019) (author preprint; read source closure)

  Squarefree-support antecedent. Corollary 1.2 (PDF p. 4; proof pp. 10–11), specialised to $E$ equal to the primes, $s=2$, ell=1, and $q=2$, proves linear independence of $1$ and the squarefree Lambert values at bases $2^j$; Example 1.1 displays the family using |mu(n)|.

  Averaging antecedent. The proof of Theorem 1.1 (Section 2, (2.3)–(2.9), PDF pp. 5–6) selects its index by averaging a local coefficient mass over an arithmetic progression and taking a term attaining the minimum. The #257 note cites this after its weighted-support theorem as the antecedent of the selection step in its displacement averaging.

  Boundary. The condition $|q|L\le s$, a product with L = lcm(1,...,ell), is essential to this specialisation, so the result does not give squarefree irrationality at every integer base and does not settle universal #257. With s = infinity it covers the perfect $i$th-power supports at every integer base. It also does not prove the release’s Lean, Comparator, Palomar, geometry, or totient-kernel claims; no novelty or priority claim is made.

• P. B. Borwein, On the irrationality of ∑ 1/(q^n+r) (1991) (publisher record; read source closure)

  Fixed-base rational-offset antecedent. Theorem 4 (printed pp. 257–258) proves that ∑ 1/(q^n+r) is irrational and not a Liouville number when q is an integer greater than one and r is a nonzero rational avoiding the denominator zeros r = -q^n for n ≥ 1. The paper’s Padé/Stieltjes construction is the direct source for this full-support family.

  Boundary. The result is for every positive index with an integer base; it does not settle arbitrary infinite supports, the release’s rational noninteger-base claim at $3/2$, universal #257, or the release’s Lean results. Its recurrence and Padé estimates are not the Amdeberhan–Zeilberger q-WZ operator, and no novelty or priority claim is made.

• P. B. Borwein, On the irrationality of certain series (1992) (author PDF; read source closure)

  Full-support antecedent. Theorems 1 and 2 (printed pp. 142 and 145; proof pp. 142–146) prove irrationality, and non-Liouville behavior, for the full-support series $\sum_{n\ge1}(q^n+c)^{-1}$ and its alternating variant under their stated integer/rational hypotheses. Theorem 1 with $q=2$, $c=-1$ contains the full-support Mersenne–Lambert specialization.

  Boundary. The paper sums over every positive index, not an arbitrary infinite support, so it does not settle universal #257, prime-support or squarefree subseries, or the release’s #249 reductions. Its contour-integral proof is not formalised here; no novelty or priority claim is made.

• H. Kaneko, Y. Suzuki, and Y. Tachiya, Refinements of Erdős’s irrationality criterion for certain sparse infinite series (2026) (read source closure)

  Nearby current work proving irrationality for sparse series such as $\sum d(n)^k/t^{\varphi(n)}$.

  Averaged-tail antecedent for #257. The quantity $R_c(q,x,z)$ of (1.7) (PDF p. 3) and Lemmas 1–2 (PDF pp. 6–8) derive irrationality from scaled tails that are small on average. The #257 note cites them beside its weighted-support theorem. There the divisor-incidence coefficients are positive on every multiple of $\min A$, so the scaled tail is at least the series value and the note averages the displacement instead.

  Residue-series antecedent for #249. Theorem 3 (PDF p. 5), with $b=0$, implies the irrationality of $\sum_{n\ge1}(\varphi(n)\bmod m)t^{-n}$ for every $m\ge3$ and integer $t\ge2$, because these coefficients are bounded and nonzero only on a set of density zero; Theorem A (p. 2, proof p. 18) is Erdős’s 1957 Lemma 4′. The #249 papers cite this beside the residue theorem; see the adjudication under the #249 attribution update above.

  Boundary. Here $\varphi(n)$ occurs in the exponent. It does not treat the coefficient-weighted constant $\sum\varphi(n)/2^n$, its denominator bound, or its tail-certificate equivalence. The counting hypotheses of Theorems 1 and 3 fail for divisor-incidence coefficients, so these criteria do not apply to Mersenne–Lambert subseries.

• P. Erdős, On the irrationality of certain series (Indag. Math. 19 (1957), 212–219)

  Residue-series antecedent for #249. Lemma 1 (printed p. 213), the case $b_k=0$ of Lemma 4 (pp. 215–218), gives irrationality of $\sum a_kt^{-k}$ for nonnegative integers with bounded averages and infinitely many but density-zero nonzero terms, and hence of $\sum(\varphi(n)\bmod m)t^{-n}$ for every $m\ge3$ and integer $t\ge2$. Lemma 4′ (p. 218) is stated without proof.

  Boundary. The paper’s Theorem 1 concerns $\sum 1/t^{\varphi(n)}$ and $\sum1/t^{\sigma(n)}$, with the arithmetic function in the exponent; its introduction (printed p. 212) says the author cannot prove irrationality of $\sum\varphi(n)/t^n$. It does not prove #249, the dyadic classification with mixed-sign values, the finite-dilation independence with mixed-sign relations, or any Lean or Comparator claim. No source closure file or local copy is recorded in this pass.

• T. M. Apostol, Introduction to Analytic Number Theory (1976); M. Merca, The Lambert series factorization theorem (2017); M. Merca and M. D. Schmidt, Generating Special Arithmetic Functions by Lambert Series Factorizations (2019) (official journal PDF; read source closure)

  Apostol supplies the classical Dirichlet/Möbius background; Merca gives the modern factorisation theorem and Merca–Schmidt its synthesis/unification treatment. Merca–Schmidt’s equation (2) records the totient Lambert identity used as transform background, while Theorem 3.2 and Corollary 3.3 give their partition/inverse-matrix mechanism. Apostol/Merca 2017 remain cited background without a source closure in this pass.

  Boundary. The release uses classical transforms and claims a Lean-checked composition, not new Möbius inversion, Lambert identities, or the cited factorisation theorems.

• Y. V. Nesterenko, Modular functions and transcendence questions (1996) (read source closure)

  Direct source for the cited-only transcendence of the divisor-sum ladder rung $L(\mathrm{Id})=\sum_{m\geq1}\sigma(m)/2^m$.

  Boundary. This positions one ladder row only; no part of its modular-transcendence proof is formalised here.

• K. Postelmans and W. Van Assche, Irrationality of $\zeta_q(1)$ and $\zeta_q(2)$ (2007) (read source closure)

  Primary source for the cited-only linear independence of $1,\zeta_q(1),\zeta_q(2)$ when $q^{-1}$ is an integer of absolute value greater than one. At $q=1/2$, this implies the irrationality of the squared-ladder value $L_2(\mathbf1)=\zeta_{1/2}(2)-\zeta_{1/2}(1)$.

  Boundary. The release formalises the identity placing $L_2(\mathbf1)$ in this q-zeta family, not the Hermite–Padé proof. Linear independence of the constant-weight row gives no irrationality transfer to the Möbius row $L_2(\mu)=S-1/2$, which remains open.

• S. Kakeya, On the Set of Partial Sums of an Infinite Series (1914) (read source closure)

  Classical strict-tail criterion for subsum sets: domination of every remaining tail by its term gives the Cantor-set regime.

  Boundary. The release uses this as historical geometry, not as a claim that Kakeya supplied the local executable machinery.

• V. Kovač and T. Tao, On several irrationality problems for Ahmes series (2025) (read source closure)

  Fixed-base strict-tail antecedent. Their Remark 4.1 (PDF p. 13) verifies $\sum_{\ell>n}(t^\ell-1)^{-1}<(t^n-1)^{-1}$ for every integer $t\ge2$, and deduces distinct Lambert subsums and a Cantor set. Their Theorem 2.3 (PDF p. 5; proof pp. 13–14) separately constructs rational merged sums from several bases under a mass hypothesis.

  Boundary. At $t=2$ the strict-tail remark supplies the known Mersenne geometry, but it does not assert a measure formula. The multi-base theorem allows repeated terms and is not a fixed-base counterexample. The release now formalises compactness, perfection, total disconnectedness, nowhere density, and measure one as well as the two-scale gap, greedy interface, and finite death certificates. It makes no novelty claim for those refinements, and Kovač–Tao explicitly leave the universal fixed-base subseries question open; none of these results settles #257.

• M. Coons, (Non)Automaticity of number theoretic functions (Journal de Théorie des Nombres de Bordeaux 22 (2010), no. 2, 339–352) (official PDF; read source closure)

  Global totient-kernel boundary. Coons’s Theorem 3.2, stated on printed p. 348 and proved on p. 349, shows that Euler’s totient function is not $k$-regular for any $k\ge2$, using the Dirichlet-series identity $\sum_{n\ge1}\varphi(n)n^{-s}=\zeta(s-1)/\zeta(s)$ and the pole-counting criterion of Corollary 3.1. This is the prior-art source for the release’s global non-finite-generation context; it does not state the finite-level rank, explicit basis, or relation normal form proved or discussed locally.

  Boundary. For integer-valued sequences, finite generation of the $\mathbb Z$-module generated by the kernel is equivalent to finite dimension of its rational span: if the span has dimension $d$, some $d$ evaluations embed it in $\mathbb Q^d$ and the module in $\mathbb Z^d$. The #249 short note states this in §1, so the infinite-dimensionality of the totient-kernel span is Coons’s theorem in another form, and the exact ranks recover it. Coons does not prove the release’s Lean declarations, dyadic rank $2^e+1$, CRT–Dirichlet–determinant construction, or Erdős Problem #249. No novelty or priority claim is made for either the cited theorem or the local finite-level results.

• M. Coons, Regular sequences and the joint spectral radius (International Journal of Foundations of Computer Science 28 (2017), no. 2, 135–140) (arXiv:1511.07535; read source closure)

  Basis versus spanning family for regular sequences. For a $k$-regular sequence, Theorem 1 identifies the growth exponent with the base-$k$ logarithm of the joint spectral radius of matrices associated to a basis of the kernel span; Proposition 4 gives the upper bound for any spanning set, Corollary 7 compares the two, and the example after it shows that a redundant spanning set can overestimate. Appendix A shows that the evaluation vectors of a basis of sequences span the coefficient space. The #249 short note cites these results for the basis-versus-spanning-family distinction and for the evaluation argument in the equivalence above.

  Boundary. The source concerns regular sequences and does not mention Euler’s totient, which is not regular, so its growth theorem is not applied to the totient. It does not state the release’s finite-level basis, ranks, section-map description, relation module, or Lean declarations. Statement numbers follow arXiv:1511.07535v1. No novelty or priority claim is made.

• J. Farey, On a Curious Property of Vulgar Fractions (1816)

  Historical source for the Farey language. The standard neighbouring-fraction/mediant lemma is the method that directly produces the finite #249 denominator bound: for the committed interval it gives $b+d-1$, exactly the formal bound.

  Boundary. The mathematical method and denominator estimate are classical. The local contribution is a kernel-checked arithmetic instance and proof that $b+d$ is the first failure for each selected window; the improvement over the classical Farey bound is zero.

• G. Martin, Simultaneous inequalities among values of the Euler phi-function (arXiv:math/0603053, 2006) (read source closure)

  Subsuming source for affine-totient ratio comparisons. His Theorem 1 assumes only that the slopes $a_i$ are positive integers and that $a_ib_j\neq a_jb_i$, and proves that for every $C>0$ the simultaneous ratio gaps $\varphi(a_1n+b_1)/\varphi(a_2n+b_2)>C,\ldots$ hold on a set of positive lower density; the symmetry discussion supplies strict ordering patterns. For the local all-base argument it is an earlier source that already implies the affine-totient independence, which the release proves separately; the finite dyadic Lean theorem remains separately formalised, not a theorem directly stated by Martin. His Corollary 4 transfers Theorem 1 and Corollaries 2–3 to $\sigma$.

  Boundary. The release’s dyadic Lean independence result is separately formalised from this broader comparison input by a finite CRT–Dirichlet–determinant argument; Martin does not present the release’s Lean statement or proof. The all-base paper theorem proves its affine independence by a determinant that is diagonal modulo an auxiliary prime, built with the Chinese remainder theorem and Dirichlet’s theorem, and cites Martin’s Theorem 1 as an earlier source that already implies that independence. Lean proves the all-base independence, the exact rank $k^e+1$ for $k\ge 2$ and $e\ge 1$, and the explicit basis unconditionally in AllBaseTotientKernel.lean; it does not formalise Martin’s positive-density theorem, which is not an input of that proof. Martin needs neither odd slopes, nor primitivity, nor a residue bound, and concludes strictly more. A $\sigma$ analogue would likewise not be new. Exact-title, DOI and venue searches did not locate a separate journal publication, so this is cited as a public preprint.

• F. Luca and Y. Tachiya, Irrationality of Lambert series associated with a periodic sequence (2014) (read source closure)

  Direct antecedent for the eventually-periodic coefficient family. Their rational-coefficient theorem contains the indicator-support case and the nonnegative rational weights formalised here.

  Boundary. Their theorem is broader, and its Chowla–Erdős/large-modulus-prime proof is separate. This release uses a periodic-divisor certificate route. For signed integer weights it proves only an irrational-or-base-terminating dichotomy; it does not exclude the terminating alternative in general or claim the full mixed-sign theorem.

• T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers (arXiv v2, 2026) (read source closure)

  Direct source for the cited-only irrationality of the prime-support series: Theorem 1.3, equation (1.7), on PDF p. 4, with proof on pp. 44–56. It gives the $\sum_n\omega(n)/2^n = \sum_p(2^p-1)^{-1}$ formulation and this release’s separately formalised identity bridge.

  Boundary. It settles the prime-support family at base 2, not universal #257. The source only says that other integer bases and the prime-power variant can be treated by modifications and leaves those details to the reader; its quantitative correlation proof is not formalised here.

• H. Wang, Sparse Polynomial-Weighted Expansions (arXiv:2606.24972v4, 2026) (read source closure)

  Direct antecedent for the rationality-forced integral carry recurrence in the weighted-binary special case (c(n)=n d_n).

  Boundary. The public generic criterion is a formalisation/abstraction; its converse and rigidity make no priority claim. The source’s positive-density theorem and Erdős #260 corollary are neither used nor formalised here.

• R. Crandall, The googol-th bit of the Erdős–Borwein constant (2012); J. M. Campbell, On the binary digits of the Erdős–Borwein constant (arXiv, 2026)

  Adjacent work on binary digits of the full-support constant; Campbell resolves Crandall’s question on infinitely many occurrences of the block $11$.

  Boundary. Neither result is formalised or used by this release, and neither changes its irrationality or open-problem claims.

Expansion-note principal sources (#68, #243, #251, #269, #1041, #1049)

The same contract as above applies: relationship, not proof authority, and no row widens a release claim. Each source below is load-bearing for exactly the stated use in its problem note, where the full statement-level comparison is recorded.

Entries carry the same three parts as above — source, relationship, boundary — grouped by the problem whose note they serve.

Provisional theorem-specific comparisons

These local rows come after the direct antecedents on purpose. They record dated searches and residual comparisons; failure to identify a closer theorem is not a novelty result.

Each entry names the local package, the comparison this release recorded for it, and the boundary of that comparison.

• The complete tail-certificate normal form. The comparison search covered the original problem sources, Erdős’s and Borwein’s Lambert-series theorems, periodic-coefficient results, and current arithmetic-function series literature. No theorem with the same pointwise certificate equivalence was identified as of 16 July 2026. The finite denominator number is deliberately excluded because it is obtained directly by the classical Farey/mediant method.

  Boundary. This is a dated search result, not a priority or novelty theorem. A closer antecedent should replace it if one is found.

• Finite-difference and affine-moment transport. General algebraic techniques are applied here to exact Möbius residue kernels and totient-tail windows. The primary-source search found no cited theorem matching the combined curvature, prime-jump, anchored $(3,5)$, or fixed-precision no-go statements.

  Boundary. Absence of an identified match is not a novelty claim. The release claims only the pinned Lean theorems and keeps the open supply hypotheses explicit.

• First-harmonic and large-prime pivot reductions. The additive-character step and $\varphi(mp)=\varphi(m)(p-1)$ use standard ingredients; Apostol supplies the arithmetic background. The local statement is the four-term supplier-fibre decomposition, its one-sided $14/25,1/100,1/100,8/25$ budget, and its composition with certificate completeness.

  Boundary. No matching combined theorem is recorded, but no prime-distribution or residual-decorrelation estimate populating the four budgets is proved.

• Reduced-direction, Stern–Brocot cylinder, and continuant-run package. The direct sources above supply the classical divisor/Möbius, mediant, and adjacent squared-Lambert settings. The release proves an exact Mersenne-weight probability normalization, a telescoping cylinder law with uniform geometric error, and sharp Fibonacci/continuant run estimates.

  Boundary. No priority claim is made. The run estimates have no endpoint consumer, and matching Fibonacci and denominator scales does not prove denominator survival or irrationality of $S$.

• Exact $1/2$-membership, fatal-gap, and last-producer package. The strict-tail source above gives the global subsum geometry. The maintained search found no source stating the exact equivalence between $1/2$-membership, infinitely many greedy skips, cofinal false seam terminals, and absence of a last skip, nor the surviving middle-producer future-tail condition.

  Boundary. This is provisional positioning, not a novelty assertion. Positive membership would refute universal #257; nonmembership would decide only this test value.

Audit rule for new sources

Add a public citation only when the source can be tied to a named statement, method, or historical formulation in the release. Before describing a source as an antecedent of a local theorem family, record the exact statement comparison: assumptions, conclusion, specialisation map, proof mechanism, and the remaining delta. Otherwise, retain it as private research context rather than turning a bibliographic lead into a public priority claim.