2/3<=L<1 for the fixed log series; x_ell=ell*L/2 satisfies 0<=x_ell<3 and x_(ell+1)-x_ell>=1/3 for ell<6. A weaker [0,7] enclosure is allowed in bounds.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.