Graphs whose every cycle has more vertices than chords: is the maximum edge count linear? (Erdős #642)

Let $f(n)$ be the maximum number of edges in a graph on $n$ vertices in which every cycle has more vertices than chords. Here a chord of a cycle is an edge of the graph joining two vertices of the cycle that are not consecutive along it; the condition requires that for every cycle $C$ in the graph, the number of chords of $C$ is strictly less than the number of vertices of $C$. Is it true that $f(n) \ll n$, i.e. $f(n) \le Cn$ for an absolute constant $C$?

Acceptance. FULLY RESOLVES: a complete proof that $f(n) \le Cn$ for an absolute constant $C$ (machine-checkable Lean/Coq preferred, otherwise a full written proof with all steps); OR a disproof: an explicit family of $n$-vertex graphs with $\omega(n)$ edges together with a proof that every cycle in each graph has strictly more vertices than chords. A finite computation alone cannot settle the asymptotics. ADVANCES: (a) an upper bound with a strictly smaller growth rate than the best bound stated in the background (currently $n(\log n)^8$ — e.g. reducing the power of the logarithm, or reaching $n\cdot(\log n)^{o(1)}$), with proof; (b) a construction with a superlinear-in-$n$ edge count that verifiably satisfies the cycle condition (this refutes the conjecture, but a construction beating $cn$ for the best explicit linear lower-bound constant, with proof, is also an advance); (c) exact values of $f(n)$ for small $n$ with the extremal graphs, computed by exhaustive enumeration and accompanied by the search code and an exhaustiveness certificate; (d) proving the linear bound for a substantive graph class (e.g. bounded degeneracy or bipartite graphs), with proof. Deliver the proof file (or compiling Lean sources), or the construction plus verification, or the enumeration code with the certified table of exact values.