For any $d\ge 1$ and $k\ge 0$ let $P(d,k)$ be the set of integers which are the sum of distinct powers $d^i$ with $i\ge k$. Let $3\le d_1<d_2<\cdots <d_r$ be integers such that$$\sum _{1\le i\le r}\frac{1}{d_r-1}\ge 1.$$Can all sufficiently large integers be written as a sum of the shape ${\sum }_i{c}_i{a}_i$ where $c_i\in \{0,1\}$ and $a_i\in P(d_i,0)$? If we further have $\gcd (d_1,\dots ,d_r)=1$ then, for any $k\ge 1$, can all sufficiently large integers be written as a sum of the shape ${\sum }_i{c}_i{a}_i$ where $c_i\in \{0,1\}$ and $a_i\in P(d_i,k)$?

attempted via frontier 'sidon/B2' (transfer_strength=weak) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'weak'. Do not re-attack cold; needs a new idea or richer accumulated context.

Erdos #124: lean/Vela/Erdos124IntervalBlock.lean kernel-verifies the interval-block criterion that underlies the GPT-Pro reduction (att_61ff8f87c2f692b0). interval_block: if PB is L-syndetic (every length-L window meets it), PF contains the L consecutive integers u..u+L-1, and PB+PF subset PS, then PS contains every n >= u+L; interval_block_eventually gives the cofinite (atTop) form. Instantiated with PB=Sigma(B), PF=Sigma(F), PS=Sigma(B union F) for a disjoint split, this turns the open #124 target (erdos124.ne_zero) into the interval-block lemma. The interval-block lemma itself (existence of such a split for every admissible finite D,k) is the open core and is NOT proved here. Build green; axioms = {propext, Quot.sound} (+Classical.choice for the atTop form); no sorry.

