Turán density of the tetrahedron $K_4^3$: evaluate $\lim \mathrm{ex}_3(n,K_4^3)/\binom{n}{3}$ (Erdős #500)

Work with $3$-uniform hypergraphs, whose edges are $3$-element subsets (triples) of the vertex set. A copy of $K_4^3$ is a set of $4$ vertices all $\binom{4}{3}=4$ of whose triples are edges (a 'tetrahedron'). Let $\mathrm{ex}_3(n,K_4^3)$ be the largest number of triples that can be placed on $n$ vertices with no $K_4^3$. Determine $\mathrm{ex}_3(n,K_4^3)$, equivalently the Turán density $$\pi(K_4^3)=\lim_{n\to\infty}\frac{\mathrm{ex}_3(n,K_4^3)}{\binom{n}{3}},$$ the largest possible limiting edge density of a $K_4^3$-free $3$-graph.

Acceptance. FULLY RESOLVES: determine the exact Turán density $\pi(K_4^3)$ with a complete proof — both a construction (a family of $K_4^3$-free $3$-graphs whose densities tend to $\pi$) and a matching upper bound proving no $K_4^3$-free $3$-graph exceeds density $\pi$ in the limit. A machine-checkable certificate (a verified flag-algebra/SOS certificate, or a Lean/Coq proof) is preferred; otherwise a complete written proof with all steps. Proving Turán's conjecture $\pi(K_4^3)=5/9$, or exhibiting a $K_4^3$-free construction of limiting density strictly above $5/9$, qualifies. ADVANCES (each independently checkable): (a) improve the upper bound strictly below the best value stated in the background (currently $\approx 0.5611666\binom{n}{3}$) with a verifiable flag-algebra/SDP certificate; (b) improve the lower bound strictly above $5/9$ by exhibiting a $K_4^3$-free construction of higher limiting density, together with a machine-checkable proof that it is $K_4^3$-free and a proof of its density; or (c) determine exact values of $\mathrm{ex}_3(n,K_4^3)$ for new small $n$ by exhaustive search with a reproducible exhaustiveness certificate. Deliver the SDP/SOS certificate + attained bound, the construction + freeness proof, or the search code + exact values.