erdos_12.parts.i.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

80 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

abbrev Erdos12.IsGood Property P: no member divides the sum of two larger distinct members line 48 source
Source documentation
A set A is "good" if it is infinite and there are no distinct a,b,c in A such that a ∣ (b+c) and b > a, c > a.
L4DEL explanation
divides the sum of two larger terms
— Paul Erdős and András Sárközy (1970), p. 97
IsGood A means that A is infinite and whenever a,b,c ∈ A, a ∣ b+c, a<b, and a<c, the two larger terms must coincide. Equivalently, no three distinct members realize the forbidden divisibility pattern.
1. The conclusion b = c is how the Lean predicate permits repeated use of one larger element while excluding a triple of distinct elements.
2. This is the formal version of the property introduced by Paul Erdős and András Sárközy; their ordered-sequence wording and the set-based Lean wording express the same restriction.
Sources and attribution: Pinned Lean source (0647711a7118), Paul Erdős and András Sárközy (1970), p. 97
no axioms what this means
Statement uses: Set, Nat
Proof uses: And, Set.Infinite, Membership.mem, Dvd.dvd, HAdd.hAdd, LT.lt, Eq
5 instances, coercions and auxiliary constants left out.

Also declared: APNOutputs/ErdosProblems/erdos_12.parts.ii.lean:48 (same declaration text).
```
abbrev IsGood (A : Set ℕ) : Prop := A.Infinite ∧
…
```
lemma Erdos12.exists_prime_bounded Find a controlled next prime line 89 source
L4DEL explanation
For every natural number n, there is a prime p with n < p ≤ 2*n+2.
1. The case n=0 uses the prime 2; otherwise Mathlib's Bertrand bound supplies a prime at most 2*n.
2. This is the existence result used to define the prime sequence q.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, LT.lt, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat.Prime
Proof uses: Eq, Ne, Or, eq_or_ne, Exists.intro, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.prime_two, Eq.symm, Nat.exists_prime_lt_and_le_two_mul, Decidable.byContradiction, Not
21 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma exists_prime_bounded (n : ℕ) : ∃ p, n < p ∧ p ≤ 2 * n + 2 ∧ p.Prime := by
…
```
def Erdos12.q A recursively chosen increasing sequence of primes line 95 source
L4DEL explanation
q 0 = 5; each q (m+1) is a prime chosen strictly above q m but no larger than 2*q m+2.
1. exists_prime_bounded supplies the next prime using the Bertrand-type prime bound already available in Mathlib.
2. The lower bound gives new moduli for separating blocks, while the upper bound later controls their quantitative growth.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Erdos12.q.match_1, Unit, OfNat.ofNat, Nat.succ, Classical.choose, And, LT.lt, LE.le, HAdd.hAdd, HMul.hMul, Nat.Prime
10 instances, coercions and auxiliary constants left out.
```
noncomputable def q : ℕ → ℕ
| 0 => 5
| m + 1 => Classical.choose (exists_prime_bounded (q m))
```
Mentions: Erdos12.exists_prime_bounded
lemma Erdos12.q_prime Every chosen modulus is prime line 99 source
L4DEL explanation
Each value q m is prime.
1. The base value is 5, and every successor is the witness selected by exists_prime_bounded.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Erdos12.q
Proof uses: Nat.casesAuxOn, Eq, OfNat.ofNat, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, HAdd.hAdd, And, LT.lt, Classical.choose, LE.le, HMul.hMul, Erdos12.exists_prime_bounded, Classical.choose_spec, And.right
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma q_prime (m : ℕ) : (q m).Prime := by
…
```
Mentions: Erdos12.q
lemma Erdos12.q_gt Successive chosen primes strictly increase line 106 source
L4DEL explanation
q m < q (m+1) for every block index m.
1. This is the strict lower inequality carried by the witness selected in the recursive definition of q.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Erdos12.q, HAdd.hAdd, OfNat.ofNat
Proof uses: And, Classical.choose, LE.le, HMul.hMul, Nat.Prime, Erdos12.exists_prime_bounded, Classical.choose_spec, And.left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma q_gt (m : ℕ) : q m < q (m + 1) := by
…
```
Mentions: Erdos12.q
lemma Erdos12.q_ge_5 Every chosen prime is at least five line 110 source
L4DEL explanation
The increasing sequence q never falls below its initial value 5.
1. Induction combines q 0 = 5 with the strict growth lemma q_gt.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Erdos12.q
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, LT.lt, HAdd.hAdd, Erdos12.q_gt, Decidable.byContradiction, Not
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma q_ge_5 (m : ℕ) : 5 ≤ q m := by
…
```
Mentions: Erdos12.q
def Erdos12.K The accumulated modulus from all earlier primes line 117 source
L4DEL explanation
K 0 = 729 = 3^6, and K (m+1) = K m * q m.
1. Thus K m is divisible by every earlier q j with j<m, as well as by 3.
2. Members of block m will be congruent to 1 modulo K m, which makes them congruent to 1 modulo each earlier prime.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Erdos12.q.match_1, Unit, OfNat.ofNat, Nat.succ, HMul.hMul, Erdos12.q
5 instances, coercions and auxiliary constants left out.
```
noncomputable def K : ℕ → ℕ
| 0 => 729
| m + 1 => K m * q m
```
Mentions: Erdos12.q
def Erdos12.P The full period for block $m$ line 121 source
L4DEL explanation
P m = K m * q m, combining the accumulated earlier-prime modulus with the block's new prime.
1. Because K m and q m are coprime, the Chinese remainder theorem selects a residue modulo this product satisfying both block congruences.
2. The arithmetic progression enumerating block elements advances by P m, so both congruences remain unchanged.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, Erdos12.K, Erdos12.q
2 instances, coercions and auxiliary constants left out.
```
noncomputable def P (m : ℕ) : ℕ := K m * q m
```
Mentions: Erdos12.K, Erdos12.q
def Erdos12.M The rapidly growing scale separating the blocks line 123 source
L4DEL explanation
M m is the eighth power of P m.
1. The eighth power makes room for roughly fourth-power-many progression points while keeping each block inside [M m, 2*M m].
2. Since successive primes are at least five, the scales grow fast enough that one block ends before the next begins.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, Erdos12.P, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
noncomputable def M (m : ℕ) : ℕ := (P m)^8
```
Mentions: Erdos12.P
def Erdos12.MyGoodSet The Lean proof's congruence-block witness line 125 source
L4DEL explanation
We will construct a sequence of “blocks” that individually cannot contain such a, b, c
— Human-written proof companion for Erdős 12(i)
MyGoodSet contains a natural number n when some block index m places it near M m, below a controlled progression cutoff, with n ≡ 1 (mod K m) and n ≡ 0 (mod q m).
1. The interval conditions are M m ≤ n ≤ 2*M m and a sharper upper bound determined by P (m+1)^4/2 progression steps of size P m.
2. This is the witness actually formalized in Lean. The linked human-written companion proves the same final theorem with a different base-2-to-base-3 block construction.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 12(i)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: setOf, Exists, And, LE.le, Erdos12.M, HMul.hMul, OfNat.ofNat, LT.lt, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Erdos12.P, Eq, HMod.hMod, Erdos12.K, Erdos12.q
14 instances, coercions and auxiliary constants left out.
```
def MyGoodSet : Set ℕ :=
…
```
lemma Erdos12.K_pos The accumulated modulus is positive line 129 source
L4DEL explanation
K m is positive for every block index.
1. K 0=729, and each successor multiplies a positive earlier value by the positive prime q m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Erdos12.K
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Erdos12.q, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq and 46 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma K_pos (m : ℕ) : 0 < K m := by
…
```
Mentions: Erdos12.K
lemma Erdos12.P_pos The joint period is positive line 136 source
L4DEL explanation
P m = K m*q m is always positive.
1. Positivity follows from K_pos and the lower bound q m≥5.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Erdos12.P
Proof uses: Nat.mul_pos, Erdos12.K, Erdos12.q, Erdos12.K_pos, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast and 43 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma P_pos (m : ℕ) : 0 < P m := Nat.mul_pos (K_pos m) (by linarith [q_ge_5 m])
```
Mentions: Erdos12.P, Erdos12.K_pos, Erdos12.q_ge_5
lemma Erdos12.M_succ Successive block scales differ by an eighth power line 138 source
L4DEL explanation
M (m+1) = M m * q (m+1)^8.
1. Since P (m+1)=P m*q (m+1) and M=P^8, the identity follows by distributing the eighth power over multiplication.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos12.M, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HPow.hPow, Erdos12.q
Proof uses: Trans.trans, Erdos12.P, rfl, Nat.mul_pow
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma M_succ (m : ℕ) : M (m + 1) = M m * (q (m + 1))^8 := by
…
```
Mentions: Erdos12.M, Erdos12.q
lemma Erdos12.pow_eight_le Eighth powers preserve order on naturals line 144 source
L4DEL explanation
If a≤b, then a^8≤b^8.
1. This elementary monotonicity lemma is used in the block-growth estimates.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat
Proof uses: pow_le_pow_left₀, zero_le
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma pow_eight_le {a b : ℕ} (h : a ≤ b) : a^8 ≤ b^8 := by
…
```
lemma Erdos12.M_increasing Consecutive block scales are more than a factor of two apart line 147 source
L4DEL explanation
M_increasing m proves 2*M m < M (m+1).
1. The identity M (m+1) = M m * q (m+1)^8 reduces the claim to the fact that the next prime is at least five.
2. This strict separation prevents the intervals [M m,2*M m] for different block indices from overlapping.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HMul.hMul, OfNat.ofNat, Erdos12.M, HAdd.hAdd
Proof uses: Eq, HPow.hPow, Erdos12.q, Erdos12.M_succ, LE.le, Erdos12.q_ge_5, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Erdos12.pow_eight_le, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg and 74 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma M_increasing (m : ℕ) : 2 * M m < M (m + 1) := by
…
```
Mentions: Erdos12.M
lemma Erdos12.M_monotone Block scales are monotone line 159 source
L4DEL explanation
If m1≤m2, then M m1≤M m2.
1. Induction advances through M_increasing, whose stronger conclusion says each next scale exceeds twice the previous one.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M
Proof uses: Nat.recAux, OfNat.ofNat, Eq, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, le_refl, HAdd.hAdd, Or, LT.lt, HMul.hMul, Erdos12.M_increasing, Eq.symm
17 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma M_monotone {m1 m2 : ℕ} (h : m1 ≤ m2) : M m1 ≤ M m2 := by
…
```
Mentions: Erdos12.M
lemma Erdos12.m_le_of_lt Numerical order respects block order line 172 source
L4DEL explanation
If a lies in block ma, b lies in block mb, and a<b, then ma≤mb.
1. If mb<ma, then the factor-of-two separation puts the start of block ma above the end of block mb, contradicting a<b.
2. The good-set proof uses this lemma to reduce all possible triples to later-block and same-block cases.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M, HMul.hMul, OfNat.ofNat, LT.lt
Proof uses: Decidable.byContradiction, Not, HAdd.hAdd, Eq.mp, Erdos12.M_increasing, Erdos12.M_monotone
19 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma m_le_of_lt {a b ma mb : ℕ} (ha : M ma ≤ a) (_ : a ≤ 2 * M ma)
  (_ : M mb ≤ b) (hb2 : b ≤ 2 * M mb) (hab : a < b) : ma ≤ mb := by
…
```
Mentions: Erdos12.M
lemma Erdos12.q_dvd_K Every earlier prime is absorbed into later accumulated moduli line 181 source
L4DEL explanation
When ma<mb, the prime q ma divides K mb.
1. The recursion K (m+1)=K m*q m inserts each chosen prime and preserves all earlier prime factors.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Dvd.dvd, Erdos12.q, Erdos12.K
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, HAdd.hAdd, Or, Eq, dvd_mul_of_dvd_left, Exists.intro, HMul.hMul, mul_comm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma q_dvd_K {ma mb : ℕ} (hma : ma < mb) : q ma ∣ K mb := by
…
```
Mentions: Erdos12.q, Erdos12.K
lemma Erdos12.mod_q_of_lt A later block is $1$ modulo every earlier block prime line 192 source
L4DEL explanation
If b ≡ 1 (mod K mb) and ma<mb, then b ≡ 1 (mod q ma).
1. q_dvd_K proves that the earlier prime q ma divides the later accumulated modulus K mb.
2. Reducing the block congruence through that divisibility transfers the residue 1 to the earlier prime.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.K, OfNat.ofNat, LT.lt, Erdos12.q
Proof uses: Dvd.dvd, Erdos12.q_dvd_K, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Nat.div_add_mod, Trans.trans, Eq.symm, Eq.mp, congrArg, Eq.mpr, id, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf and 21 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma mod_q_of_lt {b mb ma : ℕ} (hb : b % K mb = 1) (hma : ma < mb) : b % q ma = 1 := by
…
```
Mentions: Erdos12.K, Erdos12.q
lemma Erdos12.q_div_a Zero remainder gives divisibility by the block prime line 214 source
L4DEL explanation
If a mod q ma = 0, then q ma divides a.
1. This is the standard remainder characterization of divisibility.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.q, OfNat.ofNat, Dvd.dvd
Proof uses: Nat.dvd_of_mod_eq_zero
7 instances, coercions and auxiliary constants left out.
```
lemma q_div_a {a ma : ℕ} (ha : a % q ma = 0) : q ma ∣ a := Nat.dvd_of_mod_eq_zero ha
```
Mentions: Erdos12.q
lemma Erdos12.K_mod_3 Every accumulated modulus is divisible by three line 216 source
L4DEL explanation
K m mod 3 = 0 for every m.
1. The base K 0=729=3^6 is divisible by three, and multiplication by later primes preserves that factor.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.K, OfNat.ofNat
Proof uses: Nat.recAux, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, Erdos12.q, Nat.mul_mod, Nat.zero_mul, Eq.mp, congrArg
9 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma K_mod_3 (m : ℕ) : K m % 3 = 0 := by
…
```
Mentions: Erdos12.K
lemma Erdos12.mod_3_eq_1 The block residue forces residue one modulo three line 226 source
L4DEL explanation
If n mod K m = 1, then n mod 3 = 1.
1. Because 3 divides K m, writing n as a multiple of K m plus one gives the claimed residue.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.K, OfNat.ofNat
Proof uses: Dvd.dvd, Nat.dvd_of_mod_eq_zero, Erdos12.K_mod_3, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Nat.div_add_mod, Trans.trans, Eq.symm, Eq.mp, congrArg, Eq.mpr, id, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr and 15 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma mod_3_eq_1 {n m : ℕ} (hn : n % K m = 1) : n % 3 = 1 := by
…
```
Mentions: Erdos12.K
lemma Erdos12.prime_dvd_K Prime factors of an accumulated modulus precede the current prime line 237 source
L4DEL explanation
If a prime p divides K m, then p<q m.
1. At m=0, every prime factor of 3^6 is at most 3<5; the successor step splits a prime divisor of K m*q m between the two factors.
2. Strict growth of q then places either possible factor below q (m+1).
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Dvd.dvd, Erdos12.K, LT.lt, Erdos12.q
Proof uses: Nat.recAux, OfNat.ofNat, Eq, rfl, LE.le, HPow.hPow, Eq.mp, congrArg, Nat.Prime.dvd_of_dvd_pow, Nat.le_of_dvd, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, HAdd.hAdd and 61 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma prime_dvd_K {p m : ℕ} (hp : p.Prime) (h : p ∣ K m) : p < q m := by
…
```
Mentions: Erdos12.K, Erdos12.q
lemma Erdos12.K_q_coprime The accumulated modulus and the new prime are coprime line 261 source
L4DEL explanation
K_q_coprime m proves Nat.Coprime (K m) (q m).
1. Every prime divisor of K m is smaller than q m, whereas q m itself is prime.
2. This coprimality is the exact hypothesis needed to combine residues 1 mod K m and 0 mod q m by the Chinese remainder theorem.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, Erdos12.K, Erdos12.q
Proof uses: Dvd.dvd, Nat.gcd, Nat.gcd_dvd_right, Nat.Prime, Erdos12.q_prime, Or, Eq, OfNat.ofNat, Iff.mp, Nat.dvd_prime, Nat.gcd_dvd_left, LT.lt, Erdos12.prime_dvd_K, Eq.mp, congrArg, Decidable.byContradiction, Not
6 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma K_q_coprime (m : ℕ) : Nat.Coprime (K m) (q m) := by
…
```
Mentions: Erdos12.K, Erdos12.q
lemma Erdos12.K_ge_3 The accumulated modulus is never smaller than three line 272 source
L4DEL explanation
3≤K m for every block index.
1. The base is 729, and the recursion only multiplies by primes at least five.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Erdos12.K
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, HMul.hMul, Erdos12.q, rfl, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg and 57 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma K_ge_3 (m : ℕ) : 3 ≤ K m := by
…
```
Mentions: Erdos12.K
lemma Erdos12.P_dvd_M The joint period divides the block scale line 282 source
L4DEL explanation
P m divides M m=P m^8.
1. Factor the eighth power as P m^7 * P m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Erdos12.P, Erdos12.M
Proof uses: Eq, HPow.hPow, OfNat.ofNat, rfl, HMul.hMul, Eq.mpr, id, congrArg, dvd_mul_left
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma P_dvd_M (m : ℕ) : P m ∣ M m := by
…
```
Mentions: Erdos12.P, Erdos12.M
lemma Erdos12.K_dvd_P The accumulated modulus divides the joint period line 288 source
L4DEL explanation
K m divides P m because P m=K m*q m.
Sources and attribution: Pinned Lean source (0647711a7118)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Erdos12.K, Erdos12.P
Proof uses: Exists.intro, Eq, HMul.hMul, Erdos12.q, rfl
3 instances, coercions and auxiliary constants left out.
```
lemma K_dvd_P (m : ℕ) : K m ∣ P m := ⟨q m, rfl⟩
```
Mentions: Erdos12.K, Erdos12.P, Erdos12.q
lemma Erdos12.q_dvd_P The current prime divides the joint period line 290 source
L4DEL explanation
q m divides P m because P m=K m*q m.
Sources and attribution: Pinned Lean source (0647711a7118)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Erdos12.q, Erdos12.P
Proof uses: Exists.intro, Eq, HMul.hMul, Erdos12.K, mul_comm
7 instances, coercions and auxiliary constants left out.
```
lemma q_dvd_P (m : ℕ) : q m ∣ P m := ⟨K m, mul_comm (K m) (q m)⟩
```
Mentions: Erdos12.q, Erdos12.P, Erdos12.K
lemma Erdos12.K_dvd_M The accumulated modulus divides the block scale line 292 source
L4DEL explanation
K m divides M m.
1. Divisibility passes through K m ∣ P m and P m ∣ M m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Erdos12.K, Erdos12.M
Proof uses: dvd_trans, Erdos12.P, Erdos12.K_dvd_P, Erdos12.P_dvd_M
2 instances, coercions and auxiliary constants left out.
```
lemma K_dvd_M (m : ℕ) : K m ∣ M m := dvd_trans (K_dvd_P m) (P_dvd_M m)
```
Mentions: Erdos12.K, Erdos12.M, Erdos12.K_dvd_P, Erdos12.P_dvd_M
lemma Erdos12.q_dvd_M The current prime divides the block scale line 294 source
L4DEL explanation
q m divides M m.
1. Divisibility passes through q m ∣ P m and P m ∣ M m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, Erdos12.q, Erdos12.M
Proof uses: dvd_trans, Erdos12.P, Erdos12.q_dvd_P, Erdos12.P_dvd_M
2 instances, coercions and auxiliary constants left out.
```
lemma q_dvd_M (m : ℕ) : q m ∣ M m := dvd_trans (q_dvd_P m) (P_dvd_M m)
```
Mentions: Erdos12.q, Erdos12.M, Erdos12.q_dvd_P, Erdos12.P_dvd_M
lemma Erdos12.pow_four_le Fourth powers preserve order on naturals line 296 source
L4DEL explanation
If a≤b, then a^4≤b^4.
1. This elementary monotonicity lemma supports the quantitative block estimates.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat
Proof uses: pow_le_pow_left₀, zero_le
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma pow_four_le {a b : ℕ} (h : a ≤ b) : a^4 ≤ b^4 := by gcongr
```
def Erdos12.r_val A Chinese-remainder solution for the two block residues line 298 source
L4DEL explanation
r_val m selects the natural-number representative produced by the Chinese remainder theorem for residue 1 modulo K m and residue 0 modulo q m.
1. Existence depends on K_q_coprime m.
2. The definition is noncomputable because it chooses a representative from an existence theorem; the surrounding proof needs its specification, not an extraction algorithm.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, Nat.ModEq, Erdos12.K, OfNat.ofNat, Erdos12.q, Nat.chineseRemainder, Erdos12.K_q_coprime
2 instances, coercions and auxiliary constants left out.
```
noncomputable def r_val (m : ℕ) : ℕ := (Nat.chineseRemainder (K_q_coprime m) 1 0).val
```
Mentions: Erdos12.K_q_coprime
def Erdos12.x_val The canonical block offset modulo the full period line 300 source
L4DEL explanation
x_val m reduces r_val m modulo P m = K m*q m.
1. Consequently x_val m < P m, which keeps the first progression point close to the block's base scale.
2. Because both K m and q m divide P m, reduction modulo P m preserves the two Chinese-remainder congruences.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HMod.hMod, Erdos12.r_val, Erdos12.P
2 instances, coercions and auxiliary constants left out.
```
noncomputable def x_val (m : ℕ) : ℕ := (r_val m) % P m
```
Mentions: Erdos12.r_val, Erdos12.P
lemma Erdos12.x_val_lt_P Choose the canonical residue below one period line 302 source
L4DEL explanation
x_val m is strictly smaller than P m.
1. By definition it is the remainder of r_val m modulo the positive number P m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Erdos12.x_val, Erdos12.P
Proof uses: Nat.mod_lt, Erdos12.r_val, Erdos12.P_pos
1 instances, coercions and auxiliary constants left out.
```
lemma x_val_lt_P (m : ℕ) : x_val m < P m := Nat.mod_lt _ (P_pos m)
```
Mentions: Erdos12.x_val, Erdos12.P, Erdos12.P_pos
lemma Erdos12.x_val_mod_K The canonical offset is $1$ modulo the accumulated modulus line 304 source
L4DEL explanation
x_val_mod_K m establishes x_val m % K m = 1.
1. It combines the Chinese-remainder specification of r_val with the fact that K m ∣ P m.
2. Adding multiples of P m therefore keeps every enumerated block element at residue one modulo K m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.x_val, Erdos12.K, OfNat.ofNat
Proof uses: Nat.ModEq, Erdos12.r_val, And.left, And, Erdos12.q, Nat.chineseRemainder, Erdos12.K_q_coprime, Subtype.property, LE.le, Erdos12.K_ge_3, Nat.mod_eq_of_lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, LT.lt, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub and 56 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma x_val_mod_K (m : ℕ) : (x_val m) % K m = 1 := by
…
```
Mentions: Erdos12.x_val, Erdos12.K
lemma Erdos12.x_val_mod_q The canonical offset is $0$ modulo the block's new prime line 314 source
L4DEL explanation
x_val_mod_q m establishes x_val m % q m = 0.
1. It transfers the second Chinese-remainder congruence through reduction modulo P m, using q m ∣ P m.
2. Every point in block m will consequently be divisible by q m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos12.x_val, Erdos12.q, OfNat.ofNat
Proof uses: Nat.ModEq, Erdos12.r_val, And.right, Erdos12.K, And, Nat.chineseRemainder, Erdos12.K_q_coprime, Subtype.property, Nat.zero_mod, Erdos12.P, Nat.mod_mod_of_dvd, Erdos12.q_dvd_P, Eq.mp, congrArg
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma x_val_mod_q (m : ℕ) : (x_val m) % q m = 0 := by
…
```
Mentions: Erdos12.x_val, Erdos12.q
lemma Erdos12.exists_good_in_block Every block contains at least one admissible residue line 323 source
L4DEL explanation
For each m, some n lies in the mth block and satisfies n ≡ 1 (mod K m) and n ≡ 0 (mod q m).
1. The Chinese remainder theorem supplies a residue x<P m satisfying both congruences because K m and q m are coprime.
2. Taking n=M m+x preserves those residues because both moduli divide M m; the size estimates place n within the required block cutoff.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, LE.le, Erdos12.M, HMul.hMul, OfNat.ofNat, LT.lt, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Erdos12.P, Eq, HMod.hMod, Erdos12.K, Erdos12.q
Proof uses: Nat.Coprime, Erdos12.K_q_coprime, Subtype, Nat.ModEq, Nat.chineseRemainder, And.left, Subtype.property, And.right, Erdos12.K_ge_3, Nat.mod_eq_of_lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast and 99 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma exists_good_in_block (m : ℕ) : ∃ n, M m ≤ n ∧ n ≤ 2 * M m ∧ n < M m + (P (m + 1)^4 / 2) * P m ∧ n % K m = 1 ∧ n % q m = 0 := by
…
```
Mentions: Erdos12.M, Erdos12.P, Erdos12.K, Erdos12.q
lemma Erdos12.M_gt_m Block scales eventually dominate their indices immediately line 383 source
L4DEL explanation
Every index satisfies m<M m.
1. The base scale is positive, and M_increasing more than doubles the scale at each successor.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Erdos12.M
Proof uses: Nat.recAux, Eq, OfNat.ofNat, HPow.hPow, Erdos12.P, rfl, LE.le, Erdos12.P_pos, Erdos12.pow_eight_le, Trans.trans, Eq.symm, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq and 75 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma M_gt_m (m : ℕ) : m < M m := by
…
```
Mentions: Erdos12.M
lemma Erdos12.my_good_set_infinite The congruence-block witness is infinite line 398 source
L4DEL explanation
Beyond every natural bound N, the proof constructs a member of MyGoodSet in block N+1.
1. exists_good_in_block supplies a number with the block inequalities and both required residues.
2. M_gt_m places that number above N, yielding the standard unboundedness characterization of an infinite set of naturals.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Infinite, Nat, Erdos12.MyGoodSet
Proof uses: Eq.mpr, Exists, And, Membership.mem, Set, LT.lt, id, Eq, congrArg, propext, Set.infinite_iff_exists_gt, LE.le, Erdos12.M, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HDiv.hDiv, HPow.hPow, Erdos12.P, HMod.hMod and 65 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma my_good_set_infinite : MyGoodSet.Infinite := by
…
```
lemma Erdos12.my_good_set_is_good The congruences exclude every forbidden divisibility triple line 409 source
L4DEL explanation
my_good_set_is_good proves that MyGoodSet is infinite and satisfies property P.
1. If one larger term lies in a later block, it is 1 mod q ma; the other larger term is 0 or 1 mod q ma, so their sum cannot be divisible by q ma, while a is divisible by that prime.
2. If all three terms lie in the same block, interval bounds force (b+c)/a to be 3 or 4. Every block member is 1 mod 3, but neither multiplier gives the required residue 2 mod 3 for b+c.
3. This is a complete congruence proof internal to the Lean file; it does not invoke the companion PDF's base-3 progression-free map.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos12.IsGood, Erdos12.MyGoodSet
Proof uses: And.intro, Set.Infinite, Nat, Membership.mem, Set, Dvd.dvd, HAdd.hAdd, LT.lt, Eq, Erdos12.my_good_set_infinite, And, LE.le, Erdos12.M, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Erdos12.P, HMod.hMod, Erdos12.K and 99 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 138 steps
Open to load the checked before-and-after goal states.
```
lemma my_good_set_is_good : IsGood MyGoodSet := by
…
```
Mentions: Erdos12.IsGood, Erdos12.MyGoodSet
def Erdos12.f_val Enumerate the arithmetic progression inside one block line 519 source
L4DEL explanation
f_val m i = M m + x_val m + i*P m is the ith candidate in block m.
1. M m and P m are divisible by both K m and q m, while x_val m has residues one and zero respectively.
2. Varying i therefore produces distinct candidates with exactly the congruences required by MyGoodSet.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, Erdos12.M, Erdos12.x_val, HMul.hMul, Erdos12.P
4 instances, coercions and auxiliary constants left out.
```
noncomputable def f_val (m i : ℕ) : ℕ := M m + x_val m + i * P m
```
Mentions: Erdos12.M, Erdos12.x_val, Erdos12.P
lemma Erdos12.P_le_M One period fits inside its block scale line 521 source
L4DEL explanation
P m≤M m=P m^8.
1. Positivity of P m makes the seventh-power multiplier at least one.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.P, Erdos12.M
Proof uses: Eq, HMul.hMul, HPow.hPow, OfNat.ofNat, rfl, Erdos12.P_pos, pow_le_pow_left₀, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Nat.mul_le_mul_right, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd and 66 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma P_le_M (m : ℕ) : P m ≤ M m := by
…
```
Mentions: Erdos12.P, Erdos12.M
lemma Erdos12.q_bound_le An exponential upper bound for the chosen primes line 530 source
L4DEL explanation
q m+2 ≤ 7*2^m.
1. Each selected prime is at most 2*q m+2, so the shifted quantity q m+2 at most doubles at every step.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, Erdos12.q, OfNat.ofNat, HMul.hMul, HPow.hPow
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.left, Classical.choose, And, LT.lt, Nat.Prime, Erdos12.exists_prime_bounded, And.right, Classical.choose_spec, Decidable.byContradiction, Not, Nat.mul_le_mul_left, Mathlib.Tactic.Ring.of_eq and 26 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma q_bound_le (m : ℕ) : q m + 2 ≤ 7 * 2^m := by
…
```
Mentions: Erdos12.q
lemma Erdos12.P_lower_bound An exponential lower bound for the joint periods line 540 source
L4DEL explanation
3645*5^m ≤ P m.
1. The base value is exactly 3645, and every successor multiplies by a prime at least five.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, Erdos12.P
Proof uses: Nat.recAux, Eq, rfl, Decidable.byContradiction, Not, HAdd.hAdd, Erdos12.q, Erdos12.q_ge_5, Nat.mul_le_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.pow_add, Mathlib.Tactic.Ring.single_pow and 17 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma P_lower_bound (m : ℕ) : 3645 * 5^m ≤ P m := by
…
```
Mentions: Erdos12.P
lemma Erdos12.q_pow_four_bound_helper Compare the explicit exponential envelopes line 552 source
L4DEL explanation
38416*16^m ≤ 48427561125*125^m.
1. The base case is numerical; induction preserves the inequality because the left side grows by 16 while the right side grows by 125.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero and 21 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma q_pow_four_bound_helper (m : ℕ) : 38416 * 16^m ≤ 48427561125 * 125^m := by
…
```
lemma Erdos12.q_pow_four_bound The next prime grows slowly relative to the current period line 563 source
L4DEL explanation
The inequality q (m+1)^4 ≤ P m^3 supplies the quantitative room needed to fit many progression points into block m.
1. The proof combines the recursive upper bound q m + 2 ≤ 7*2^m with the lower bound 3645*5^m ≤ P m.
2. Raising those estimates to the relevant powers reduces the comparison to an explicit exponential inequality.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, Erdos12.q, HAdd.hAdd, OfNat.ofNat, Erdos12.P
Proof uses: HMul.hMul, Erdos12.q_bound_le, Decidable.byContradiction, Not, Erdos12.P_lower_bound, pow_le_pow_left₀, zero_le, le_of_lt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, pow_pos, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr and 42 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma q_pow_four_bound (m : ℕ) : q (m + 1) ^ 4 ≤ P m ^ 3 := by
…
```
Mentions: Erdos12.q, Erdos12.P
lemma Erdos12.f_val_bound Progression offsets occupy at most half a block line 596 source
L4DEL explanation
If i≤P (m+1)^4/2, then i*P m≤M m/2.
1. Expand P (m+1)^4 as P m^4*q (m+1)^4 and use q (m+1)^4≤P m^3.
2. The resulting seventh power, after multiplying by P m, is exactly M m=P m^8.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HDiv.hDiv, HPow.hPow, Erdos12.P, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Erdos12.M
Proof uses: Decidable.byContradiction, Not, Eq, Erdos12.q, rfl, Eq.mpr, id, congrArg, Nat.mul_pow, Eq.refl, Erdos12.q_pow_four_bound, Trans.trans, Nat.mul_le_mul_left, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos and 60 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma f_val_bound (m i : ℕ) (hi : i ≤ (P (m + 1))^4 / 2) : i * P m ≤ M m / 2 := by
…
```
Mentions: Erdos12.P, Erdos12.M
lemma Erdos12.P_le_M_half Even one full period fits inside half a block line 613 source
L4DEL explanation
P m≤M m/2.
1. Since P m≥15, its seventh power is at least two, so 2*P m≤P m^8=M m.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.P, HDiv.hDiv, Erdos12.M, OfNat.ofNat
Proof uses: Eq, HMul.hMul, HPow.hPow, rfl, LT.lt, Erdos12.P_pos, Erdos12.K, Erdos12.K_ge_3, Erdos12.q, Erdos12.q_ge_5, Nat.mul_le_mul, Decidable.byContradiction, Not, Trans.trans, Nat.le_mul_of_pos_right, pow_pos, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 26 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma P_le_M_half (m : ℕ) : P m ≤ M m / 2 := by
…
```
Mentions: Erdos12.P, Erdos12.M
lemma Erdos12.f_val_in_good_set Every bounded progression index produces a valid block member line 631 source
L4DEL explanation
For i < P (m+1)^4/2, the point f_val m i belongs to MyGoodSet ∩ [M m,2*M m].
1. Growth estimates bound i*P m by M m/2, while x_val m<P m≤M m/2, placing the point inside the block interval and below the sharper cutoff.
2. Divisibility of M m and P m preserves x_val's residues, proving the membership congruences.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HDiv.hDiv, HPow.hPow, Erdos12.P, HAdd.hAdd, OfNat.ofNat, Membership.mem, Set, Inter.inter, Erdos12.MyGoodSet, Set.Icc, Erdos12.M, HMul.hMul, Erdos12.f_val
Proof uses: And.intro, Exists.intro, And, LE.le, Eq, HMod.hMod, Erdos12.K, Erdos12.q, id, Decidable.byContradiction, Erdos12.x_val, Not, Erdos12.P_le_M_half, Erdos12.f_val_bound, Erdos12.x_val_lt_P, Nat.mul_le_mul_right, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr and 35 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
```
lemma f_val_in_good_set (m i : ℕ) (hi : i < (P (m + 1))^4 / 2) : f_val m i ∈ MyGoodSet ∩ Set.Icc (M m) (2 * M m) := by
…
```
Mentions: Erdos12.P, Erdos12.f_val, Erdos12.MyGoodSet, Erdos12.M
lemma Erdos12.f_val_inj Distinct progression indices give distinct block members line 708 source
L4DEL explanation
The map i ↦ f_val m i is injective on the permitted index interval.
1. Equality cancels the common block offset and leaves i*P m=j*P m; positivity of P m permits cancellation.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.InjOn, Erdos12.f_val, Set.Ico, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Erdos12.P, HAdd.hAdd
Proof uses: Membership.mem, Set, Eq, HMul.hMul, Decidable.byContradiction, Not, LT.lt, Erdos12.P_pos, Nat.eq_of_mul_eq_mul_right
24 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma f_val_inj (m : ℕ) : Set.InjOn (f_val m) (Set.Ico 0 ((P (m + 1))^4 / 2)) := by
…
```
Mentions: Erdos12.f_val, Erdos12.P
lemma Erdos12.finset_coe_ncard Set cardinality agrees with finite-set cardinality line 715 source
L4DEL explanation
Viewing a finite set s as a Set does not change its number of elements.
1. This bridge lets the counting proof move between Finset.card and Set.ncard.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Eq, Nat, Set.ncard, Finset.card
Proof uses: of_eq_true, Eq.trans, True, congrArg, Set.ncard_coe_finset, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma finset_coe_ncard {α : Type*} (s : Finset α) : (s : Set α).ncard = s.card := by
…
```
lemma Erdos12.good_set_inter_finite A bounded slice of the witness set is finite line 718 source
L4DEL explanation
MyGoodSet ∩ [M m,2*M m] is finite.
1. It is a subset of the finite natural-number interval [M m,2*M m].
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Finite, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, Erdos12.M, HMul.hMul, OfNat.ofNat
Proof uses: HasSubset.Subset, Membership.mem, And.right, Set.finite_Icc, Set.Finite.subset
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma good_set_inter_finite (m : ℕ) : (MyGoodSet ∩ Set.Icc (M m) (2 * M m)).Finite := by
…
```
Mentions: Erdos12.MyGoodSet, Erdos12.M
lemma Erdos12.count_interval Each block contains at least half a fourth power of points line 723 source
L4DEL explanation
Block m contains at least P (m+1)^4/2 members of MyGoodSet between M m and 2*M m.
1. The indices 0 ≤ i < P (m+1)^4/2 map into the block by f_val_in_good_set.
2. f_val_inj shows that different indices give different natural numbers, so the image cardinality supplies the lower bound.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HDiv.hDiv, HPow.hPow, Erdos12.P, HAdd.hAdd, OfNat.ofNat, Set.ncard, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, Erdos12.M, HMul.hMul
Proof uses: Eq, Finset.card, Finset.Ico, Nat.card_Ico, Membership.mem, Finset, Erdos12.f_val, Set.Ico, LT.lt, And.right, Iff.mp, And, Finset.mem_Ico, And.intro, Decidable.byContradiction, Not, Erdos12.f_val_inj, Erdos12.f_val_in_good_set, Finset.image, Eq.mpr and 11 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma count_interval (m : ℕ) : P (m + 1) ^ 4 / 2 ≤ (MyGoodSet ∩ Set.Icc (M m) (2 * M m)).ncard := by
…
```
Mentions: Erdos12.P, Erdos12.MyGoodSet, Erdos12.M
lemma Erdos12.density_ineq_x A floor-division estimate beyond ten line 764 source
L4DEL explanation
For x≥10, the inequality 8*x≤9*(x/2)^2 holds in natural arithmetic.
1. The proof controls the remainder modulo two and reduces the claim to a quadratic inequality in x/2.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, HDiv.hDiv
Proof uses: Eq, HAdd.hAdd, HMod.hMod, Nat.div_add_mod, Decidable.byContradiction, Not, GE.ge, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.instCommSemiringNat and 75 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma density_ineq_x {x : ℕ} (hx : 10 ≤ x) : 8 * x ≤ 9 * (x / 2)^2 := by
…
```
lemma Erdos12.density_ineq_x_sq A squared floor-division estimate beyond twenty line 770 source
L4DEL explanation
For x≥20, the inequality 2*x^2≤9*(x/2)^2 holds.
1. As in density_ineq_x, the proof accounts explicitly for the possible remainder when dividing by two.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, HDiv.hDiv
Proof uses: Eq, HAdd.hAdd, HMod.hMod, Nat.div_add_mod, Decidable.byContradiction, Not, GE.ge, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.instCommSemiringNat and 75 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma density_ineq_x_sq {x : ℕ} (hx : 20 ≤ x) : 2 * x^2 ≤ 9 * (x / 2)^2 := by
…
```
lemma Erdos12.density_helper_pow The density envelopes separate exponentially line 776 source
L4DEL explanation
2151296*32^(m+6) ≤ 3375*125^(m+6).
1. The base inequality is checked directly, then induction uses the growth-rate comparison 32≤125.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow, HAdd.hAdd
Proof uses: Nat.recAux, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Decidable.byContradiction, Not, Eq.mpr, congrArg, pow_add, pow_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 29 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma density_helper_pow (m : ℕ) : 2151296 * 32^(m + 6) ≤ 3375 * 125^(m + 6) := by
…
```
lemma Erdos12.density_ineq_q_helper Compare prime-growth and period-growth envelopes line 793 source
L4DEL explanation
For m≥6, 4*(7*2^(m+1))^5 ≤ (15*5^m)^3.
1. Writing m=k+6 converts both sides to the exponential forms compared by density_helper_pow.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, HAdd.hAdd
Proof uses: Exists, Eq, Exists.intro, HSub.hSub, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, pow_add, pow_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_congr and 31 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma density_ineq_q_helper (m : ℕ) (hm : 6 ≤ m) : 4 * (7 * 2^(m + 1))^5 ≤ (15 * 5^m)^3 := by
…
```
lemma Erdos12.density_ineq_q Bound the fifth power of the next prime line 821 source
L4DEL explanation
For m≥6, 4*q (m+1)^5≤P m^3.
1. The upper envelope for q and lower envelope for P reduce the claim to density_ineq_q_helper.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, Erdos12.q, HAdd.hAdd, Erdos12.P
Proof uses: Erdos12.q_bound_le, Decidable.byContradiction, Not, pow_le_pow_left₀, zero_le, Erdos12.P_lower_bound, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 64 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma density_ineq_q (m : ℕ) (hm : 6 ≤ m) : 4 * (q (m + 1))^5 ≤ P m ^ 3 := by
…
```
Mentions: Erdos12.q, Erdos12.P
lemma Erdos12.density_ineq The next scale is controlled by the square of the block count line 831 source
L4DEL explanation
density_ineq m proves 2*M (m+1) ≤ 9*(P (m+1)^4/2)^2.
1. Since M (m+1)=P (m+1)^8, the right-hand side is a constant multiple of the same eighth power after accounting for integer division by two.
2. This inequality converts the block cardinality lower bound into a uniform lower bound after division by √N.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMul.hMul, OfNat.ofNat, Erdos12.M, HAdd.hAdd, HPow.hPow, HDiv.hDiv, Erdos12.P
Proof uses: Eq, rfl, Eq.mpr, id, congrArg, Erdos12.K, Erdos12.K_ge_3, Erdos12.q, Erdos12.q_ge_5, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 77 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma density_ineq (m : ℕ) : 2 * M (m + 1) ≤ 9 * (P (m + 1) ^ 4 / 2) ^ 2 := by
…
```
Mentions: Erdos12.M, Erdos12.P
lemma Erdos12.exists_M_interval Locate every sufficiently large $N$ between consecutive block scales line 847 source
L4DEL explanation
For N≥M 7, there is an m≥7 with M m≤N<M (m+1).
1. The proof chooses the least index whose scale exceeds N and subtracts one.
2. Monotonicity and the initial lower bound ensure the preceding index exists and is at least seven.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M, OfNat.ofNat, Exists, And, GE.ge, LT.lt, HAdd.hAdd
Proof uses: Exists.intro, Erdos12.M_gt_m, id, Decidable.byContradiction, Not, Nat.find, Nat.find_spec, Eq, Erdos12.M_monotone, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mp, congrArg, HSub.hSub, Nat.find_min, Eq.mpr, And.intro
28 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma exists_M_interval (N : ℕ) (hN : M 7 ≤ N) : ∃ m ≥ 7, M m ≤ N ∧ N < M (m + 1) := by
…
```
Mentions: Erdos12.M
lemma Erdos12.density_ratio_bound Convert a square count bound into a normalized density bound line 884 source
L4DEL explanation
If C≤count and N≤9*C^2 with N>0, then 1/3≤count/√N.
1. Taking square roots gives √N≤3*C; division by the positive √N yields the ratio bound.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HPow.hPow, Real, HDiv.hDiv, Real.sqrt
Proof uses: Iff.mpr, Nat.cast_le, Eq, Eq.mpr, id, congrArg, Eq.trans, Nat.cast_mul, Nat.cast_pow, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf and 56 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma density_ratio_bound (N C count : ℕ) (h_N_pos : 0 < N) (h_count : C ≤ count) (h_N_bound : N ≤ 9 * C^2) : (1 / 3 : ℝ) ≤ (count : ℝ) / (N : ℝ).sqrt := by
…
```
lemma Erdos12.density_bound_N A uniform lower bound for every sufficiently large cutoff line 901 source
L4DEL explanation
For every N≥M 7, the normalized count |MyGoodSet∩[1,N]|/√N is at least 1/3.
1. Locate N between M m and M (m+1). If N<2*M m, use the completed previous block; otherwise use the completed current block.
2. count_interval supplies the count in either case, and density_ineq bounds N by nine times the square of that count.
3. density_ratio_bound takes square roots and divides by the positive √N to obtain the constant 1/3.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M, OfNat.ofNat, Real, HDiv.hDiv, Set.ncard, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, Real.sqrt
Proof uses: Exists, And, GE.ge, LT.lt, HAdd.hAdd, Erdos12.exists_M_interval, Set.Finite, HasSubset.Subset, Membership.mem, And.right, Set.Finite.subset, Set.finite_Icc, Erdos12.M_gt_m, Decidable.byContradiction, Not, dite, HMul.hMul, HSub.hSub, Eq, Erdos12.M_increasing and 14 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
```
lemma density_bound_N (N : ℕ) (hN : M 7 ≤ N) : (1 / 3 : ℝ) ≤ (MyGoodSet ∩ Set.Icc 1 N).ncard / (N : ℝ).sqrt := by
…
```
Mentions: Erdos12.M, Erdos12.MyGoodSet
lemma Erdos12.sum_P_pow_four Earlier fourth-power periods are dominated by the latest one line 972 source
L4DEL explanation
∑ k<m, P (k+1)^4 ≤ 2*P m^4.
1. Each successor period is at least five times the preceding period, so its fourth power more than absorbs twice the preceding accumulated bound.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.sum, Finset.range, HPow.hPow, Erdos12.P, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.mpr, id, Eq, congrArg, Finset.sum_range_succ, Erdos12.q, rfl, Erdos12.q_ge_5, Nat.mul_le_mul_left, pow_le_pow_left₀, mul_nonneg, zero_le, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble and 79 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma sum_P_pow_four (m : ℕ) : ∑ k ∈ Finset.range m, P (k + 1)^4 ≤ 2 * P m^4 := by
…
```
Mentions: Erdos12.P
lemma Erdos12.dvd_sub_of_mod_eq Equal residues make the difference divisible by the modulus line 989 source
L4DEL explanation
If a and b have the same remainder modulo c and b≤a, then c divides a-b.
1. Expanding both numbers by quotient and remainder cancels the common remainder and factors out c.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, LE.le, Dvd.dvd, HSub.hSub
Proof uses: HMul.hMul, HDiv.hDiv, HAdd.hAdd, Trans.trans, Eq.symm, Nat.div_add_mod, Eq.mpr, id, congrArg, Eq.refl, Decidable.byContradiction, Not, Nat.mul_sub_left_distrib, dvd_mul_right
22 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_sub_of_mod_eq {a b c x : ℕ} (ha : a % c = x) (hb : b % c = x) (hle : b ≤ a) : c ∣ a - b := by
…
```
lemma Erdos12.div_eq_implies_sub_lt Equal quotient cells are narrower than one period line 1002 source
L4DEL explanation
If a/P=b/P, b≤a, and P>0, then a-b<P.
1. Both numbers share the same quotient, so their difference is controlled by remainders that are each smaller than P.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HDiv.hDiv, LE.le, LT.lt, OfNat.ofNat, HSub.hSub
Proof uses: HAdd.hAdd, HMul.hMul, HMod.hMod, Nat.div_add_mod, Nat.mod_lt, Eq.mpr, id, congrArg, Eq.symm, Decidable.byContradiction, Not
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma div_eq_implies_sub_lt {a b P : ℕ} (h_div : a / P = b / P) (_hle : b ≤ a) (hP : 0 < P) : a - b < P := by
…
```
Mentions: Erdos12.P
lemma Erdos12.good_set_inj A block and quotient cell contain at most one admissible number line 1010 source
L4DEL explanation
Two numbers with the block's required residues and the same quotient (n-M m)/P m must be equal.
1. Their difference is divisible by both coprime factors K m and q m, hence by P m.
2. The shared quotient cell makes that same difference smaller than P m; the only such multiple is zero.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M, Eq, HMod.hMod, Erdos12.K, OfNat.ofNat, Erdos12.q, HDiv.hDiv, HSub.hSub, Erdos12.P
Proof uses: Nat.Coprime, Erdos12.K_q_coprime, HMul.hMul, rfl, LT.lt, Erdos12.P_pos, Or, le_total, Dvd.dvd, Erdos12.dvd_sub_of_mod_eq, Eq.mpr, id, congrArg, Nat.Coprime.mul_dvd_of_dvd_of_dvd, Nat.sub_le_sub_right, Eq.symm, Erdos12.div_eq_implies_sub_lt, Decidable.byContradiction, Not, Nat.eq_zero_of_dvd_of_lt
31 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma good_set_inj {n1 n2 m : ℕ}
  (hn1_ge : M m ≤ n1) (hn1_modK : n1 % K m = 1) (hn1_modq : n1 % q m = 0)
  (hn2_ge : M m ≤ n2) (hn2_modK : n2 % K m = 1) (hn2_modq : n2 % q m = 0)
  (h_div : (n1 - M m) / P m = (n2 - M m) / P m) : n1 = n2 := by
