Dead end: U80 (restart)

Settle Lemma.erdos_1158: prove it or disprove it Method: Prove Lemma.erdos_1158 or its negation: ∀ t r : ℕ, 2 ≤ t → 2 ≤ r → ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ ((t : ℝ) - (r : ℝ) ^ (1 - (t : ℝ)) - ε) ≤ (Hypergraph.partiteExtremalNumber n t r : ℝ). Question from Erdős problem 1158 (https://www.erdosproblems.com/1158): Let $K_t(r)$ be the complete $t$-partite $t$-uniform hypergraph with $r$ vertices in each class. Is it true that $${\mathrm{ex}}_t(n,K_t(r))\ge n^{t-r^{1-t}-o(1)}$$ for all $t,r\ge 2$? The restriction $r\ge 2$ excludes forbidding a single edge. Formal statement: formal-conjectures FormalConjectures/ErdosProblems/1158.lean. Start from proofs/Lemma.erdos_1158.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): U80 dead end for Lemma.erdos_1158. Printed definitions with #guard_msgs: partiteExtremalNumber n t r = extremalNumber n t (fun H => ¬ H.ContainsCompletePartiteHypergraph t r), extremalNumber = sup of card over subfamilies of powersetCard t univ (Fin n) satisfying P; ContainsCompletePartiteHypergraph H t r = ∃ f : Fin t × Fin r ↪ V, ∀ a : Fin t → Fin r, image (i ↦ f(i, a i)) ∈ H. This is exactly ex_t(n, K_t(r)), so the statement is faithful, with no edge case (t,r ≥ 2, eventually in n). The t=2 case is Zarankiewicz's ex(n,K_{r,r}) ≥ n^{2-1/r-o(1)}, which is open for r ≥ 4, so the full statement is open. I did not attempt formalizing the probabilistic deletion bound n^{t-(rt-t)/(r^t-1)} because it does not reach the conjectured exponent. Submitting the starting files unchanged. Statement checked: faithful Blocked by: out-of-reach Would unblock it: The t=2 case alone is the lower bound ex(n,K_{r,r}) ≥ n^{2-1/r-o(1)}, which is open for r≥4 (Kollár–Rónyai–Szabó and Bukh only cover unbalanced K_{s,t}), so a proof needs new constructions for the Erdős box problem; a disproof would need to improve the known upper bounds, which is also open.

{"proofs":{}}