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

54 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def A258667_inner_sum The inner sum of the formula used in A258667: $$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ line 46 source
Source documentation
The inner sum of the formula used in A258667: $$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$
```
private def A258667_inner_sum (n k : ℕ) : ℤ :=
…
```
def A258667 A258667: A total of $n$ married couples, including a mathematician M and his wife, are to be seated at the $2n$ chairs around a circular table, with no man seated next to his wife line 60 source
Source documentation
A258667: A total of $n$ married couples, including a mathematician M and his wife, are to be seated at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies are seated at every other chair, M is the first man allowed to choose one of the remaining chairs. The sequence gives the number of ways of seating the other men, with no man seated next to his wife, if M chooses the chair that is 9 seats clockwise from his wife's chair.
$$a(n) = \begin{cases} 0 & \text{if } n \le 5 \\ \sum_{k=0}^{n-1}(-1)^k(n-k-1)! \sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j} & \text{if } n > 5 \end{cases}$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: dite, LE.le, OfNat.ofNat, Not, Int.natAbs, Finset.sum, Int, Finset.range, ite, Eq, HMod.hMod, Neg.neg, Int.ofNat, Nat.factorial, HSub.hSub, HMul.hMul
14 instances, coercions and auxiliary constants left out.
```
def A258667 (n : ℕ) : ℕ :=
…
```
def nat_fac_to_real line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Nat.factorial
2 instances, coercions and auxiliary constants left out.
def menage_denom_term The denominator term $k! (n-1)_k$ represented as a Real number line 73 source
Source documentation
The denominator term $k! (n-1)_k$ represented as a Real number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: nat_fac_to_real, Nat.descFactorial, HSub.hSub, OfNat.ofNat, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
noncomputable def menage_denom_term (n k : ℕ) : ℝ :=
…
```
def A258667_asymptotic_sum_part The infinite series part of the asymptotic expansion: $\sum_{k \ge 1} \frac{(-1)^k}{k!(n-1)_k}$ line 80 source
Source documentation
The infinite series part of the asymptotic expansion: $\sum_{k \ge 1} \frac{(-1)^k}{k!(n-1)_k}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.range, ite, Eq, OfNat.ofNat, menage_denom_term, HDiv.hDiv, HPow.hPow, Neg.neg
15 instances, coercions and auxiliary constants left out.
```
noncomputable def A258667_asymptotic_sum_part (n : ℕ) : ℝ :=
…
```
def A258667_asymptotic_term The proposed asymptotic expression for A258667(n) line 91 source
Source documentation
The proposed asymptotic expression for A258667(n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: ite, LE.le, OfNat.ofNat, nat_fac_to_real, HMul.hMul, Real.exp, Neg.neg, HDiv.hDiv, HSub.hSub, HAdd.hAdd, A258667_asymptotic_sum_part
21 instances, coercions and auxiliary constants left out.
```
noncomputable def A258667_asymptotic_term (n : ℕ) : ℝ :=
…
```
lemma inner_sum_zero line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int
Proof uses: id, Eq.rec, Max.max, Min.min, Finset.sum, Finset.Icc, Nat.choose, HSub.hSub, HAdd.hAdd, HMul.hMul, Int.ofNat, Eq.trans, add_zero, congr_arg, Nat.choose_zero_right, Eq.symm, Nat.sub_eq_zero_of_le
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma inner_sum_one line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Int, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Finset.sum, Finset.Icc, Nat.choose, HAdd.hAdd, id, congr, Max.max, Min.min, Int.ofNat, congrArg, Finset.sum_congr, Finset, Eq.trans, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, sup_of_le_right, of_eq_true and 29 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma asymp_sum_limit line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, A258667_asymptotic_sum_part, Filter.atTop, nhds, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.sum, Finset.range, ite, Eq, menage_denom_term, HDiv.hDiv, HPow.hPow, Neg.neg, Finset.filter, And, Not, nat_fac_to_real, LE.le, HSub.hSub, Finset.erase, HMul.hMul, Nat.descFactorial, congrArg and 119 more
213 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma asymp_sum_plus_one_limit line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HAdd.hAdd, OfNat.ofNat, A258667_asymptotic_sum_part, Filter.atTop, nhds
Proof uses: id, Eq.mpr, LE.le, Filter, Filter.map, Finset.sum, Finset.range, ite, Eq, menage_denom_term, HDiv.hDiv, HPow.hPow, Neg.neg, Finset.filter, And, Not, nat_fac_to_real, HSub.hSub, Finset.erase, HMul.hMul and 138 more
261 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma asymp_sum_equiv_one line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, HAdd.hAdd, OfNat.ofNat, A258667_asymptotic_sum_part
Proof uses: Eq.mpr, Exists, And, Filter.Tendsto, nhds, Filter.EventuallyEq, Finset.sum, Finset.range, ite, Eq, menage_denom_term, HDiv.hDiv, HPow.hPow, Neg.neg, HMul.hMul, id, Eq.trans, congrArg, funext, Finset.sum_congr and 125 more
239 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma ratio_identity line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, HDiv.hDiv, HSub.hSub, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, one_add_div, Iff.mpr, Ne, sub_ne_zero, cast, Not, Eq.symm, LT.lt.ne', sub_add_cancel, Eq.refl
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma term_two_div_limit line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, OfNat.ofNat, HSub.hSub, Filter.atTop, nhds
Proof uses: Filter.Tendsto.const_div_atTop, HAdd.hAdd, Neg.neg, Filter.Tendsto.atTop_add, tendsto_natCast_atTop_atTop, tendsto_const_nhds
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma prefactor_ratio_limit line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HSub.hSub, OfNat.ofNat, Filter.atTop, nhds
Proof uses: Filter.Tendsto.congr, HAdd.hAdd, Neg.neg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Inv.inv, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.neg_add and 25 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma prefactor_frac_equiv line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, HDiv.hDiv, nat_fac_to_real, HSub.hSub, OfNat.ofNat
Proof uses: id, Eq.mpr, Nat.factorial, Exists, Filter.Tendsto, nhds, Filter.EventuallyEq, HMul.hMul, Eq, Exists.intro, HAdd.hAdd, Neg.neg, tendsto_natCast_div_add_atTop, Rat, NNRat, Iff.mpr, Filter.Eventually, GE.ge, Filter.eventually_atTop, asymp_sum_plus_one_limit.match_3 and 45 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma prefactor_equiv line 206 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, HDiv.hDiv, nat_fac_to_real, HSub.hSub
Proof uses: id, Eq.mpr, Nat.factorial, Eq, congrArg, funext, mul_div, Exists, Filter.Tendsto, nhds, Filter.EventuallyEq, Exists.intro, HAdd.hAdd, tendsto_natCast_div_add_atTop, Rat, NNRat, Iff.mpr, Filter.Eventually, GE.ge, Filter.eventually_atTop and 22 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma asymp_term_def_eventually line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Eventually, Nat, Eq, Real, A258667_asymptotic_term, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, HDiv.hDiv, nat_fac_to_real, HSub.hSub, HAdd.hAdd, A258667_asymptotic_sum_part, Filter.atTop
Proof uses: Eq.mpr, id, congrArg, funext, mul_assoc, ite, LE.le, ite_congr, Eq.refl, Not, Finset.sum, Finset.range, menage_denom_term, HPow.hPow, congr, Finset.sum_congr, Finset, Membership.mem, Filter.Eventually.mono, LT.lt and 3 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma asymp_term_equiv line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, A258667_asymptotic_term, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, nat_fac_to_real, HSub.hSub
Proof uses: id, Eq.mpr, ite, LE.le, Nat.factorial, Complex.re, Complex.exp, HDiv.hDiv, HAdd.hAdd, A258667_asymptotic_sum_part, Exists, And, Filter.Tendsto, nhds, Filter.EventuallyEq, Finset.sum, Finset.range, Eq, menage_denom_term, HPow.hPow and 280 more
330 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
def seq_sum line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: Finset.sum, Finset.range, HMul.hMul, ite, Eq, HMod.hMod, OfNat.ofNat, Neg.neg, Nat.factorial, HSub.hSub
14 instances, coercions and auxiliary constants left out.
lemma seq_def_eventually line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Eventually, Nat, Eq, Real, A258667, abs, seq_sum, Filter.atTop
Proof uses: id, Filter.Eventually.mono, LT.lt, OfNat.ofNat, dite, LE.le, Not, Int.natAbs, Finset.sum, Int, Finset.range, ite, HMod.hMod, Neg.neg, Int.ofNat, Nat.factorial, HSub.hSub, HMul.hMul, Filter.eventually_gt_atTop, Eq.rec and 8 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def seq_sum_ratio line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, seq_sum, nat_fac_to_real, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
def seq_sum_ratio_term line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.descFactorial, HSub.hSub
19 instances, coercions and auxiliary constants left out.
lemma seq_sum_real_def line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, seq_sum, Finset.sum, Finset.range, HMul.hMul, ite, HMod.hMod, OfNat.ofNat, Neg.neg, Nat.factorial, HSub.hSub
Proof uses: Eq.mpr, Finset.Icc, Max.max, HAdd.hAdd, Min.min, HPow.hPow, Int.ofNat, Nat.choose, id, congr, Int, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.mul_sum, Int.cast_sum, Int.cast_mul and 23 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_eq line 255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, Real, HDiv.hDiv, HMul.hMul, ite, HMod.hMod, OfNat.ofNat, Neg.neg, Nat.factorial, HSub.hSub, nat_fac_to_real, seq_sum_ratio_term
Proof uses: Eq.mpr, HPow.hPow, Finset.sum, Finset.Icc, Max.max, HAdd.hAdd, Min.min, Int.ofNat, Nat.choose, Nat.descFactorial, id, congr, Int, congrArg, Eq.trans, Or, Nat.mod_two_eq_zero_or_one, Or.inl, of_eq_true, True and 30 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_sum_def line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, seq_sum_ratio, Finset.sum, Finset.range, seq_sum_ratio_term
Proof uses: Eq.mpr, HSub.hSub, OfNat.ofNat, id, congrArg, Eq.symm, Finset.sum_range_reflect, HDiv.hDiv, seq_sum, nat_fac_to_real, seq_sum_ratio.eq_1, propext, Eq.comm, HMul.hMul, HPow.hPow, Neg.neg, Nat.descFactorial, ite, HMod.hMod, Nat.factorial and 45 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_zero_of_ge line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, Real, seq_sum_ratio_term, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, eq_comm, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, Nat.descFactorial, HSub.hSub, seq_sum_ratio_term.eq_1, Nat.casesAuxOn, of_eq_true, Finset.sum, Int, Finset.Icc, Max.max, HAdd.hAdd and 37 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_tsum line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, seq_sum_ratio, tsum, seq_sum_ratio_term, SummationFilter.unconditional
Proof uses: id, Eq.mpr, HDiv.hDiv, seq_sum, nat_fac_to_real, HSub.hSub, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, Nat.descFactorial, Finset.sum, Finset.range, ite, HMod.hMod, Nat.factorial, Finset.Icc, Max.max, HAdd.hAdd, Min.min and 67 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_limit line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Filter.Tendsto, Real, seq_sum_ratio_term, Filter.atTop, nhds, HDiv.hDiv, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.factorial
Proof uses: id, Eq.mpr, LE.le, Filter, Filter.map, HMul.hMul, Nat.descFactorial, HSub.hSub, Finset.sum, Finset.Icc, Max.max, HAdd.hAdd, Min.min, Int.ofNat, Nat.choose, Finset.prod, Finset.range, Eq, congrArg, Int and 152 more
285 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma hasSum_exp_minus_two line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: HasSum, Real, Nat, HDiv.hDiv, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.factorial, Real.exp, SummationFilter.unconditional
Proof uses: Eq, NormedSpace.exp, Real.exp_eq_exp_ℝ, Eq.mpr, id, congrArg, of_eq_true
64 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def bound_seq line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat.factorial
13 instances, coercions and auxiliary constants left out.
lemma bound_seq_summable line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Summable, Real, Nat, bound_seq, SummationFilter.unconditional
Proof uses: id, of_eq_true, HDiv.hDiv, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat.factorial, Eq.trans, True, congrArg, funext, mul_div_assoc, eq_true, Summable.mul_left, Real.summable_pow_div_factorial
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma k_sub_succ_eq line 311 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HSub.hSub, HAdd.hAdd, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma choose_sub_one_le_choose_add_one line 313 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Nat.choose, HSub.hSub, OfNat.ofNat, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, zero_tsub, Nat.choose_zero_right, le_self_add, Nat.succ
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma choose_le_choose_add_step line 317 source
no axioms what this means
Statement uses: Nat, LE.le, Nat.choose, HAdd.hAdd, OfNat.ofNat, HSub.hSub
Proof uses: Eq.rec, Nat.succ, Eq, LE.le.trans, Nat.succ_add
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma choose_le_choose_add line 323 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Nat.choose, HSub.hSub, HAdd.hAdd
Proof uses: dite, Nat.rec, le_refl, Nat.zero, Nat.succ, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, zero_tsub, Nat.choose_zero_right, eq_true, True.intro, Eq.rec, Eq, le_add_right, Nat.add, Eq.symm and 7 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma desc_factorial_le_of_le_step line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Nat.descFactorial, HMul.hMul, HPow.hPow, OfNat.ofNat, HSub.hSub, HAdd.hAdd
Proof uses: LE.le.trans_eq, Nat.mul_le_mul, Eq.rec, Eq, 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.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.mul_one, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.zero_mul, Mathlib.Tactic.Ring.pow_congr and 11 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma desc_factorial_le_of_le line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat.descFactorial, HPow.hPow
Proof uses: Eq.mpr, Finset.prod, Finset.range, Fin, Finset.univ, id, Eq, congr, congrArg, Nat.descFactorial_eq_prod_range, LE.le.trans, Finset.prod_le_prod', Function.comp, Membership.mem, Finset, of_eq_true, Eq.trans, True, implies_congr, Eq.refl and 5 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma desc_factorial_bound_nat line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Nat.descFactorial, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: desc_factorial_le_of_le, Decidable.byContradiction, Not
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma term1_bound line 343 source
standard axioms: propext what this means
Statement uses: Nat, LE.le, Nat.choose, HSub.hSub, OfNat.ofNat
Proof uses: term1_bound.match_1, Unit, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, of_eq_true, HAdd.hAdd, Eq.trans, True, congrArg, tsub_eq_zero_of_le, Nat.Simproc.le_add_le, eq_true_of_decide
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma inner_sum_bound_choose line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat.choose, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.Icc, Max.max, HAdd.hAdd, Min.min, Int.ofNat, id, Eq, congr, Int, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, two_mul, Int.cast_sum, Int.cast_mul and 103 more
174 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma inner_sum_nonneg line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat
Proof uses: id, LE.le.trans', Finset.sum, Int, Finset.Icc, Max.max, HSub.hSub, HAdd.hAdd, Min.min, Nat.choose, HMul.hMul, Int.ofNat, Function.comp, Iff.mpr, Int.cast_le, Finset.sum_nonneg', Int.NonNeg.mk, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 4 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_abs line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, abs, seq_sum_ratio_term, HDiv.hDiv, Nat.descFactorial, HSub.hSub, OfNat.ofNat
Proof uses: id, Eq.mpr, HMul.hMul, HPow.hPow, Neg.neg, Max.max, HAdd.hAdd, Min.min, Finset.sum, Int, Finset.Icc, Nat.choose, Int.ofNat, congrArg, mul_div_assoc, abs_mul, abs_neg_one_pow, one_mul, abs_of_nonneg, div_nonneg and 14 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma choose_real_eq line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Nat.choose, HDiv.hDiv, Nat.descFactorial, Nat.factorial
Proof uses: of_eq_true, Eq.trans, True, congrArg, HMul.hMul, Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_mul, mul_div_cancel_left₀, Not, OfNat.ofNat, False, eq_false, Nat.factorial_ne_zero, not_false_eq_true, eq_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_bound_lt line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Real, abs, seq_sum_ratio_term, bound_seq
Proof uses: Eq.mpr, HDiv.hDiv, Nat.descFactorial, HSub.hSub, OfNat.ofNat, id, Eq, congrArg, seq_sum_ratio_term_abs, HMul.hMul, Nat.choose, inner_sum_bound_choose, Nat.factorial, choose_real_eq, HPow.hPow, cast, Eq.symm, Eq.trans, desc_factorial_bound_nat, rfl and 78 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_bound_ge line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, LT.lt, LE.le, Real, abs, seq_sum_ratio_term, bound_seq
Proof uses: id, Nat.casesAuxOn, Eq, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.descFactorial, HSub.hSub, Nat.factorial, of_eq_true, Finset.sum, Int, Finset.Icc, Max.max, HAdd.hAdd, Min.min, Nat.choose, Int.ofNat and 47 more
163 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_term_bound line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, abs, seq_sum_ratio_term, bound_seq
Proof uses: dite, LT.lt, seq_sum_ratio_term_bound_lt, Not, seq_sum_ratio_term_bound_ge
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tsum_limit_eq_exp_minus_two line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, tsum, Nat, HDiv.hDiv, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.factorial, SummationFilter.unconditional, Real.exp
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, eq_comm, NormedSpace.exp, Real.exp_eq_exp_ℝ, of_eq_true, Eq.trans, True, NormedSpace.exp_eq_tsum_div, eq_self
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_limit_tsum line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, tsum, seq_sum_ratio_term, SummationFilter.unconditional, Filter.atTop, nhds, HDiv.hDiv, HPow.hPow, Neg.neg, OfNat.ofNat, Nat.factorial
Proof uses: LE.le, Norm.norm, bound_seq, seq_sum_ratio_term_bound, Summable, bound_seq_summable, seq_sum_ratio_term_limit, tendsto_tsum_of_dominated_convergence, Filter.Eventually.of_forall
41 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_ratio_limit line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, seq_sum_ratio, Filter.atTop, nhds, Real.exp, Neg.neg, OfNat.ofNat
Proof uses: Eq, tsum, seq_sum_ratio_term, SummationFilter.unconditional, funext, seq_sum_ratio_tsum, Eq.mpr, id, congrArg, HDiv.hDiv, HPow.hPow, Nat.factorial, tsum_limit_eq_exp_minus_two, Eq.symm, seq_sum_ratio_limit_tsum
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_equiv line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, seq_sum, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, nat_fac_to_real, HSub.hSub
Proof uses: Filter.Tendsto, HDiv.hDiv, nhds, seq_sum_ratio_limit, Eq.mpr, Exists, Filter.EventuallyEq, Nat.factorial, id, Eq, Exists.intro, Eq.rec, Filter.Tendsto.div_const, div_self, Real.exp_ne_zero, Filter.Eventually.of_forall, Eq.trans, Iff.mp, div_eq_iff, ne_of_gt and 17 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma exp_fac_pos line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, HMul.hMul, Real.exp, Neg.neg, nat_fac_to_real, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, mul_comm, Nat.factorial, nat_fac_to_real.eq_1, Eq.mp, Eq.refl, Function.comp, mul_pos, Iff.mpr, Nat.cast_pos, Nat.factorial_pos, Real.exp_pos
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma seq_sum_abs_equiv line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, abs, seq_sum, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, nat_fac_to_real, HSub.hSub
Proof uses: seq_sum_equiv, id, Eq.mpr, Nat.factorial, Exists, Filter.Tendsto, nhds, Filter.EventuallyEq, Eq, Exists.elim, Eq.mp, seq_sum_abs_equiv.match_1, Exists.intro, Norm.norm, LE.le.trans, Filter, Filter.map, Filter.Tendsto.norm, LE.le, congrArg and 14 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma seq_equiv line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, A258667, HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, nat_fac_to_real, HSub.hSub
Proof uses: Filter.Eventually, Eq, abs, seq_sum, seq_def_eventually, seq_sum_abs_equiv, Eq.mpr, id, congrArg, funext, mul_comm, Exists, Filter.Tendsto, nhds, Filter.EventuallyEq, Exists.imp, Function.comp, Filter.Eventually.mp, Filter.Eventually.mono, Eq.trans and 1 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem target_theorem_0 line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, A258667, A258667_asymptotic_term
Proof uses: HMul.hMul, Real.exp, Neg.neg, OfNat.ofNat, nat_fac_to_real, HSub.hSub, seq_equiv, asymp_term_equiv, Asymptotics.IsEquivalent.trans, Asymptotics.IsEquivalent.symm
17 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/OEIS/A224515_conjecture_existence.lean:269 (different declaration text), APNOutputs/OEIS/A309132_conjecture_carmichael.lean:375 (different declaration text), APNOutputs/OEIS/A382590_conjecture_kth_prime_factor_is_eventually_periodic.lean:303 (different declaration text), APNOutputs/OEIS/a091669_conjecture_primitive_root.lean:275 (different declaration text), APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean:187 (different declaration text), APNOutputs/OEIS/oeis_103311_conjecture_0.lean:240 (different declaration text), APNOutputs/OEIS/oeis_108_conjecture_2.lean:281 (different declaration text), APNOutputs/OEIS/oeis_113254_conjecture_0.lean:153 (different declaration text), APNOutputs/OEIS/oeis_175386_conjecture_0.lean:326 (different declaration text), APNOutputs/OEIS/oeis_194806_conjecture_0.lean:495 (different declaration text), APNOutputs/OEIS/oeis_227582_conjecture_0.lean:306 (different declaration text), APNOutputs/OEIS/oeis_228143_conjecture_1.lean:730 (different declaration text), APNOutputs/OEIS/oeis_243106_conjecture_0.lean:164 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_0.lean:223 (different declaration text), APNOutputs/OEIS/oeis_248802_conjecture_4.lean:841 (different declaration text), APNOutputs/OEIS/oeis_256012_conjecture_0.lean:116 (different declaration text), APNOutputs/OEIS/oeis_267581_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_271591_conjecture_0.lean:518 (different declaration text), APNOutputs/OEIS/oeis_278070_conjecture_0.lean:91 (different declaration text), APNOutputs/OEIS/oeis_282779_conjecture_0.lean:141 (different declaration text), APNOutputs/OEIS/oeis_289411_conjecture_0.lean:189 (different declaration text), APNOutputs/OEIS/oeis_2897_conjecture_0.lean:427 (different declaration text), APNOutputs/OEIS/oeis_306424_conjecture_0.lean:300 (different declaration text), APNOutputs/OEIS/oeis_307865_conjecture_0.lean:212 (different declaration text), APNOutputs/OEIS/oeis_323557_conjecture_0.lean:214 (different declaration text), APNOutputs/OEIS/oeis_340737_conjecture_0.lean:456 (different declaration text), APNOutputs/OEIS/oeis_341254_conjecture_0.lean:136 (different declaration text), APNOutputs/OEIS/oeis_363347_conjecture_2.lean:848 (different declaration text), APNOutputs/OEIS/oeis_372761_conjecture_2.lean:756 (different declaration text), APNOutputs/OEIS/oeis_51293_conjecture_0.lean:517 (different declaration text), APNOutputs/OEIS/oeis_62567_conjecture_0.lean:329 (different declaration text), APNOutputs/OEIS/oeis_A028859_conjecture_1.lean:432 (different declaration text), APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean:264 (different declaration text), APNOutputs/OEIS/oeis_a237271_conjecture_2.lean:124 (different declaration text), APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean:1111 (different declaration text), APNOutputs/OEIS/oeis_a363102_conjecture_1.lean:302 (different declaration text), APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean:182 (different declaration text). Qualify references as target_theorem_0@path.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.