…
```
Mentions: Erdos12.M, Erdos12.K, Erdos12.q, Erdos12.P
lemma Erdos12.block_unique A number has only one compatible block index line 1040 source
L4DEL explanation
If n∈[M m,2*M m] and also M k≤n<M (k+1), then m=k.
1. The separation 2*M j<M (j+1) and monotonicity of M rule out either index being smaller than the other.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos12.M, HMul.hMul, OfNat.ofNat, LT.lt, HAdd.hAdd, Eq
Proof uses: Or, lt_trichotomy, Erdos12.M_monotone, Erdos12.M_increasing, Decidable.byContradiction, Not, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma block_unique {n m k : ℕ} (h1 : M m ≤ n) (h2 : n ≤ 2 * M m) (h3 : M k ≤ n) (h4 : n < M (k + 1)) : m = k := by
…
```
Mentions: Erdos12.M
def Erdos12.g_block Select the scale interval containing a number line 1049 source
L4DEL explanation
g_block n is the least k with M k≤n<M (k+1), when such a block exists; otherwise it is zero.
1. The definition uses Nat.find, so it is noncomputable but has a precise least-witness specification.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: dite, Exists, And, LE.le, Erdos12.M, LT.lt, HAdd.hAdd, OfNat.ofNat, Nat.find, Not
9 instances, coercions and auxiliary constants left out.
```
noncomputable def g_block (n : ℕ) : ℕ :=
…
```
lemma Erdos12.g_block_spec The selected block really contains the number line 1052 source
L4DEL explanation
Whenever some scale interval contains n, the selected index satisfies M (g_block n)≤n<M (g_block n+1).
1. Unfolding g_block reduces the statement to the witness specification of Nat.find.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, LE.le, Erdos12.M, LT.lt, HAdd.hAdd, OfNat.ofNat, Erdos12.g_block
Proof uses: id, Eq.mpr, dite, Nat.find, Not, Eq, congrArg, dif_pos, Nat.find_spec
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma g_block_spec {n : ℕ} (h : ∃ k, M k ≤ n ∧ n < M (k + 1)) :
  M (g_block n) ≤ n ∧ n < M (g_block n + 1) := by
