Local pair-piercing vs global transversals: is $f(k,7)=(3/4+o(1))k$? (Erdős #644)

Let $f(k,r)$ be minimal such that the following holds: if $A_1,A_2,\ldots$ is a family of sets, all of size $k$, such that for every collection of $r$ of the $A_i$ there is some pair $\{x,y\}$ which intersects all $r$ of them, then there is some set of size $f(k,r)$ which intersects all of the sets $A_i$. Is it true that $$f(k,7)=(1+o(1))\frac{3}{4}k?$$ Is it true that for every $r\geq 3$ there exists a constant $c_r$ such that $$f(k,r)=(1+o(1))c_r k?$$ (This is a Helly-type transversal problem: a local condition — every $r$ of the $k$-sets can be pierced by just two points — is required to force a small global transversal.)

Acceptance. FULLY RESOLVES: a complete proof determining the asymptotics of $f(k,7)$ (confirming or refuting $(3/4+o(1))k$) AND settling whether $f(k,r)=(1+o(1))c_r k$ for every $r\geq 3$ — a full written proof with all steps, or machine-checkable (Lean/Coq). A proof resolving only the $r=7$ asymptotic is accepted as resolving the problem's lead question and should be flagged as such. ADVANCES: an upper bound $f(k,7)\leq (1-c)k$ for an explicit $c>0$ (strictly better than the trivial bound $f(k,6)=k$ stated in the background), with proof; a lower-bound construction showing $f(k,7)\geq (3/4-o(1))k$, with proof; existence of $\lim_k f(k,r)/k$ for some $r\geq 7$; or exact values of $f(k,7)$ for small $k$, each certified by an extremal family (checkable witness) plus a program-verifiable argument (ILP/SAT certificate with a stated finite reduction) that no smaller transversal size suffices. Deliver the proof file, or the constructions/code plus certificates and the table of computed values.