If $a_n/b_n\to 1$ and $A+B$ contains all large integers, is the representation count unbounded? (Erdős #1145)

Let $A=\{1\leq a_1<a_2<\cdots\}$ and $B=\{1\leq b_1<b_2<\cdots\}$ be infinite sets of integers with $a_n/b_n\to 1$. Write $1_A\ast 1_B(n)=\#\{(a,b)\in A\times B : a+b=n\}$ for the number of representations of $n$ as a sum of one element from each set. If $A+B$ contains all sufficiently large positive integers, is it true that $$\limsup_{n\to\infty} 1_A\ast 1_B(n)=\infty?$$

Acceptance. FULLY RESOLVES: a complete proof that the hypotheses force $\limsup 1_A\ast 1_B(n)=\infty$ — machine-checkable (Lean/Coq) preferred, else a full written proof (note this would in particular resolve the Erdős–Turán conjecture, so extraordinary scrutiny applies); OR a counterexample: explicitly defined infinite sequences $A$ and $B$ (given by a computable rule) together with complete proofs of all three properties — $a_n/b_n\to 1$, $A+B$ contains all sufficiently large integers, and $\sup_n 1_A\ast 1_B(n)<\infty$ — plus machine verification of the three properties on a large finite prefix as a sanity certificate. ADVANCES: (a) a proof under clearly stated additional structural hypotheses on $A$ and $B$ that strictly extend what the background records as known; (b) a theorem constraining any potential counterexample (e.g. forcing digit-system-like structure), with proof; (c) a proof that the conclusion holds with $\limsup$ replaced by a weaker but explicit unboundedness statement along a specified subsequence. Deliver the proof file, or the construction rule + proofs + prefix-verification code.