…
```
Mentions: Erdos12.M, Erdos12.g_block
lemma Erdos12.my_good_set_has_block Every witness-set member lies between consecutive scales line 1058 source
L4DEL explanation
If n∈MyGoodSet, then some k satisfies M k≤n<M (k+1).
1. Membership already gives n≤2*M k, and block separation strengthens this to n<M (k+1).
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos12.MyGoodSet, Exists, And, LE.le, Erdos12.M, LT.lt, HAdd.hAdd, OfNat.ofNat
Proof uses: HMul.hMul, HDiv.hDiv, HPow.hPow, Erdos12.P, Eq, HMod.hMod, Erdos12.K, Erdos12.q, Exists.intro, And.intro, Erdos12.M_increasing, Decidable.byContradiction, Not
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma my_good_set_has_block {n : ℕ} (hn : n ∈ MyGoodSet) : ∃ k, M k ≤ n ∧ n < M (k + 1) := by
…
```
Mentions: Erdos12.MyGoodSet, Erdos12.M
def Erdos12.g_val Encode a good-set member by its block and progression cell line 1065 source
L4DEL explanation
g_val n pairs the block index containing n with the quotient (n-M k)/P k inside that block.
1. g_block chooses the scale interval M k≤n<M (k+1).
2. This coordinate map supports the separate upper bound needed to show the liminf is a finite real rather than positive infinity.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod
Proof uses: Prod.mk, Erdos12.g_block, HDiv.hDiv, HSub.hSub, Erdos12.M, Erdos12.P
4 instances, coercions and auxiliary constants left out.
```
noncomputable def g_val (n : ℕ) : ℕ × ℕ :=
…
```
lemma Erdos12.g_val_inj The block-and-cell coordinate is injective on the witness set line 1068 source
L4DEL explanation
Two members of MyGoodSet with the same g_val must be the same natural number.
1. Equality of the first coordinate gives a common block; equality of the second gives a common quotient interval of width P m.
2. Matching residues modulo coprime K m and q m make their difference divisible by P m; being smaller than P m forces that difference to vanish.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.InjOn, Nat, Prod, Erdos12.g_val, Erdos12.MyGoodSet
Proof uses: Membership.mem, Set, Eq, Erdos12.g_block, Prod.fst, Prod.mk, HDiv.hDiv, HSub.hSub, Erdos12.M, Erdos12.P, Eq.mpr, id, congrArg, Eq.refl, Prod.snd, And, LE.le, LT.lt, HAdd.hAdd, OfNat.ofNat and 13 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma g_val_inj : Set.InjOn g_val MyGoodSet := by
…
```
Mentions: Erdos12.g_val, Erdos12.MyGoodSet
def Erdos12.target_set A finite coordinate box for all earlier blocks line 1090 source
L4DEL explanation
target_set m contains pairs (k,i) with k<m and 0≤i≤P (k+1)^4/2.
1. Every good-set member up to M m maps into this finite union of block-and-cell coordinates.
2. Its deliberately slightly generous inclusive cell range makes the containment proof simple while retaining the required fourth-power bound.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Finset.biUnion, Finset.range, Finset.image, Prod.mk, Finset.Icc, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Erdos12.P, HAdd.hAdd
12 instances, coercions and auxiliary constants left out.
```
noncomputable def target_set (m : ℕ) : Finset (ℕ × ℕ) :=
…
```
lemma Erdos12.target_set_card Bound the finite code space for all earlier blocks line 1093 source
L4DEL explanation
The encoding set target_set m has at most 2*P m^4 pairs.
1. Bound the union by the sum of its per-block index ranges, absorb the endpoint term into each fourth power, and apply sum_P_pow_four.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.card, Prod, Erdos12.target_set, HMul.hMul, OfNat.ofNat, HPow.hPow, Erdos12.P
Proof uses: Finset.sum, Finset.range, Finset.image, Prod.mk, Finset.Icc, HDiv.hDiv, HAdd.hAdd, Finset.card_biUnion_le, Eq, Finset.sum_congr, rfl, Finset, Membership.mem, Set.InjOn, Set, congr_arg, Prod.snd, Eq.mpr, id, congrArg and 86 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma target_set_card (m : ℕ) : (target_set m).card ≤ 2 * P m^4 := by
…
```
Mentions: Erdos12.target_set, Erdos12.P
lemma Erdos12.g_val_maps_to Every early witness-set member has a bounded block code line 1118 source
L4DEL explanation
If n∈MyGoodSet∩[1,M m], then g_val n∈target_set m.
1. The containing block must have index k<m; equality at k=m contradicts the required residue, and a later block starts above M m.
2. The block cutoff bounds the quotient coordinate by P (k+1)^4/2, placing the pair in the corresponding finite range.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Inter.inter, Erdos12.MyGoodSet, Set.Icc, OfNat.ofNat, Erdos12.M, Prod, Finset, Erdos12.target_set, Erdos12.g_val
Proof uses: LE.le, And.right, Erdos12.g_block, And, LT.lt, HAdd.hAdd, Erdos12.g_block_spec, Erdos12.my_good_set_has_block, Or, Eq, lt_trichotomy, Eq.mpr, id, congrArg, Eq.symm, And.left, Decidable.byContradiction, Not, Erdos12.g_val_maps_to.match_1, HMul.hMul and 38 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma g_val_maps_to (m : ℕ) {n : ℕ} (hn : n ∈ MyGoodSet ∩ Set.Icc 1 (M m)) :
  g_val n ∈ target_set m := by
