Turán density of $C_4$ in the hypercube: does $(1/2+o(1))n2^{n-1}$ edges force a $C_4$? (Erdős #86)

Let $Q_n$ be the $n$-dimensional hypercube graph, with $2^n$ vertices (the binary strings of length $n$) and $n2^{n-1}$ edges (pairs of strings differing in one coordinate). Is it true that every subgraph of $Q_n$ with at least $$\left(\tfrac12+o(1)\right)n2^{n-1}$$ edges contains a $4$-cycle $C_4$? Equivalently, writing $f(n)$ for the maximum number of edges in a $C_4$-free subgraph of $Q_n$, is $f(n)\leq\left(\tfrac12+o(1)\right)n2^{n-1}$?

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable preferred, else full written) that $f(n)=(\tfrac12+o(1))n2^{n-1}$ — the $C_4$-free edge-density coefficient tends to $1/2$ — OR a disproof: a construction plus proof that $\limsup_n f(n)/(n2^{n-1})>1/2$. ADVANCES: lower the upper-bound coefficient strictly below the best stated in the background ($0.60318\,n2^{n-1}$, Baber) with a verifiable flag-algebra / SDP certificate; OR improve the lower-order term of the lower bound beyond Brass–Harborth–Nienborg's $(\tfrac12+c/\sqrt{n})$ via an explicit construction and proof; OR extend the exact sequence $f(n)$ (maximum edges in a $C_4$-free subgraph of $Q_n$) to a new record $n$ by ILP/exhaustive search with a reproducible program and exhaustiveness certificate. Deliver the proof file, the SDP certificate, the explicit construction plus proof, or the search code plus certified values.