erdos_125.variants.positive_lower_density.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

19 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

lemma Erdos125.zero_in_A Zero belongs to the base-3 digit set line 91 source
L4DEL explanation
The natural number 0 belongs to A because its base-3 expansion contains no digit outside {0,1}.
1. This supplies the additive identity used to place zero in the sumset.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, True, List.nil, congrArg, List, Nat.digits_zero, eq_true, True.intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma zero_in_A : 0 ∈ A := by
…
```
lemma Erdos125.zero_in_B Zero belongs to the base-4 digit set line 94 source
L4DEL explanation
The natural number 0 belongs to B because its base-4 expansion contains no digit outside {0,1}.
1. Together with zero_in_A, this gives a concrete representation of zero in A+B.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, True, List.nil, congrArg, List, Nat.digits_zero, eq_true, True.intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma zero_in_B : 0 ∈ B := by
…
```
lemma Erdos125.zero_in_A_plus_B The sumset contains zero line 97 source
L4DEL explanation
Since 0∈A and 0∈B, the equality 0=0+0 witnesses 0∈A+B.
1. This fact is used when the final lower-density argument needs a nonempty filtered interval.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, HAdd.hAdd, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: Erdos125.zero_in_A, Erdos125.zero_in_B, Exists.intro, And, Exists, Eq, And.intro, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma zero_in_A_plus_B : 0 ∈ A + B := by
…
```
lemma Erdos125.A_max_k The largest k-digit base-3 number using only zero and one line 102 source
L4DEL explanation
the maximum possible value for abot is the integer consisting of k ones in base 3
— Human-written proof companion for Erdős 125
If x∈A and x<3^k, then x≤(3^k-1)/2, the number whose first k base-3 digits are all one.
1. The geometric sum 1+3+⋯+3^(k-1) equals (3^k-1)/2.
2. The proof inducts over digit positions and uses membership in A to exclude a base-3 digit equal to two.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Membership.mem, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, LE.le, HDiv.hDiv, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.range, id, Eq, congrArg, Eq.trans, HMul.hMul, HAdd.hAdd, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natSub, mul_div_cancel_right₀, Mathlib.Meta.NormNum.isNat_eq_false and 42 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma A_max_k (k x : ℕ) (hx : x < 3^k) (hA : x ∈ A) : x ≤ (3^k - 1) / 2 := by
…
```
lemma Erdos125.B_max_m The largest m-digit base-4 number using only zero and one line 107 source
L4DEL explanation
yielding the analogous bound
— Human-written proof companion for Erdős 125
If y∈B and y<4^m, then y≤(4^m-1)/3, the number whose first m base-4 digits are all one.
1. The geometric sum 1+4+⋯+4^(m-1) equals (4^m-1)/3.
2. The digit restriction eliminates residues two and three at every base-4 position.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Membership.mem, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, LE.le, HDiv.hDiv, HSub.hSub
Proof uses: Iff.mpr, HMul.hMul, Nat.le_div_iff_mul_le, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.le_pred_of_lt, Nat.sub, Nat.rec, of_eq_true, Eq.trans, True, forall_congr, implies_congr, congrArg, pow_zero and 45 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma B_max_m (m y : ℕ) (hy : y < 4^m) (hB : y ∈ B) : y ≤ (4^m - 1) / 3 := by
…
```
lemma Erdos125.A_B_gap A common digit-scale gap in the sumset line 112 source
L4DEL explanation
If x is below both 3^k and 4^m but exceeds (3^k-1)/2+(4^m-1)/3, then x∉A+B.
1. Any representation x=a+b forces a<3^k and b<4^m; A_max_k and B_max_m then make their sum too small.
2. This lemma isolates the gap mechanism, while the stronger density proof below tracks top digits as well as the gap.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HPow.hPow, OfNat.ofNat, Not, Membership.mem, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton
Proof uses: And, Exists, Eq, False, Iff.mp, Set.mem_add, Or, LE.le, Decidable.byContradiction, Erdos125.A_max_k, Erdos125.B_max_m
46 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma A_B_gap (k m x : ℕ) (hx_gt : (3^k - 1) / 2 + (4^m - 1) / 3 < x) (hx_lt_A : x < 3^k) (hx_lt_B : x < 4^m) : x ∉ A + B := by
…
```
lemma Erdos125.A_decomp Split a base-3 digit string into top and bottom blocks line 125 source
L4DEL explanation
we can decompose it at the k-th digit into a top and bottom part
— Human-written proof companion for Erdős 125
Every a∈A can be written a=a1*3^k+a0, where both a1 and a0 remain in A and a0<3^k.
1. Choose a1=a/3^k and a0=a mod 3^k.
2. Division discards the first k digits and remainder keeps exactly those digits, so neither operation introduces a digit outside {0,1}.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, OfNat.ofNat, Insert.insert, Singleton.singleton, Exists, And, LT.lt, HPow.hPow, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Exists.intro, HDiv.hDiv, HMod.hMod, Nat.rec, Eq.rec, Eq.symm, Nat.div_one, Nat.casesAuxOn, GT.gt, Or, Nat.eq_zero_or_pos, Or.inl, of_eq_true, Eq.trans, True, implies_congr_ctx, List.nil, congrArg, List, Nat.digits_zero and 75 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma A_decomp (k a : ℕ) (ha : a ∈ A) : ∃ a1 a0 : ℕ, a1 ∈ A ∧ a0 ∈ A ∧ a0 < 3^k ∧ a = a1 * 3^k + a0 := by
…
```
lemma Erdos125.B_decomp Split a base-4 digit string into top and bottom blocks line 136 source
L4DEL explanation
applying the exact same logic to any b ∈ B at scale m
— Human-written proof companion for Erdős 125
Every b∈B can be written b=b1*4^m+b0, where both pieces remain in B and b0<4^m.
1. The quotient b/4^m retains the top digits and the remainder b mod 4^m retains the bottom m digits.
2. Because the original digits are only zero or one, both resulting digit strings satisfy the same restriction.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, OfNat.ofNat, Insert.insert, Singleton.singleton, Exists, And, LT.lt, HPow.hPow, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Exists.intro, HDiv.hDiv, HMod.hMod, Nat.rec, Eq.rec, Eq.symm, Nat.div_one, Nat.casesAuxOn, of_eq_true, Eq.trans, True, implies_congr_ctx, List.nil, congrArg, List, Nat.digits_zero, Nat.zero_div, Eq.refl, Or, List.cons and 77 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma B_decomp (m b : ℕ) (hb : b ∈ B) : ∃ b1 b0 : ℕ, b1 ∈ B ∧ b0 ∈ B ∧ b0 < 4^m ∧ b = b1 * 4^m + b0 := by
…
```
lemma Erdos125.log_ratio_irrational The logarithms of four and three have irrational ratio line 152 source
L4DEL explanation
log 4 / log 3 is irrational; otherwise a rational relation would force a nontrivial equality between a power of three and a power of four.
1. Clearing a hypothetical rational denominator and exponentiating gives 3^u=4^v for positive integers.
2. The left side is odd and the right side is even, so the equality is impossible.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Irrational, HDiv.hDiv, Real, Real.log, OfNat.ofNat, Nat
Proof uses: Membership.mem, Set, Set.range, Rat, Exists.elim, Eq, False, Iff.mpr, Ne, HMul.hMul, Iff.ne, eq_div_iff, of_eq_true, Not, Eq.trans, True, congrArg, Or, Neg.neg, congr and 64 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma log_ratio_irrational : Irrational (Real.log 4 / Real.log 3) := by use(·.elim fun and x =>(eq_div_iff (by norm_num)).ne.2 (and.num_div_den▸ne_of_eq_of_ne (by rw [Rat.cast_div,div_mul_eq_mul_div]) ((div_eq_iff (by norm_num)).ne.2 fun and=>?_)) x)
…
```
lemma Erdos125.exists_small_pos_lin_comb_help A positive irrational has arbitrarily small positive integer linear combinations line 157 source
L4DEL explanation
For positive irrational α and every δ>0, there are positive naturals m,k with 0<m*α-k<δ.
1. The proof starts from infinitely many rational approximations to α and handles approximants on either side so the final error is positive.
2. Scaling or reflecting a sufficiently accurate approximation produces the required positive integer pair.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Irrational, LT.lt, OfNat.ofNat, Exists, Nat, And, HSub.hSub, HMul.hMul
Proof uses: Set.Infinite, Rat, setOf, abs, HDiv.hDiv, HPow.hPow, Rat.den, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, Eq.mpr, Eq.refl, by_contradiction, Not, Function.comp, GE.ge, Min.min, Set.Finite, False, Exists.elim, Filter.Eventually.exists_forall_of_atTop, Filter.Tendsto.eventually_lt_const and 265 more
319 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma exists_small_pos_lin_comb_help (α : ℝ) (hα : Irrational α) (hα_pos : 0 < α) (δ : ℝ) (hδ : 0 < δ) :
  ∃ m k : ℕ, 0 < m ∧ 0 < k ∧ 0 < (m : ℝ) * α - (k : ℝ) ∧ (m : ℝ) * α - (k : ℝ) < δ := by
…
```
lemma Erdos125.exists_small_pos_lin_comb Make m log 4 minus k log 3 positive and arbitrarily small line 187 source
L4DEL explanation
Because the ratio of logarithms ln(4)/ ln(3) is irrational
— Human-written proof companion for Erdős 125
For every δ>0, positive naturals m,k satisfy 0<m*log 4-k*log 3<δ.
1. Apply exists_small_pos_lin_comb_help to α=log 4/log 3, then multiply through by the positive number log 3.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, And, HSub.hSub, HMul.hMul, Real.log
Proof uses: Irrational, HDiv.hDiv, Erdos125.log_ratio_irrational, div_pos, Mathlib.Meta.Positivity.log_pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, Erdos125.exists_small_pos_lin_comb_help, id, Eq.mp, congrArg, funext, congr, Eq.trans, mul_div, div_sub', ne_of_gt and 1 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma exists_small_pos_lin_comb (δ : ℝ) (hδ : 0 < δ) :
  ∃ m k : ℕ, 0 < m ∧ 0 < k ∧ 0 < (m : ℝ) * Real.log 4 - (k : ℝ) * Real.log 3 ∧ (m : ℝ) * Real.log 4 - (k : ℝ) * Real.log 3 < δ := by