…
```
Mentions: Erdos12.MyGoodSet, Erdos12.M, Erdos12.g_val, Erdos12.target_set
lemma Erdos12.count_upper_bound The witness count at a block scale is at most twice a fourth power line 1161 source
L4DEL explanation
Up to M m, MyGoodSet has at most 2*P m^4 members.
1. The injective map g_val sends those members into target_set m.
2. target_set_card bounds the finite coordinate set by summing the earlier fourth powers and comparing that sum with 2*P m^4.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Set.ncard, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, OfNat.ofNat, Erdos12.M, HMul.hMul, HPow.hPow, Erdos12.P
Proof uses: HasSubset.Subset, Prod, Set.image, Erdos12.g_val, Finset, Erdos12.target_set, Membership.mem, And, Eq, Erdos12.g_val_maps_to, Set.Finite, Set.Finite.subset, Set.finite_Icc, And.right, Set.ncard_le_ncard, Finset.finite_toSet, Set.InjOn, Set.InjOn.mono, And.left, Erdos12.g_val_inj and 8 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma count_upper_bound (m : ℕ) : (MyGoodSet ∩ Set.Icc 1 (M m)).ncard ≤ 2 * P m^4 := by
…
```
Mentions: Erdos12.MyGoodSet, Erdos12.M, Erdos12.P
lemma Erdos12.exists_f_le_two The normalized count is at most two infinitely often line 1179 source
L4DEL explanation
Along the unbounded subsequence N=M m, the ratio |MyGoodSet∩[1,N]|/√N is at most 2.
1. count_upper_bound gives the numerator bound 2*P m^4.
2. Since M m=P m^8, its real square root is exactly P m^4, giving the ratio bound after cancellation.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Frequently, Nat, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, OfNat.ofNat, Real.sqrt, Filter.atTop
Proof uses: Iff.mpr, Exists, And, GE.ge, Filter.frequently_atTop, Exists.intro, Erdos12.M, And.intro, LT.lt.le, Erdos12.M_gt_m, HMul.hMul, HPow.hPow, Erdos12.P, Erdos12.count_upper_bound, Eq, rfl, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq and 43 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma exists_f_le_two : ∃ᶠ N in Filter.atTop, (MyGoodSet ∩ Set.Icc 1 N).ncard / (N : ℝ).sqrt ≤ 2 := by
…
```
Mentions: Erdos12.MyGoodSet
lemma Erdos12.bdd_above_of_frequently_le A frequent upper bound caps every eventual lower bound line 1206 source
L4DEL explanation
If f N≤c frequently, then the set of real numbers that are eventually below f N is bounded above by c.
1. A frequent occurrence of f N≤c intersects any eventual assertion a≤f N, producing one index with a≤c.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Filter.Frequently, LE.le, Filter.atTop, BddAbove, setOf, Filter.Eventually
Proof uses: Exists.intro, Membership.mem, Set, upperBounds, And, Filter.Frequently.and_eventually, Exists, Filter.Frequently.exists, le_trans
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma bdd_above_of_frequently_le {f : ℕ → ℝ} {c : ℝ} (h : ∃ᶠ N in Filter.atTop, f N ≤ c) :
  BddAbove {a | ∀ᶠ N in Filter.atTop, a ≤ f N} := by
…
```
lemma Erdos12.my_good_set_density The normalized counting function has positive lower limit line 1214 source
L4DEL explanation
The liminf of |MyGoodSet∩[1,N]|/√N is at least 1/3, hence strictly positive.
1. density_bound_N supplies the eventual lower bound 1/3.
2. exists_f_le_two supplies a frequently occurring upper bound, which proves the set of eventual lower bounds is bounded above and lets the proof use the real-valued liminf characterization safely.
3. The proof then applies le_csSup to obtain 1/3≤liminf and concludes positivity.
Sources and attribution: Pinned Lean source (0647711a7118)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, OfNat.ofNat, Filter.liminf, Nat, HDiv.hDiv, Set.ncard, Inter.inter, Set, Erdos12.MyGoodSet, Set.Icc, Real.sqrt, Filter.atTop
Proof uses: Filter.Eventually, LE.le, Eq.mpr, Exists, GE.ge, id, Eq, congrArg, propext, Filter.eventually_atTop, Exists.intro, Erdos12.M, Erdos12.density_bound_N, BddAbove, setOf, Erdos12.bdd_above_of_frequently_le, Erdos12.exists_f_le_two, le_csSup, Filter.map, lt_of_not_ge and 78 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma my_good_set_density : (0 : ℝ) < Filter.atTop.liminf (fun N => (MyGoodSet ∩ Set.Icc 1 N).ncard / (N : ℝ).sqrt) := by
…
```
Mentions: Erdos12.MyGoodSet
theorem Erdos12.target_theorem_0 Erdős problem 12(i): a dense infinite set avoiding the divisibility pattern line 1228 source
L4DEL explanation
We will construct a sequence of “blocks” that individually cannot contain such a, b, c
— Human-written proof companion for Erdős 12(i)
divides the sum of two larger terms
— Paul Erdős and András Sárközy (1970), p. 97
There exists an infinite set A of natural numbers with no distinct a,b,c in A satisfying a < b, a < c, and a ∣ b+c, while |A ∩ [1,N]|/√N has positive lower limit.
1. The Lean proof witnesses the existential with MyGoodSet, whose prime and Chinese-remainder congruences establish IsGood and whose arithmetic-progression blocks establish an eventual normalized count of at least 1/3.
2. The reverse implication is logically trivial because the left side is answer(True); the mathematical content is the forward construction of the set.
3. Provenance boundary: the human-written companion proves the same theorem by a different construction using a base-2-to-base-3 map and progression-free blocks. Those proof details are not attributed to the Lean declarations above.
4. Erdős and Sárközy introduced property P and exhibited a weaker square-root-over-logarithm example in 1970; this theorem supplies the positive square-root-scale liminf asked for in problem 12(i).
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 12(i), Erdős Problems 12 source record, Paul Erdős and András Sárközy (1970), p. 97
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, True, Exists, Set, Nat, And, Erdos12.IsGood, LT.lt, Real, OfNat.ofNat, Filter.liminf, HDiv.hDiv, Set.ncard, Inter.inter, Set.Icc, Real.sqrt, Filter.atTop
Proof uses: Iff.intro, Exists.intro, Erdos12.MyGoodSet, And.intro, Erdos12.my_good_set_is_good, Erdos12.my_good_set_density, True.intro
26 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/ErdosProblems/erdos_12.parts.ii.lean:762 (different declaration text). Qualify references as Erdos12.target_theorem_0@path.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(True) ↔ ∃ (A : Set ℕ), IsGood A ∧ (0 : ℝ) < Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ).sqrt) := by
…
```
Mentions: Erdos12.IsGood