erdos_152.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

64 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def Erdos152.f Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n line 27 source
Source documentation
Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: iInf, Set, setOf, And, Eq, Set.ncard, IsSidon, Not, Membership.mem, HAdd.hAdd, HSub.hSub, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
noncomputable def f (n : ℕ) : ℕ :=
…
```
def Erdos152.num_isolated line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, setOf, And, Not, Membership.mem, HAdd.hAdd, HSub.hSub, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
def Erdos152.N_k_N line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
def Erdos152.N_k_Z line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
def Erdos152.V_2_N line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, HSub.hSub, OfNat.ofNat, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
def Erdos152.I_N line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, Not, HSub.hSub, OfNat.ofNat, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
def Erdos152.D_set line 76 source
no axioms what this means
Statement uses: Set, Nat, Int
Proof uses: setOf, Exists, And, Membership.mem, Eq, HSub.hSub
5 instances, coercions and auxiliary constants left out.
def Erdos152.ind line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int
Proof uses: ite, Membership.mem, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
lemma Erdos152.H_val line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Erdos152.ind, HAdd.hAdd, OfNat.ofNat, GE.ge, HMul.hMul
Proof uses: id, dite, ite, Membership.mem, Eq.mpr, Eq, congr, congrArg, if_pos, Decidable.byContradiction, Not, if_neg
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.sum_H line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Finset, GE.ge, Finset.sum, HAdd.hAdd, Erdos152.ind, OfNat.ofNat, HMul.hMul
Proof uses: Finset.sum_le_sum, Membership.mem, Erdos152.H_val
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.universal_parity_3 line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Erdos152.N_k_Z, Set.ncard
Proof uses: Eq.mpr, Finset.card, Set.Finite.toFinset, id, Eq, congrArg, Exists.elim, Real, NNReal, Eq.dvd, NNReal.coe_zero, Set.ncard_eq_toFinset_card, Trans.simple, setOf, And, Membership.mem, Nat.card, Subtype, Finset, Finset.filter and 63 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def Erdos152.Z_S line 106 source
no axioms what this means
Statement uses: Set, Nat, Int
Proof uses: Set.image
2 instances, coercions and auxiliary constants left out.
def Erdos152.I_Z line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, Not, HSub.hSub, OfNat.ofNat, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
def Erdos152.V_2_Z line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Nat
Proof uses: Set.ncard, setOf, And, Membership.mem, HSub.hSub, OfNat.ofNat, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
def Erdos152.C_set_Z line 110 source
no axioms what this means
Statement uses: Set, Int
Proof uses: setOf, And, Membership.mem, Not, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
lemma Erdos152.I_identity_Z line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, Eq, Nat, HAdd.hAdd, Erdos152.I_Z, HMul.hMul, OfNat.ofNat, Erdos152.N_k_Z, Set.ncard, Erdos152.V_2_Z
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, eq_comm, setOf, And, Membership.mem, Not, HSub.hSub, Erdos152.I_Z.eq_1, two_mul, Erdos152.N_k_Z.eq_1, Erdos152.V_2_Z.eq_1, Finset.card, Set.Finite.toFinset, Set.ncard_eq_toFinset_card, Finset.filter, Or and 40 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Erdos152.C1 line 120 source
no axioms what this means
Statement uses: Set, Int
Proof uses: setOf, And, Membership.mem, Erdos152.C_set_Z, Not, HSub.hSub, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
def Erdos152.C2 line 121 source
no axioms what this means
Statement uses: Set, Int
Proof uses: setOf, And, Membership.mem, Erdos152.C_set_Z, Not, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
def Erdos152.C3 line 122 source
no axioms what this means
Statement uses: Set, Int
Proof uses: setOf, And, Membership.mem, Erdos152.C_set_Z, HSub.hSub, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
def Erdos152.C4 line 123 source
no axioms what this means
Statement uses: Set, Int
Proof uses: setOf, And, Membership.mem, Erdos152.C_set_Z, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
lemma Erdos152.C_bound line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, And, LE.le, Nat, Set.ncard, Erdos152.C_set_Z, HAdd.hAdd, Erdos152.C1, Erdos152.C3, Erdos152.C2, Erdos152.C4
Proof uses: id, And.intro, setOf, Membership.mem, Not, OfNat.ofNat, HSub.hSub, LE.le.trans_eq, Inter.inter, SDiff.sdiff, Eq.ge, Set.ncard_inter_add_ncard_diff_eq_ncard, Set.Finite.sep, add_comm
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.C1_bound line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, Set.ncard, Erdos152.C1, Erdos152.I_Z
Proof uses: id, Nat.card_mono, setOf, And, Membership.mem, Erdos152.C_set_Z, Not, HSub.hSub, OfNat.ofNat, HAdd.hAdd, Set.Finite.sep, And.rec, Erdos152.C1_bound.match_1
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.C2_bound line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, Set.ncard, Erdos152.C2, Erdos152.I_Z
Proof uses: id, Nat.card, setOf, And, Membership.mem, Erdos152.C_set_Z, Not, HAdd.hAdd, OfNat.ofNat, HSub.hSub, LE.le.trans, Inter.inter, Set.image, Eq.ge, Nat.card_image_of_injective, add_left_injective, Nat.card_mono, Set.Finite.sep, Iff.mpr, HasSubset.Subset and 20 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.C34_bound line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, HAdd.hAdd, Set.ncard, Erdos152.C3, Erdos152.C4, Erdos152.N_k_Z, OfNat.ofNat
Proof uses: id, Eq.mpr, setOf, And, Membership.mem, Erdos152.C_set_Z, HSub.hSub, Not, Eq, congrArg, congr, funext, Eq.trans, Inter.inter, Set.sep_and, dite, Trans.simple, Finset.card, Union.union, Finset and 42 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.local_pattern_C_Z line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, HMul.hMul, OfNat.ofNat, Set.ncard, Erdos152.C_set_Z, HAdd.hAdd, Erdos152.N_k_Z, Erdos152.I_Z
Proof uses: And, Erdos152.C1, Erdos152.C3, Erdos152.C2, Erdos152.C4, Erdos152.C_bound, Erdos152.C1_bound, Erdos152.C2_bound, Erdos152.C34_bound, Decidable.byContradiction, Not
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.local_pattern_bound_Z_hN line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, Eq, Nat, Erdos152.N_k_Z, OfNat.ofNat, HAdd.hAdd, Erdos152.V_2_Z, Set.ncard, Erdos152.C_set_Z
Proof uses: id, setOf, And, Membership.mem, HSub.hSub, Not, Eq.mpr, congrArg, rfl, Set.Finite.subset, And.left, Union.union, Set.ext, Iff, Or, Iff.intro, And.intro, Erdos152.local_pattern_bound_Z_hN.match_1, dite, Or.inl and 19 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.local_pattern_bound_Z line 212 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Int, Set.Finite, LE.le, Nat, HMul.hMul, OfNat.ofNat, Erdos152.N_k_Z, HAdd.hAdd, Erdos152.V_2_Z, Erdos152.I_Z
Proof uses: Set.ncard, Erdos152.C_set_Z, Erdos152.local_pattern_C_Z, Eq, Erdos152.local_pattern_bound_Z_hN, Decidable.byContradiction, Not
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.num_isolated_Z_rel line 218 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LE.le, Erdos152.I_Z, Erdos152.Z_S, HAdd.hAdd, Erdos152.num_isolated, OfNat.ofNat
Proof uses: Eq.mpr, Set.ncard, Int, setOf, And, Exists, Membership.mem, Eq, Not, HSub.hSub, id, congrArg, Set.image, funext, congr, Eq.trans, dite, Set.Finite, LE.le.trans, Nat.card and 32 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_k_Z_rel_1 line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos152.N_k_Z, Erdos152.Z_S, HAdd.hAdd, OfNat.ofNat, Int, Erdos152.N_k_N
Proof uses: id, Eq.trans, Set.ncard, setOf, And, Membership.mem, Set.image, congr_arg, Set.ext, Set.ncard_image_of_injective, Nat.cast_injective
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_k_Z_rel_2 line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos152.N_k_Z, Erdos152.Z_S, HAdd.hAdd, OfNat.ofNat, Int, Erdos152.N_k_N
Proof uses: Eq.mpr, Set.ncard, setOf, And, Exists, Membership.mem, id, congrArg, Set.image, funext, congr, Eq.trans, congr_arg, Set.ext, Iff.intro, And.elim, Exists.elim, Eq.rec, cast, Eq.symm and 18 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_k_Z_rel_3 line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos152.N_k_Z, Erdos152.Z_S, HAdd.hAdd, OfNat.ofNat, Int, Erdos152.N_k_N
Proof uses: id, Function.comp, Function.Injective, Set.ncard, Set.image, setOf, And, Membership.mem, Eq.trans, congr_arg, Set.ext, Iff.intro, Erdos152.N_k_Z_rel_3.match_1, Exists.intro, And.intro, HEq, Eq.refl, HEq.refl, Eq.symm, Erdos152.N_k_Z_rel_3.match_2 and 6 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.Z_S_card line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Set.ncard, Int, Erdos152.Z_S, HAdd.hAdd
Proof uses: id, Set.ncard_image_of_injective, Nat.cast_injective
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Erdos152.quad_k_N line 244 source
no axioms what this means
Statement uses: Set, Nat, Prod
Proof uses: setOf, And, Membership.mem, Prod.fst, Prod.snd, Eq, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
lemma Erdos152.quad_upper_Q0 line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, GT.gt, OfNat.ofNat, LE.le, Set.ncard, Prod, setOf, And, Membership.mem, Erdos152.quad_k_N, Eq, Int, HSub.hSub, Prod.fst, Prod.snd
Proof uses: id, Eq.mpr, HAdd.hAdd, congrArg, funext, congr, add_assoc, Eq.trans, LE.le.trans, Nat.card, Set.image, Eq.ge, Nat.card_image_of_injOn, Or, And.left, And.right, And.elim, Decidable.byContradiction, Not, Or.inl and 10 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_Qk_inj line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, GT.gt, OfNat.ofNat, Set.InjOn, Prod, Prod.fst, Prod.snd, setOf, And, Membership.mem, Erdos152.quad_k_N, Eq, Int, HSub.hSub, Neg.neg
Proof uses: HAdd.hAdd, Iff.mpr, Prod.ext_iff, And.elim, Eq.mpr, id, congrArg, Eq.trans, True, congr, eq_self, true_and, Or, Prod.mk, Eq.mp, funext, add_right_comm, AddCommGroup, propext, Function.Injective.eq_iff' and 12 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_Qk_im line 259 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, GT.gt, OfNat.ofNat, HasSubset.Subset, Set.image, Prod, Prod.fst, Prod.snd, setOf, And, Membership.mem, Erdos152.quad_k_N, Eq, Int, HSub.hSub, Neg.neg
Proof uses: Iff.mpr, Set.preimage, Set.image_subset_iff, And.elim, HAdd.hAdd, And.intro, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_Qk line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, GT.gt, OfNat.ofNat, LE.le, Set.ncard, Prod, setOf, And, Membership.mem, Erdos152.quad_k_N, Eq, Int, HSub.hSub, Prod.fst, Prod.snd, Neg.neg
Proof uses: Set.InjOn, Erdos152.quad_upper_Qk_inj, HasSubset.Subset, Set.image, Erdos152.quad_upper_Qk_im, Set.MapsTo, Set.Finite.of_injOn, Eq.mp, Set.preimage, congrArg, propext, Set.image_subset_iff, Set.ncard_image_of_injOn, Set.ncard_le_ncard, Decidable.byContradiction, Not
23 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_other_inj line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.InjOn, Prod, Int, HSub.hSub, Prod.fst, Prod.snd, setOf, And, Membership.mem, Erdos152.quad_k_N, Ne, OfNat.ofNat, Neg.neg
Proof uses: Eq, HAdd.hAdd, Erdos152.quad_upper_other_inj.match_2, Erdos152.quad_upper_other_inj.match_1, Eq.mpr, id, Eq.trans, congrArg, Or, eq_or_ne, Or.inl, Not, Prod.mk, Eq.mp, funext, add_assoc, True, congr, eq_true, true_and and 24 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_other_im line 281 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, HasSubset.Subset, Int, Set.image, Prod, HSub.hSub, Prod.fst, Prod.snd, setOf, And, Membership.mem, Erdos152.quad_k_N, Ne, OfNat.ofNat, Neg.neg, Erdos152.D_set, HAdd.hAdd
Proof uses: id, Eq.mpr, Eq, Not, Set.preimage, Exists, Eq.trans, congrArg, funext, congr, Prod.mk, forall_congr, implies_congr, Eq.refl, And.intro, Exists.intro, rfl, Decidable.byContradiction
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_other line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, LE.le, Set.ncard, Prod, setOf, And, Membership.mem, Erdos152.quad_k_N, Ne, Int, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat, Neg.neg, Erdos152.N_k_Z, Erdos152.D_set
Proof uses: Set.InjOn, Erdos152.quad_upper_other_inj, HasSubset.Subset, Set.image, HAdd.hAdd, Erdos152.quad_upper_other_im, id, Set.Finite.sep, Exists, Eq, Set.Finite.subset, Prod.rec, SProd.sprod, Set.Finite.image, Set.Finite.prod, Erdos152.quad_upper_other.match_1, Exists.intro, Prod.mk, And.intro, Eq.symm and 4 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_part line 298 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, LE.le, Set.ncard, Prod, Erdos152.quad_k_N, HAdd.hAdd, setOf, And, Membership.mem, Eq, Int, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat, Neg.neg, Ne
Proof uses: Function.comp, Union.union, Eq.trans_le, congr_arg, Set.ext, LE.le.trans, Set.ncard_union_le, Nat.add_le_add_right
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, GT.gt, OfNat.ofNat, LE.le, Set.ncard, Prod, Erdos152.quad_k_N, HAdd.hAdd, Erdos152.N_k_Z, Erdos152.D_set, Int, HMul.hMul
Proof uses: setOf, And, Membership.mem, Eq, HSub.hSub, Prod.fst, Prod.snd, Neg.neg, Ne, Erdos152.quad_upper_part, Erdos152.quad_upper_Q0, Erdos152.quad_upper_Qk, Erdos152.quad_upper_other, Decidable.byContradiction, Not
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Erdos152.S_good line 312 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: setOf, And, Membership.mem, HAdd.hAdd, Not, Exists, Eq, HMul.hMul, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
def Erdos152.quad_fiber line 314 source
no axioms what this means
Statement uses: Set, Nat, Prod
Proof uses: setOf, And, Membership.mem, SProd.sprod, Eq, HAdd.hAdd, Prod.fst, Prod.snd
4 instances, coercions and auxiliary constants left out.
lemma Erdos152.quad_fiber_subset line 317 source
standard axioms: propext what this means
Statement uses: Set, Nat, Set.Finite, HasSubset.Subset, Prod, Erdos152.quad_fiber, Erdos152.quad_k_N
Proof uses: setOf, And, Membership.mem, SProd.sprod, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Erdos152.quad_fiber_subset.match_1, Iff.mpr, Set.mem_setOf, of_eq_true, Eq.trans, True, congr, congrArg, eq_true, And.left, True.intro, And.right and 2 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_fiber_card line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, Membership.mem, Erdos152.S_good, LE.le, OfNat.ofNat, Set.ncard, Prod, Erdos152.quad_fiber
Proof uses: id, Finset, Eq, Exists, setOf, And, SProd.sprod, HAdd.hAdd, Prod.fst, Prod.snd, Set.Finite.exists_finset_coe, Eq.mpr, Inter.inter, congrArg, funext, Eq.trans, congr, Trans.simple, Finset.card, Finset.filter and 104 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_fiber_disjoint line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, Ne, Disjoint, Prod, Erdos152.quad_fiber
Proof uses: id, Iff.mpr, setOf, And, Membership.mem, SProd.sprod, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Not, Set.disjoint_left, Eq.rec, And.left, And.right
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_lower_sub_fin line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, Erdos152.S_good
Proof uses: id, Set.Finite.sep, HAdd.hAdd, Set.Finite.add, And, Membership.mem, Not, Exists, Eq, HMul.hMul, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_lower_sub line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, LE.le, HMul.hMul, OfNat.ofNat, Set.ncard, Erdos152.S_good, Prod, Erdos152.quad_k_N
Proof uses: Erdos152.quad_lower_sub_fin, Set.iUnion, Membership.mem, Erdos152.quad_fiber, HasSubset.Subset, iSup₂_le, Erdos152.quad_lower_sub.match_1, SProd.sprod, And, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Iff.mpr, setOf, Set.mem_setOf, of_eq_true, Eq.trans, True, congr and 102 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_lower_edges line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, LE.le, Erdos152.N_k_N, HAdd.hAdd, Set.ncard, Erdos152.S_good, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, two_mul, setOf, And, Membership.mem, Erdos152.N_k_N.eq_1, Not, Exists, Erdos152.S_good.eq_1, Trans.simple, Union.union, Set.image, HSub.hSub, LE.le.trans, Set.ncard_le_ncard, Iff.mpr, Or and 22 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_lower line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, LE.le, HMul.hMul, OfNat.ofNat, Erdos152.N_k_N, HAdd.hAdd, Set.ncard, Prod, Erdos152.quad_k_N
Proof uses: Erdos152.S_good, Erdos152.quad_lower_sub, Erdos152.quad_lower_edges, Decidable.byContradiction, Not
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_lower_2 line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, LE.le, Erdos152.N_k_Z, Erdos152.D_set, Int, HAdd.hAdd, Set.ncard, Prod, Erdos152.quad_k_N, HMul.hMul, OfNat.ofNat
Proof uses: id, Eq.mpr, setOf, And, Membership.mem, Eq, congrArg, two_mul, Exists, HSub.hSub, dite, Nat.card, Prod.fst, Prod.snd, SProd.sprod, Trans.simple, Subtype, Finset, Finset.image, Set.Finite.toFinset and 30 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.quad_upper_2 line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsSidon, Set.Finite, LE.le, Set.ncard, Prod, Erdos152.quad_k_N, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Erdos152.N_k_N
Proof uses: id, Finset, Eq, Exists, Nat.card, setOf, And, Membership.mem, Prod.fst, Prod.snd, CanLift.prf, Trans.simple, Finset.card, Finset.filter, SProd.sprod, Eq.rec, Subtype, Eq.ge, congr_arg, of_eq_true and 76 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_bound_upper_1 line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, IsSidon, LE.le, HMul.hMul, OfNat.ofNat, Erdos152.N_k_N, HAdd.hAdd, Erdos152.N_k_Z, Erdos152.D_set, Int, Set.ncard
Proof uses: Prod, Erdos152.quad_k_N, Erdos152.quad_lower, Erdos152.quad_upper, Decidable.byContradiction, GT.gt, Not
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_bound_lower_2 line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, IsSidon, LE.le, Erdos152.N_k_Z, Erdos152.D_set, OfNat.ofNat, Int, HAdd.hAdd, HMul.hMul, Erdos152.N_k_N, Set.ncard
Proof uses: Prod, Erdos152.quad_k_N, Erdos152.quad_lower_2, Erdos152.quad_upper_2, Decidable.byContradiction, Not
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.N_bound_upper_3 line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, IsSidon, LE.le, HMul.hMul, OfNat.ofNat, Erdos152.N_k_N, HAdd.hAdd, Erdos152.N_k_Z, Erdos152.D_set, Int, Set.ncard
Proof uses: Prod, Erdos152.quad_k_N, Erdos152.quad_lower, Erdos152.quad_upper, Decidable.byContradiction, GT.gt, Not
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.D_set_card line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, LE.le, Set.ncard, Int, Erdos152.D_set, HMul.hMul
Proof uses: id, Eq.mpr, setOf, Exists, And, Membership.mem, Eq, HSub.hSub, congrArg, mul_comm, Eq.rec, Prod, SProd.sprod, LE.le.trans, Nat.card, Set.image, Prod.rec, Nat.card_mono, Set.Finite.image, Set.Finite.prod and 11 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.S_card line 431 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, IsSidon, GE.ge, HMul.hMul, OfNat.ofNat, Set.ncard, HAdd.hAdd
Proof uses: Finset, Eq, Exists, CanLift.prf, Eq.mpr, id, congr, congrArg, Eq.symm, Finset.card, Eq.trans, Set.ncard_coe_finset, LE.le, propext, ge_iff_le, two_mul, Eq.rec, Prod, SProd.sprod, LE.le.trans and 36 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.num_isolated_lower_bound line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Set, Eq, Set.ncard, IsSidon, GE.ge, HAdd.hAdd, HMul.hMul, Erdos152.num_isolated
Proof uses: Set.Finite, Set.finite_of_ncard_pos, Decidable.byContradiction, LT.lt, Not, Set.Finite.add, Int, Erdos152.Z_S, id, Set.Finite.image, Erdos152.D_set, Eq.mpr, setOf, Exists, And, Membership.mem, HSub.hSub, congrArg, funext, Set.Finite.subset and 31 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.exists_sidon_set_n line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Set, And, Eq, Set.ncard, IsSidon
Proof uses: id, Exists.intro, Membership.mem, HAdd.hAdd, Or, Set.image, HPow.hPow, OfNat.ofNat, Finset, Finset.range, And.intro, cast, Finset.card, Finset.image, Eq.symm, congrArg, Eq.trans, Set.ncard_coe_finset, of_eq_true, True and 94 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.f_lower_bound_div line 477 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, Erdos152.f, HDiv.hDiv, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Or, Eq, GT.gt, Nat.eq_zero_or_pos, Or.inl, Decidable.byContradiction, Not, Eq.symm, Or.inr, Erdos152.f_lower_bound_div.match_1, Exists, Set, And, Set.ncard, IsSidon, Erdos152.exists_sidon_set_n, Nonempty, setOf, Nonempty.intro, Subtype.mk and 12 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.tendsto_bound line 494 source
standard axioms: Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, HDiv.hDiv, HSub.hSub, HMul.hMul, OfNat.ofNat, Filter.atTop
Proof uses: Iff.mpr, Filter.Eventually, LE.le, Filter.tendsto_atTop, Filter.mp_mem, setOf, HAdd.hAdd, Filter.mem_atTop, Membership.mem, Set, Filter.univ_mem', id, Function.comp, Decidable.byContradiction, Not, Nat.mul_le_mul_right
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos152.tendsto_f line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Erdos152.f, Filter.atTop
Proof uses: Filter.Eventually, LE.le, HDiv.hDiv, HSub.hSub, HMul.hMul, OfNat.ofNat, Filter.mp_mem, setOf, Filter.eventually_ge_atTop, Filter.univ_mem', Membership.mem, Set, id, Erdos152.f_lower_bound_div, Filter.tendsto_atTop_mono', Erdos152.tendsto_bound
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Erdos152.target_theorem_0 Erdős problem 152: Sidon sumsets have quadratically many isolated sums line 505 source
L4DEL explanation
The proof establishes, for every Sidon set A of size n: 16 · I(A + A) + 100n + 16 ≥ n².
— Human-written proof companion for Erdős 152
suppose that the sums aᵢ+aⱼ (where i≤j) are all different. Such sequences, called B₂ sequences by Sidon
— Paul Erdős and Pál Turán (1941), original paper, p. 212
If f(n) is the minimum number of isolated elements in A+A over Sidon sets A of size n, then f(n) tends to infinity. In fact the formal proof derives the quantitative lower bound (n²-100n-16)/16.
1. Count neighbour pairs at distances 1, 2, and 3 in the sumset and relate them to isolated and interior points.
2. Use the Sidon property to control how often additive representations and short differences can coincide.
3. Combining the counting inequalities yields 16·I(A+A)+100n+16 ≥ n², and the quadratic lower bound forces divergence.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 152, Erdős Problems 152 source record, Paul Erdős and Pál Turán (1941), original paper, p. 212
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, Erdos152.f, Filter.atTop
Proof uses: Iff.intro, Erdos152.tendsto_f, True.intro
2 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(
  -- EVOLVE-VALUE-START
  True
  -- EVOLVE-VALUE-END
  ) ↔ Tendsto f atTop atTop := by
…
```
Mentions: Erdos152.f