Development index

Wave 17 — GapFareyBound.lean

Farey-gap denominator bounds. A mediant/Farey argument places any rational $m/q$ inside a forbidden gap, so no $q$ below the bound can represent $S$. Elementary and per-window; clears $q\le 2.49\times {10}^{17}$ ($K=120$) and $q\le 7.96\times {10}^{34}$ ($K=240$).

Wave 18 — MersenneLambertLadder.lean

The Mersenne–Lambert ladder, machine-checked: the rational rungs $L(\mu )=1/2$, $L(\phi )=2$, the positive lift $L(A)=S$, and the Möbius-square lens $S=1/2+\sum \mu (d)/(2^d-1{)}^2$. Engine: a signed, linear-growth weighted Lambert rearrangement.

Wave 19 — GeometricCoprimality.lean

$S$ as coprime-pair mass. $\mathrm{\#}\{(a,b):a+b=n,0<a,gcd(a,b)=1\}=\phi (n)$, so at $r=1/2$, $S-1/2=P(gcd(X,Y)=1)$ for independent fair-coin waiting times. Base 2 is the unique self-normalising point of the geometric law.

Wave 20 — GcdMomentCalculus.lean

The squared transform $L_2(f)=\sum f(d)/(2^d-1{)}^2=E[(f\ast \zeta )(gcd(X,Y))]$, since gcd-divisibility factorises across independent coordinates. Yields $L_2(\mu )=S-1/2$, the gcd-moment ladder, and Pillai’s gcd-sum function. The exact family return is the probabilistic gcd-geometry route: the totient gcd-moment declaration and the Stern–Brocot cylinder recursion, cylinder remainder bound, and run-stability declaration return to the paper’s probability-coordinate appendix, with the stable records res:directionnormalization, res:sternbrocotcylinders, and res:sternbrocotruns. The cylinder-law family is also directly recoverable through python3 scripts/query_corpus.py --claim stern_brocot_cylinder_law, which returns the probabilistic_gcd_geometry route and its source-fingerprinted resume handoff. These exact identities and combinatorial bounds do not close the open #249 irrationality or unbounded-certificate obligations.

Wave 21 — TotientTailPeriodKiller.lean

Period, not digits. Rationality of $S$ forces the tail-period law $R_{N+h}-R_N\in \mathbb{Z}$; missing that integer by a decidable margin is a finite “kill”. Reduction:

irrational_totient_series_of_certificate_supply

Wave 22 — CarrySurvivorExtinction.lean

Multiple-period collapse. Every multiple of a period is a period, so the obligation collapses onto the one-parameter family periodLcm t = lcm(1..t). Adds the carry-survivor orbit certificate (a bounded integer orbit that must escape a narrow strip).

Wave 23 — LcmDiagonalReduction.lean

Diagonal collapse. Standing on the ray (N = periodLcm t) removes the second parameter: #249 follows from one ℕ-indexed decidable sequence ∃ L, certifiedKill (periodLcm t) (periodLcm t) L holding infinitely often.

Wave 24 — LcmConeFlatness.lean

Cone-flatness law. Rationality forces one fractional constant on the whole lcm cone {k·periodLcm t}. Certificate completeness: a kill exists iff the tail difference is a non-integer:

exists_certifiedKill_iff_tail_diff_notMem_int

Plus rank-2 second-difference certificates.

Wave 25 — LcmConeNonflat.lean

Cone non-flatness refuter. Interrogates a whole menu of cone vertices at once: if their one-sided arcs shared a common fractional part, the minimal-deep-tail vertex would be a common endpoint, and its certificate row denies exactly that. Sharper than pairwise; genuinely joint for menus of size ≥ 3.

GenericTailOrbitRigidity

Depends on CertificateKernel.

For coefficients $c(n)\le n$, the binary series $\sum c(n)/2^n$ is rational exactly when a tempered integer carry orbit exists ($u(N+1)=2\cdot u(N)-v\cdot c(N+1)$ with $u(N)/2^N\to 0$); every such orbit is rigid, equal to the scaled analytic tail $v\cdot T_c(N)$. Balanced pulses also prove unbounded exact successor fan-out, ruling out a generic autonomous finite-state decoder.

Main theorems:

temperedBinaryOrbit_eq_scaledTail
binaryCoeffSeries_rational_iff_exists_temperedBinaryOrbit
balancedPulse_no_autonomous_decoder

GreedyAchievementSet

Depends on CertificateKernel.

Greedy geometry for the Mersenne achievement set (values $\sum _{n\in A}1/(2^n-1)$): strict superincreasing tail inequalities, the quantitative gap asymptotic $(2/3)\cdot 4^{-n}+O(8^{-n})$, compact/perfect/totally-disconnected/nowhere-dense structure with Lebesgue measure one, exact real and rational greedy recurrences, membership ⇔ all-level greedy survival, sound one-sided finite rational death certificates (the exact level-one certificate excludes $3/4$), and uniqueness of normalised support coding. Certificates prove nonmembership only.

Main theorems:

volume_mersenneAchievementSet
isNowhereDense_mersenneAchievementSet
mem_mersenneAchievementSet_iff_greedy_survival
certifiedGreedyMersenneDeath_not_mem

BooleanMobiusCarry

Depends on GenericTailOrbitRigidity.

Boolean–Möbius carry coordinates for support series: the Lambert coefficient $f_A(n)=\mathrm{\#}\{a\in A:a\mid n\}$ satisfies $f_A=1_A\ast \zeta$ and $\mu \ast f_A=1_A$ on positive integers; rationality of the support series is equivalent to a tempered carry orbit whose carry quotient is exactly $f_A$; normalised nonempty supports with value $p/q$ correspond exactly to quotient-only Boolean Möbius carry certificates. The displayed value $1/2$ has a canonical affine-orbit criterion. Worked support $\{2,3\}$: value $10/21$, period-six orbit $10,20,19,17,13,26$.

Main theorems:

erdosSupportSeries_rational_iff_exists_temperedCarry
exists_normalized_support_fraction_iff_exists_booleanMobiusCarry
support_half_iff_affineBinaryOrbit_tempered

RationalSupportCarrySkeleton

Depends on BooleanMobiusCarry.

Residue wraps and reciprocal mass: the binary repetend identity (least positive residues in a complete doubling cycle sum to odd modulus × number of wraps), an algebraic one-wrap classification, the Cesàro identification of mean support tails with the reciprocal mass $\sum _{a\in A}1/a$, the exact excess-mean identity, the rationality-forced lower bound $1/{\mathrm{ord}}_v(2)$ on reciprocal mass, the dyadic strengthening (mass divergent or $>1$ for infinite dyadic-rational supports), and global unboundedness of the positive carry state attached to any infinite support with rational value.

Main theorems:

sum_doublingResidue_eq_mul_wrapCount
one_div_oddOrder_le_reciprocalMass_of_support_fraction
dyadic_support_fraction_reciprocalMass_diverges_or_gt_one
exists_unbounded_shifted_odd_tail_nat_state_of_support_fraction

SublogDivisorCoverage

Depends on RationalSupportCarrySkeleton.

Sublogarithmic divisor coverage. If an Erdős support series has a rational value, consecutive zero windows in its divisor-count coefficient $f_A$ have length at most $\epsilon {\log }_2(N+1)+B$ for every $\epsilon >0$, with $B\ge 0$ obtained for that support and numerator. The proof builds $B$ from $\epsilon$, $c$ and $v$, but the support and numerator are bound before the existential, so this declaration does not export one constant uniform across all supports. The proof composes an explicit fixed-power divisor bound ($\tau (n{)}^k\le (k^{2^k}{)}^{k}n$), a binary-tail estimate, and the exact carry recurrence. This constrains support coverage; it does not solve universal #257.

Main theorem:

supportCoeffZeroWindow_length_le_eps_logb_add

None of these modules claims a solution of Erdős #249 or #257. The contribution boundary is theorem-family-specific: the carry recurrence and strict-tail geometry have direct prior art (Han Wang; Kovač–Tao); Möbius inversion, repetend algebra, and divisor averaging are classical; the converse/rigidity, certificate-normal-form, and coupled reciprocal-mass families remain exact-source-comparison candidates. No priority claim is made.

SupportSunflowerDichotomy is an adjacent conditional #257 route. It gives the exact carry conversion for finite-core orthogonal-petal bouquets and records an explicit alternating-core squared-prime-petal support. Its uniform tail-selection hypothesis is not proved, so it adds no unconditional support family.

CompositeDilationDefect supplies the exact finite correction when a composite support element dilates the divisor-count coefficient, and bounds that correction for orthogonal-petal bouquets. It is a local identity, not a correlation or irrationality theorem.

MaximalOmegaLayer extends the one-prime-power identity to two distinct prime-power layers. It records finite coefficient algebra only, with no bounded-Ω or irrationality endpoint.