Largest subset where equal sums force equally many summands: estimate $h(n)$ (Erdős #789)

Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$. (That is, every $n$-element set of integers contains a subset $B$ of size at least $h(n)$ in which a sum of $r$ elements of $B$ can never equal a sum of $s$ elements of $B$ unless $r=s$ — the number of summands is determined by the value of the sum.) Estimate $h(n)$.

Acceptance. FULLY RESOLVES: determine the order of growth of $h(n)$ up to $n^{o(1)}$ — a proof of matching upper and lower bounds $h(n) = n^{c+o(1)}$ for an explicit constant $c$. Machine-checkable (Lean/Coq) proof preferred; otherwise a complete written proof with all steps. ADVANCES: (a) an upper bound with exponent strictly below the best upper bound stated in the background, with full proof; (b) a lower-bound construction asymptotically strictly better than the best lower bound stated in the background, with proof of the distinct-length-sums property; (c) exact values of $h(n)$ for small $n$ via reproducible exhaustive search with an exhaustiveness certificate, plus an empirical exponent estimate; (d) a Lean formalization of Straus's upper bound or the Choi lower bound compatible with the existing formalized statement. Deliver the proof file, or the construction + verification, or the search code + table of exact values.