…
```
lemma Erdos125.exists_small_pos_lin_comb_large_k Obtain the logarithmic approximation beyond any requested scale line 196 source
L4DEL explanation
The exponents in the small positive logarithmic combination can also be chosen so that 3^k exceeds any real threshold K.
1. Choose a positive multiplier N with 3^N≥K, find an error below δ/N, and multiply both exponents by N.
2. Scaling preserves positivity, keeps the total error below δ, and makes the base-3 power large enough.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, And, LE.le, HPow.hPow, HSub.hSub, HMul.hMul, Real.log
Proof uses: Exists.intro, Nat.succ, Nat.ceil, And.intro, Nat.succ_pos, le_of_lt, cast, Eq.symm, congrArg, Nat.lt_of_ceil_lt, LT.lt.le, Nat.lt_pow_self, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HDiv.hDiv and 21 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma exists_small_pos_lin_comb_large_k (δ : ℝ) (hδ : 0 < δ) (K : ℝ) :
  ∃ m k : ℕ, 0 < m ∧ 0 < k ∧ K ≤ (3^k : ℝ) ∧ 0 < (m : ℝ) * Real.log 4 - (k : ℝ) * Real.log 3 ∧ (m : ℝ) * Real.log 4 - (k : ℝ) * Real.log 3 < δ := by
…
```
Mentions: K
lemma Erdos125.dirichlet_approx Choose nearby powers of three and four at a large scale line 211 source
L4DEL explanation
Dirichlet’s Approximation Theorem guarantees that we can find arbitrarily large integers k and m
— Human-written proof companion for Erdős 125
For every ε>0, positive k,m can be chosen with 3^k≤4^m≤3^k*(1+ε) and 3^k*ε≥3.
1. Make m*log 4-k*log 3 lie between zero and log(1+ε), then exponentiate both inequalities.
2. The large-scale refinement ensures the additive error budget used in the counting step is at least three.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, And, LE.le, HPow.hPow, HMul.hMul, HAdd.hAdd, GE.ge
Proof uses: Real.log, Real.log_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.sub_pf, Mathlib.Tactic.Ring.neg_add and 56 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma dirichlet_approx (ε : ℝ) (hε : 0 < ε) : ∃ k m : ℕ, 0 < k ∧ 0 < m ∧ (3^k : ℝ) ≤ 4^m ∧ (4^m : ℝ) ≤ (3^k : ℝ) * (1 + ε) ∧ (3^k : ℝ) * ε ≥ 3 := by
…
```
lemma Erdos125.hz_eq_lemma Rewrite a sum using the smaller common scale line 225 source
L4DEL explanation
When 3^k≤4^m, decompositions of a and b give x=(a1+b1)*3^k+z, with z=a0+b0+b1*(4^m-3^k).
1. Replace 4^m by 3^k+(4^m-3^k) and collect the two top-digit terms multiplying 3^k.
2. The remainder records both bottom digit blocks and the small mismatch between the nearby powers.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Decidable.byContradiction, Not, Trans.trans, congrArg, Nat.mul_add, Nat.add_mul
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma hz_eq_lemma (x a b a1 a0 b1 b0 k m : ℕ)
  (h1 : 3^k ≤ 4^m) (h3 : x = a + b) (h4 : a = a1 * 3^k + a0) (h5 : b = b1 * 4^m + b0) :
  x = (a1 + b1) * 3^k + (a0 + b0 + b1 * (4^m - 3^k)) := by
…
```
lemma Erdos125.scale_step Reduce density by a fixed factor at a larger scale line 236 source
L4DEL explanation
the density up to M · N0 is less than or equal to the density up to N0
— Human-written proof companion for Erdős 125
We want to go from density <δ at scale N to density <cδ at some bigger scale MN
— GTSoukalas, Erdős Problems 125 discussion, 30 March 2026
If the count below N is at most C*N, then at a suitable scale N'=N*3^k the count is at most (11/12)*C*N'.
1. Choose 3^k and 4^m within relative error ε≤1/(24N) and split every sum below N*3^k into a top sum y<N and a bounded remainder z.
2. The top coordinate has at most C*N choices; digit maxima and the power mismatch give fewer than 3^k*(5/6+2εN) remainder choices.
3. Since 5/6+2εN≤11/12, multiplying the two coordinate counts produces the uniform density contraction.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125, GTSoukalas, Erdős Problems 125 discussion, 30 March 2026
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, LE.le, Finset.card, Finset.filter, Membership.mem, Set, HAdd.hAdd, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, Finset.Ico, HMul.hMul, Exists and 3 more
Proof uses: Exists.intro, And.intro, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, mul_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Iff.mpr, Nat.cast_pos', le_rfl, HPow.hPow, GE.ge, Erdos125.dirichlet_approx, pow_pos, Eq, Iff.mp and 220 more
222 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
lemma scale_step (N : ℕ) (hN : 0 < N) (C : ℝ) (hC : (((Finset.Ico 0 N).filter (· ∈ A + B)).card : ℝ) ≤ C * (N : ℝ)) :
  ∃ N' > 0, (((Finset.Ico 0 N').filter (· ∈ A + B)).card : ℝ) ≤ (11/12 : ℝ) * C * (N' : ℝ) := by
…
```
lemma Erdos125.density_multi_scale Iterate the contraction through arbitrarily many scales line 301 source
L4DEL explanation
After r iterations, the density of the set up to the scale Nr is bounded by (0.99)r
— Human-written proof companion for Erdős 125
After d scale steps, some positive cutoff N has normalized count at most (11/12)^d.
1. The base case uses N=1; the successor case feeds the current bound into scale_step.
2. The new factor multiplies the previous geometric bound, yielding the next power of 11/12.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, GT.gt, OfNat.ofNat, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Set, HAdd.hAdd, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, Finset.Ico and 3 more
Proof uses: Nat.recAux, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mpr, id, Eq, congrArg, Eq.trans, pow_zero, one_mul, Finset.card_filter_le, rfl, Nat.cast_one, Eq.mp, Erdos125.scale_step and 83 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma density_multi_scale (d : ℕ) : ∃ N > 0, (((Finset.Ico 0 N).filter (· ∈ A + B)).card : ℝ) ≤ ((11/12 : ℝ)^d) * (N : ℝ) := by
…
```
lemma Erdos125.limit_11_12 Powers of eleven twelfths fall below every positive threshold line 328 source
L4DEL explanation
For every ε>0, some natural exponent d satisfies (11/12)^d≤ε.
1. This is geometric decay for a real base strictly between zero and one.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, Nat, LE.le, HPow.hPow, HDiv.hDiv
Proof uses: Exists.imp, LT.lt, le_of_lt, exists_pow_lt_of_lt_one, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, Nat.cast_one, Bool, Bool.true
75 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma limit_11_12 (ε : ℝ) (hε : ε > 0) : ∃ d : ℕ, (11/12 : ℝ)^d ≤ ε := by
…
```
lemma Erdos125.density_tends_to_zero Find a cutoff with density below any positive epsilon line 331 source
L4DEL explanation
proving that the lower density of A + B is 0
— Human-written proof companion for Erdős 125
For every ε>0, there is a positive N with |(A+B)∩[0,N)|≤εN.
1. Choose d so (11/12)^d≤ε, then use the cutoff supplied by density_multi_scale d.
2. This is the quantified subsequence estimate needed to force the lower density to zero.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, Nat, And, LE.le, Finset.card, Finset.filter, Membership.mem, Set, HAdd.hAdd, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, Finset.Ico and 1 more
Proof uses: HPow.hPow, HDiv.hDiv, Erdos125.limit_11_12, Erdos125.density_multi_scale, Exists.intro, And.intro, LE.le.trans, mul_le_mul_of_nonneg_right, Nat.cast_nonneg
58 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma density_tends_to_zero (ε : ℝ) (hε : ε > 0) : ∃ N > 0, (((Finset.Ico 0 N).filter (· ∈ A + B)).card : ℝ) ≤ ε * (N : ℝ) := by
…
```
theorem Erdos125.target_theorem_0 Erdős problem 125: the base-3 plus base-4 digit sumset has zero lower density line 342 source
L4DEL explanation
We show that the answer is no, the lower density is zero.
— Human-written proof companion for Erdős 125
have positive density? positive upper density? For example, what about set {3, 4}?
— Burr, Erdős, Graham, and Li (1996), p. 137
I was surprised to discover that the lower asymptotic density is zero
— Erdős Problems 125 discussion (Giuseppe Melfi and contributors)
Let A contain the nonnegative integers using only digits 0 and 1 in base 3, and B the analogous set in base 4. Their sumset does not have positive lower density: along suitable scales its proportion can be made arbitrarily small.
1. Split base-3 and base-4 expansions into top and bottom digit blocks at independently chosen scales.
2. Irrationality of log 4/log 3 supplies arbitrarily close powers 3^k and 4^m, so the number of possible remainders grows by a factor strictly below the ambient scale.
3. The Lean proof uses the explicit contraction 11/12 rather than the companion's expository 0.99; either fixed factor below one yields geometric decay.
4. density_tends_to_zero is converted to (A+B).lowerDensity=0, making both sides of answer(False) ↔ 0<lowerDensity false.
5. Historical provenance: Burr, Erdős, Graham, and Li asked the density question in 1996. The current Erdős Problems record explains why the formal target adopts the lower-density interpretation.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 125, Erdős Problems 125 source record, Burr, Erdős, Graham, and Li (1996), p. 137, Erdős Problems 125 discussion (Giuseppe Melfi and contributors)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, LT.lt, Real, OfNat.ofNat, Set.lowerDensity, Nat, HAdd.hAdd, Set, setOf, HasSubset.Subset, Finset, List.toFinset, Nat.digits, Insert.insert, Singleton.singleton, Set.univ
Proof uses: GT.gt, Exists, And, LE.le, Finset.card, Finset.filter, Membership.mem, Finset.Ico, HMul.hMul, Erdos125.density_tends_to_zero, Eq, id, Eq.mpr, Filter.liminf, Set.partialDensity, Filter.atTop, SupSet.sSup, Nat.digitsAux, congrArg, Filter.Eventually and 131 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(
  -- EVOLVE-VALUE-START
  False
  -- EVOLVE-VALUE-END
  ) ↔ 0 < (A + B).lowerDensity := by
…
```