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 ≤ 2.49×10¹⁷ (K=120) and q ≤ 7.96×10³⁴ (K=240).

Wave 18 — MersenneLambertLadder.lean

The Mersenne–Lambert ladder, machine-checked: the rational rungs L(μ)=1/2, L(φ)=2, the positive lift L(A)=S, and the Möbius-square lens S = 1/2 + ∑ μ(d)/(2^d−1)². Engine: a signed, linear-growth weighted Lambert rearrangement.

Wave 19 — GeometricCoprimality.lean

S as coprime-pair mass. #{(a,b) : a+b=n, 0<a, gcd(a,b)=1} = φ(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₂(f) = ∑ f(d)/(2^d−1)² = E[(f * ζ)(gcd(X,Y))], since gcd-divisibility factorises across independent coordinates. Yields L₂(μ) = S − 1/2, the gcd-moment ladder, and Pillai’s gcd-sum function.

Wave 21 — TotientTailPeriodKiller.lean

Period, not digits. Rationality of S forces the tail-period law R_{N+h} − R_N ∈ ℤ; 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) ≤ n, the binary series ∑ c(n)/2ⁿ is rational exactly when a tempered integer carry orbit exists (u(N+1) = 2·u(N) − v·c(N+1) with u(N)/2ᴺ → 0); every such orbit is rigid, equal to the scaled analytic tail v·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 ∑_{n∈A} 1/(2ⁿ−1)): strict superincreasing tail inequalities, the quantitative gap asymptotic (2/3)·4⁻ⁿ + O(8⁻ⁿ), 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) = #{a ∈ A : a ∣ n} satisfies f_A = 1_A * ζ and μ * 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 ∑_{a∈A} 1/a, the exact excess-mean identity, the rationality-forced lower bound 1/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 ε log₂(N+1) + B for every ε > 0, with B ≥ 0 obtained for that support and numerator. The proof builds B from ε, 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 (τ(n)^k ≤ (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 (Wang–Grau Ribas; 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.