{"lean_file":"lean/Vela/Erdos124IntervalBlock.lean","theorems":["Syndetic (def)","interval_block (PB+PF subset PS, syndetic+interval => PS cofinite >= u+L)","interval_block_eventually (atTop form)"...

depends on (the wall): lean/Vela/Erdos124IntervalBlock.lean

lake build Vela.Erdos124IntervalBlock (green, axiom-clean, no sorry)

Erdos #124: refinement of the interval-block reduction (att_61ff8f87c2f692b0). Finite deletion preserves syndeticity: for every finite F subset S(D,k), Sigma(S(D,k) minus F) is syndetic. Proof (GPT-Pro, Opus-checked): the already-verified surplus divergence T_n - a_{n+1} -> infinity gives U_m - b_{m+1} -> infinity for B = S minus F, then a gap-preserving prefix induction. Hence condition (i) of the interval-block lemma is FREE, and the entire open core collapses to condition (ii): exhibit a finite F with Sigma(F) containing L_F consecutive integers (L_F = the deletion syndeticity constant) -- equivalently, arbitrarily many disjoint equal-step signed subset identities in S(D,k), a finite-base replacement for BEGL's Szemeredi/Prouhet step, not supplied by known Diophantine inputs. Computationally consistent on {3,4,7},k=1 (finite deletion keeps bounded tail gaps). It is a reduction refinement, not a settlement; it sharpens the open core.

{"lemma":"finite F => Sigma(S(D,k) minus F) syndetic","proof":"surplus divergence (verified) + gap-preserving prefix induction","consequence":"interval-block condition (i) is free; open core = cond...

depends on (the wall): scripts/verify_124_finite_deletion.py

scripts/verify_124_finite_deletion.py

Erdos #124: computationally verified the Burr-Erdos-Graham-Li cofiniteness conjecture for ALL 176 admissible finite D with elements in [3,12] and sizes 3-5, at k=1. Every one is cofinite (Sigma(S(D,1)) contains all large n), with largest non-representable N(D) <= 986 (max at {3,4,6}; {3,4,7} reproduces BEGL's value 581, validating the method). This extends BEGL's single explicitly verified case {3,4,7} to 176 families and finds NO counterexample. Scope is honest and limited: k=1 only and bounded element range/size; the uniform statement over all admissible D and all k>=1 (the open core) is NOT established, and k>=2 verification requires larger search windows than used here (sparse D such as {3,6,9,10,12} push the threshold beyond a 3e5 window). This is broad verification, not the uniform proof.

{"verified":"scripts/verify_124_database.py","count":176,"element_range":"[3,12]","sizes":"3-5","k":1,"all_cofinite":true,"max_N":986,"argmax":"{3,4,6}","begl_crosscheck":"{3,4,7} -> 581 (matches B...

depends on (the wall): scripts/verify_124_database.py

scripts/verify_124_database.py (176 D, k=1, all cofinite)

Erdos #124: verified uniform equal-step identity construction for every admissible D with 3 in D, extending BEGL's single {3,4,7}. For such D and any k>=1, balanced ternary (Delta_3 = Z) yields disjoint P,Q subset S(D,k) supported on exponents >=N with sum Q - sum P = 1 (fixed step h=1, trivial residue reservoir). Verified computationally on 7 cases incl {3,4,5},{3,4,7},{3,5,8},{3,5,7,11}. This supplies the equal-step-identity ingredient of the interval-block lemma for all D containing 3 -- a real advance over the single known case -- but is NOT a full close: two gaps remain. (i) Syndetic-reservoir control: the interval-block criterion needs u+1 >= L_{F_u} where L_{F_u} is the deletion-syndeticity constant of S minus the u blocks, which may grow with u; a uniform bound or diagonal estimate is missing. (ii) For 3 not in D, balanced base-a Delta_a is a thin subset of Z, so the quotient-hit step fails -- the precise remaining obstruction.

{"construction":"3 in D, gcd=1: pick b in D with 3 not| b; U = AP of b-powers with sum U = 1 mod 3^N; A=(1-sumU)/3^N; balanced ternary A=sum eps_t 3^t; Q=U cup {3^{N+t}:eps=1}, P={3^{N+t}:eps=-1}; ...

depends on (the wall): scripts/verify_124_3inD_construction.py

scripts/verify_124_3inD_construction.py

Erdos #124: refinement/obstruction on the 3-in-D equal-step construction (att_0a14e45cbb28c9a7). That construction yields correct disjoint equal-step identities but is MASS-INEFFICIENT: to place u disjoint blocks, block exponents grow super-exponentially (for {3,4,7}: 1,14,121,1483,18737), so removed mass W_u ~ 3^(tower in u), while the blocks contribute only u+1 consecutive integers (linear). Hence the interval-block diagonal estimate L_{F_u} <= u+1 FAILS by an enormous margin, and the reservoir variant is blocked by the tightness of the admissibility threshold sum 1/(d-1) >= 1 (removing high powers can locally break the bounded-gap condition). Conclusion: the balanced-ternary construction does NOT close the interval-block lemma even for 3 in D. The sharpened open core is MASS-CONTROLLED equal-step identities: many disjoint identities at comparable bounded scale, beating the deletion-syndeticity constant. Verified via the block-exponent growth computation.

{"verified":"scripts/verify_124_mass_growth.py","block_max_exponents_347":[1,14,121,1483,18737],"obstruction":"super-exponential block mass vs linear consecutive-run => diagonal L_{F_u}<=u+1 fails;...

depends on (the wall): scripts/verify_124_mass_growth.py

scripts/verify_124_mass_growth.py

Erdos #124: sharpened reservoir criterion and no-go (corrects the earlier mass framing). (1) Exact criterion: Sigma(B) is L-syndetic iff sup_b def_B(b) < infinity, def_B(b)=b-sigma_B(b); equivalently sigma_R(b) <= Delta_S(b)+O(1) (the Budget condition), R=S\B, Delta_S(x)=sigma_S(x)-x. Verified sharp: removing {343,729,2401} from S({3,4,7},1) gives max gap = sup def = 1757 exactly. (2) Counting no-go: u disjoint unit-step identities use >=2u terms with <=r=|D| per exponent, so the minimum exponent M >= k+ceil(2u/r)-1 (LINEAR in u) and total mass >= 3^{k+floor((2u-1)/r)} (EXPONENTIAL). Hence the bounded-scale O(log u) target is impossible and total mass is the WRONG control variable. (3) Sharpened open core: construct disjoint unit identities I_j whose cumulative prefix-reserved mass sigma_R(x) stays <= Delta_S(x)+O(1) (surplus pays for reservations) -- the prefix-budgeted identity-selection lemma. Supersedes the mass-inefficiency framing (att_9fbaf1aa96de6f20): the right invariant is prefix budget vs the surplus function, not mass.

{"reservoir_criterion":"Sigma(B) L-syndetic <=> sup def_B(b)<inf <=> sigma_R(b)<=Delta_S(b)+O(1)","verified_sharp":"remove {343,729,2401} from S(3,4,7;1): max gap = sup def = 1757 (exact)","no_go":...

depends on (the wall): scripts/verify_124_reservoir_criterion.py

scripts/verify_124_reservoir_criterion.py

Erdos #124 correction: the reservation budget Delta_S(x)=sigma_S(x)-x is LINEAR even in the exact case sum 1/(d-1)=1 (verified ~0.8x to 1.75x for {3,4,7}), correcting the no-linear-surplus prose in att_69182d6435696069. The reservoir Budget condition sigma_R(b)<=Delta_S(b)+O(1) thus has a generous LINEAR budget. Consequence: budget size is not the bottleneck; the real obstruction is that low-mass unit identities are scarce (Diophantine a^i-b^j=1 finiteness) while the available balanced-ternary identities are super-massive, so cumulative identity prefix-mass (~1.5x, geometric) overshoots the ~0.8x worst-case budget. Sharpened core: many LOW-MASS disjoint unit identities.

{"finding":"Delta_S(x)=sigma_S(x)-x is linear (~0.8x-1.75x) for exact {3,4,7}","corrects":"att_69182d6435696069 exact-case no-linear-surplus prose (formula was right)","budget":"linear/generous; no...

depends on (the wall): scripts/verify_124_delta_linear.py

scripts/verify_124_delta_linear.py

Erdos #124 NEGATIVE result: the all-prefix prefix-budget unit-identity route is provably INSUFFICIENT. The lemma sigma_R(x)<=Delta_S(x)+O(1) for an infinite disjoint unit-identity family is FALSE already for D={3,4,7}. Chain (verified): every unit identity has support mass w>=2m-1 (m=max term); at the final gap b=succ(m) the budget forces G(m):=2m-1-Delta_S(succ(m))<=C; but G(m)->+infinity (verified: min G over m>=1e6 is 535415; only 9 m have G<=100), with the cross-base case reduced to Pillai/Bennett finiteness of c^l-a^n=h (Bennett 2001, <=2 solutions per triple). Hence no infinite budget-respecting family exists. This TERMINATES the prefix-budget approach (supersedes the prefix-budget-as-target framing). It does NOT disprove #124: BEGL prove {3,4,7} cofinite by a different per-D computational+Diophantine route. The interval-block criterion (Lean) remains valid but cannot be fed via all-prefix budgeting; the only remaining interval-block variant is cluster-removal (check the reservoir only at surviving B-terms, delete whole bad clusters) -- untested.

{"verifier":"scripts/verify_124_prefix_budget_nogo.py","result":"prefix-budget lemma false for {3,4,7}","mechanism":"w>=2m-1 per identity; G(m)=2m-1-Delta_S(succ(m))->inf; cross-base via Pillai/Ben...

depends on (the wall): scripts/verify_124_prefix_budget_nogo.py

scripts/verify_124_prefix_budget_nogo.py