Dead end: U49 (restart)

Settle Lemma.erdos_1075: prove it or disprove it Method: Prove Lemma.erdos_1075 or its negation: ∀ r : ℕ, 3 ≤ r → ∃ c : ℝ, (r : ℝ)⁻¹ ^ r < c ∧ ∀ ε : ℝ, 0 < ε → ∃ m : ℕ → ℕ, Tendsto m atTop atTop ∧ ∀ᶠ n : ℕ in atTop, ∀ H : Finset (Finset (Fin n)), H.IsUniform r → (1 + ε) * ((n : ℝ) / r) ^ r ≤ H.card → ∃ S : Finset (Fin n), S.card = m n ∧ c * (S.card : ℝ) ^ r ≤ (H.hypergraphInduce S).card. Conjecture from Erdős problem 1075 (https://www.erdosproblems.com/1075): Let $r\ge 3$. There exists $c_r>r^{-r}$ such that, for any $ϵ>0$, if $n$ is sufficiently large, the following holds. Any $r$-uniform hypergraph on $n$ vertices with at least $(1+ϵ)(n/r{)}^r$ many edges contains a subgraph on $m$ vertices with at least $c_r{m}^r$ edges, where $m=m(n)\to \infty$ as $n\to \infty$. Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1075.lean. Start from proofs/Lemma.erdos_1075.lean. A counterexample that only shows the formal statement is wrong (an edge case the problem didn't mean) still counts, and the lab's maintainers will report it upstream; say so in your notes. If neither is in reach, prove a useful special case or lemma, post what blocks you to the chat, and submit the files you started from unchanged, with notes on what you tried and what blocked you: the notebook keeps them as a dead end so others don't repeat it. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U49 dead end for Lemma.erdos_1075. I printed the definitions with #guard_msgs. hypergraphInduce H S = {x ∈ H | x ⊆ S} and IsUniform H r = ∀ e ∈ H, e.card = r, so the formalization is faithful. c is chosen before ε and m may depend on ε, which is the standard definition of a jump. c·m^r edges corresponds to density c·r!, so the statement is exactly Erdős's jump conjecture for α = r!/r^r (for example 2/9 at r=3, a $500 problem), which is open. There is no vacuous edge case: for small ε the hypothesis is satisfiable since (1+ε)(n/r)^r < C(n,r), for instance with complete r-partite hypergraphs, and those satisfy the conclusion only with c ≈ r^{-r}, so it is not a trivial disproof. I am submitting the unchanged starting files.

{"proofs":{}}